headers
Delia Kesner | 2 Nov 2001 10:52
Picon

Workshop on Higher-Order Rewriting

     The First International Workshop on Higher-Order Rewriting

                July 21st, 2002, Copenhagen, Denmark 

                   Held in conjunction with FLOC'02

                    http://www.lri.fr/~kesner/hor/

------------------------------------------------------------------------

Purpose: 

The aim of HOR is to provide an informal setting to discuss recent work and
work in progress concerning higher-order rewriting.

Scope:

The topics of the workshop include, but are not limited to: 

* Applications

  proof checking, 
  theorem proving, 
  declarative programming, 
  program transformation.

* Foundations

  pattern matching,
  unification,
(Continue reading)

Permalink | Reply | 0 comments |
headers
Carsten Schuermann | 6 Nov 2001 17:32
Picon
Favicon

PLI 2002-Second call for workshop proposals


                   SECOND CALL FOR WORKSHOP PROPOSALS

                 Principles, Logics, and Implementations
             of high-level programming languages (PLI 2002)
                           Pittsburgh, USA

                         October 3 - 8, 2002
                          Carsten Schuermann

                 http://www.cs.yale.edu/~carsten/pli02

PLI 2002, a federation of colloquia which includes ICFP 2002
(ACM-SIGPLAN International Conference on Functional Programming), PPDP
2002 (ACM-SIGPLAN International Conference on Principles and Practice
of Declarative Programming), and GC 2002 (ACM-SIGPLAN Conference on
Generative Component-based Software Engineering (GCSE), and the
Semantics, Applications, and Implementation of Program Generators
(SAIG) Generators and Components).  PLI 2002 will be held in
Pittsburgh, USA, October 3 - 8 2002.  Affiliated workshops will be
scheduled from October 3 through October 8.

Researchers and practitioners are invited to submit workshop
proposals, that may be sent to the PLI 2002 Workshop Chair

        Carsten Schuermann, carsten@...

by e-mail (Postscript, Pdf, ASCII) with "PLI02 Workshop Submission" in
the subject header.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Nicola Santoro | 7 Nov 2001 07:46
Picon
Picon
Favicon

TCS 2002 - Call for Papers

-----------------------------------------------------------------
                                  CALL FOR PAPERS
-----------------------------------------------------------------

                      2nd IFIP International Conference on

                       THEORETICAL COMPUTER SCIENCE

                                   (TCS 2002)

                         Montreal, August 25-30, 2002

-----------------------------------------------------------------
                    co-sponsored by  EATCS and ACM SIGACT
-----------------------------------------------------------------

The program of of the conference will be composed of two tracks:

Track 1 -  Algorithms, Complexity and Models of Computation
Track 2  -  Logic, Semantics, Specification and Verification.
-----------------------------------------------------------------

Important Dates:

December  3, 2001:  Submissions
February 20, 2002:  Notifications
-----------------------------------------------------------------

Conference Chair
----------------
(Continue reading)

Permalink | Reply | 0 comments |
headers
Mark A. Sheldon | 7 Nov 2001 19:46
Picon

Re: [very] basic question


It's been a few years, but here we go:

In the realm of formal semantics, types are sets with a bit of
structure.  A set is a collection of objects, period.  To make
programming language semantics work out (eg, to ensure the existence of
fixed points), types are required to be sets with an ordering relation
that satisfies certain properties.  Such a set together with its
ordering relation that satisfies the necessary properties (see below) is
usually called a Domain.

The relation is often called something like is-less-defined-than and is
typically written with a less-than-or-equal-to operator, often with the
less-than symbol squared off (though sometimes confusingly written like
the subset symbol).  I'll write <= in ASCII.  Like
less-than-or-equal-to, the relation is reflexive, antisymmetric, and
transitive.  This relation is NOT less-than.  For example, 3 and 4 are
both elements of the INT type (integers).  For type theorists, 3 and 4
are not comparable (neither is <= the other).  Likewise, TRUE and FALSE
are elements of BOOLEAN and are incomparable.

Exactly what properties are required of the sets and ordering relation
are a subject of some research and the object of much ingenuity in the
world of programming language semantics.  Some early semantics required
that domains be complete lattices, but we know that if all types are
CPOs (complete partial orders), then things work very neatly.  A CPO is
a set and ordering relation such that every subset of domain has a least
element in the domain.  For simple sets like the integers, we can make a
domain, like INT, by
(Continue reading)

Permalink | Reply | 0 comments |
headers
jeremy | 7 Nov 2001 23:17
Picon
Picon

Re: [very] basic question

  Could someone explain the difference between types & sets?  The maths
  texts I have available (undergrad comp. sci. stuff) state their
  equivalence explicitly, yet many writings I've looked up on the web
  differentiate between them.

In functional programming languages (such as Standard ML, 
used in the following example) a type may well not be a set.

For example

(* set up a type called thing *)
datatype thing = T of thing -> bool ;

(* an example value of this type *)
val example_thing = T (fn _ => true) ;

(* an isomorphism between things and functions : thing -> bool *)

val make_thing = T ;
fun dest_thing (T f) = f ;

(* ie make_thing and dest_thing are mutually inverse; *)

So if the type thing were a set then the cardinalities
|thing| and |{predicates on thing}| would be the same.
Note that {predicates on thing} is equiv to P (thing),
where P means power-set. 
So the type thing cannot be modelled as a set.

When you run the above, the output (which reports types of the
(Continue reading)

Permalink | Reply | 0 comments |
headers
CSL02 | 8 Nov 2001 11:57
Picon
Picon

Computer Science Logic 2002 (CSL'02) announcement


            Annual Conference of the European Association for
                        Computer Science Logic

                               CSL'02

                 22--25 September 2002, Edinburgh, UK

Computer Science Logic (CSL) is the annual conference of the European
Association for Computer Science Logic (EACSL). The conference is
intended for computer scientists whose research activities involve
logic, as well as for logicians working on issues significant for
computer science. Suggested topics of interest include: automated
deduction and interactive theorem proving, constructive mathematics
and type theory, equational logic and term rewriting, linear logic,
logical aspects of computational complexity, finite model theory,
higher order logic, logic programming and constraints, lambda and
combinatory calculi, logical foundations of programming paradigms,
modal and temporal logics, model checking, functions of program
development (specification, extraction, transformation...),
categorical logic and topological semantics, domain theory, database
theory.

The following have agreed to deliver invited lectures:
 Susumu HAYASHI (Kobe)
 Frank NEVEN (Limburg)
 Damian NIWINSKI (Warsaw)

The proceedings will be published in the Sprinter Lecture Notes in
Computer Science.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Frank Atanassow | 8 Nov 2001 13:08
Picon

Re: [very] basic question

Even before going into fixpoints and higher-order functions and domain
equations, one might object to the notion of types-as-sets on the basis that
it is too fine-grained an equivalence. In most programming languages, types
are only defined up to isomorphism, i.e., the particular representations of
values don't really matter. For example, you could model the ML type "unit" as
a one-element set, but which one? It doesn't matter, and in fact the same
holds for every single type constructor in the typed lambda-calculus.

Having realized that, you might start wondering whether the properties you
need to model typed lambda-calculus really have anything specifically to do
with sets at all! If you formulate those properties, then you discover that
there actually is a large collection of candidate structures, and sets and
functions are only one lone example (though admittedly one with a lot of
historical momentum). The upshot is that, though you can reason about sets
by treating them as types, if you try to reason about types by treating them
as sets, you may go wrong.

--

-- 
Frank Atanassow, Information & Computing Sciences, Utrecht University
Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands
Tel +31 (030) 253-3261 Fax +31 (030) 251-379
Permalink | Reply | 0 comments |
headers
John R Harrison | 8 Nov 2001 18:21
Picon

Re: [very] basic question


| datatype thing = T of thing -> bool ;
|
| [....]
| 
| So if the type thing were a set then the cardinalities
| |thing| and |{predicates on thing}| would be the same.
| Note that {predicates on thing} is equiv to P (thing),
| where P means power-set. 
| So the type thing cannot be modelled as a set.

Your example does nothing to justify such a claim. It merely suggests
that in such a model the type constructor "->" should not be interpreted
as the full function space. Since there are only countably many
computable functions, this is hardly a surprising observation. You might
just as well say that floating-point numbers "cannot be modelled" as real
numbers because the `+' you write in a program is not associative. I'm
not taking any particular position on the type/set distinction here,
merely pointing out what seems to me something of an overstatement.

John.
Permalink | Reply | 0 comments |
headers
jeremy | 9 Nov 2001 00:36
Picon
Picon

Re: [very] basic question

> From: John R Harrison <johnh@...>
> 
> 
> | datatype thing = T of thing -> bool ;
> |
> | [....]
> | 
> | So if the type thing were a set then the cardinalities
> | |thing| and |{predicates on thing}| would be the same.
> | Note that {predicates on thing} is equiv to P (thing),
> | where P means power-set. 
> | So the type thing cannot be modelled as a set.
> 
> Your example does nothing to justify such a claim. It merely suggests
> that in such a model the type constructor "->" should not be interpreted
> as the full function space. Since there are only countably many
> computable functions, this is hardly a surprising observation. You might
> just as well say that floating-point numbers "cannot be modelled" as real
> numbers because the `+' you write in a program is not associative. 

I probably would say that, actually, though I have to admit I'd be wrong,
since I can't deny you could model floats (or types, for that matter)
as reals, integers, naturals or even prime numbers.
But such models would have the unhelpful feature that there wouldn't
be much correspondence between the characteristics of floats (or types)
and those of reals, integers or whatever.

The textbooks I have which say types are sets also tell us that A -> B
means the entire set of functions from A to B.
(eg Sethi, Programming Languages Concepts and Constructs,
(Continue reading)

Permalink | Reply | 1 comment |
headers
Robin Adams | 9 Nov 2001 03:37
Picon
Picon

Re: [very] basic question

On Wed, 31 Oct 2001, Scott Finnie wrote:

> Could someone explain the difference between types & sets?  The maths
> texts I have available (undergrad comp. sci. stuff) state their
> equivalence explicitly, yet many writings I've looked up on the web
> differentiate between them.

You've had a few responses from a computer science point of view now; I'd
like to give my opinion, coming from a more mathematical background.  I
think the one thing that's been made clear so far is that this is not a
very basic question at all; it's quite a profound one.  There is by no
means one correct opinion that type theorists have settled on.  I am often
disappointed that attention to type theory has largely been confined to
computer scientists so far, when I think there are many issues (such as
this one) that mathematicians and philosophers are better placed to
investigate.

Type theory and set theory are both formal theories that try to deal with
our notion of "collection of things"; but they do so in different ways.  
The differences are subtle, and, when stated informally, they sound
pedantic or hair-splitting; but they lead to important differences in the
way the theories can be used.  Please don't spend too long analysing the
exact words I use; I'm doing my best to express things that aren't fully
understood.  I'm afraid the only real way to understand the differences is
to get involved in the formal theories yourself.

On the level of the logic used, the major difference is that, in set
theory, "a (epsilon) A" (a is a member of the set A) is one proposition
among many.  We can make it the hypothesis or conclusion of an implication
(If a (epsilon) A then ...), we can make it part of a disjunction (Either
(Continue reading)

Permalink | Reply | 0 comments |

Gmane