[Prev][Next][Index][Thread]
[Giuseppe.Longo@THEORY.CS.CMU.EDU: Re: the cmu workshop]
PEPPE LONGO JUST FORWARDED THE FOLLOWING PROGRAM OF A WORKSHOP ON TYPES HELD
AT CMU.
---------------------
Friday, April 15
9:00 Dana Scott and Daniel Leivant: Welcome
Session 1:
9:05 Henk Barendregt: The forest of lambda calculi with types
10:00 Val Breazu-Tannen: Some comparative anatomy of type disciplines
10:55 John C. Mitchell: Typed lambda models and cartesian closed categories
12:00 LUNCH
Session 2:
1:40 Gordon Plotkin: TBA
2:35 Kim Bruce: A modest model of records, inheritance,
and bounded quantification
3:30 COFFEE BREAK
3:45 Peppe Longo: An introduction to models as internal categories: examples
4:10 Andrea Asperti: Categorical models for higher order calculi
5:00 Luca Cardelli: Time for a new language
vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Saturday, April 16
Session 3:
9:00 Phil Scott: Semantic parametricity in polymorphic lambda calculus, Part I
9:55 Peter Freyd: Semantic parametricity in polymorphic lambda calculus, II
10:50 COFFEE BREAK
11:05 Andre Scedrov: Semantic parametricity in polymorphic lambda calculus, III
12:00 Rick Statman: Combinators and the theory of partitions
1:00 LUNCH
Session 4:
2:15 Dana Scott: Domains and algebras
3:10 Carl Gunter: Coherence and consistency in domains
4:05 COFFEE BREAK
4:20 John Gray: Abstract semantics for dependent types
5:15 DISCUSSION
vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv
ABSTRACTS:
=========
Andrea Asperti (CMU)
CATEGORICAL MODELS FOR HIGHER ORDER CALCULI
Category Theory has been a fundamental instrument for the semantic
investigation both of Functional Programming (the theory of Cartesian
Closed Category), and Intuizionistic Logic (Topos Theory).
Those semantic studies suggested two independent notions of Model
for the system Fw of Girard: the first, due to Seely, is based on
an algebraic generalisation of the semantic of simply typed lambda-
calculus, in a bidimensional universe of ortogonal cartesian closed
categories; the second,suggested by Moggi, was inspired by some notions
of Topos Theory, and in particular by the process of Internalisation.
We present an equational understanding of Moggi's approach and compare
the two notions of model.
Indeed, given a model a la Moggi, there is a canonical way to
define a model a la Seely; moreover the interpretation given by
Moggi, coincide with the one given by Seely on the derived model.
It will pointed out that
Moggi's notion of model, though less general, is much more "suggestive".
============================================================
Henk Barendregt (Nijmegen University, The Netherlands)
THE FOREST OF LAMBDA CALCULI WITH TYPES
Lambda calculi with various notions of generalized types---
dependent, polymorphic, parameterized, impredicative, recursive---are
proliferating. We separate them into the systems a la Curry and those a la
Church, and then present the main systems in their simplest form in a uniform
way.
============================================================
Val Breazu-Tannen (University of Pennsylvania)
SOME COMPARATIVE ANATOMY OF TYPE DISCIPLINES
The type disciplines living in the "forest of typed lambda calculi"
find themselves in natural containment relationships. We regard a
richer type discipline as introducing a new programming language
feature, for example, explicit polymorphism in the case of the
Girard-Reynolds calculus. How do these new features interact with the
ones expressible in a less complex type discipline?
This question can be formalized through results about the
relationships (such as conservative extension) between equational
theories. We survey several results of this kind and we discuss the
relative merits of semantic vs. syntactic methods in obtaining them.
============================================================
Kim Bruce
A MODEST MODEL OF RECORDS, INHERITANCE, AND BOUNDED QUANTIFICATION
Mitchell introduced, and Cardelli & Wegner refined, an extension of the
second order lambda calculus, Bounded Fun, which supports both
parametric polymorphism and inheritance. This language is very
interesting in that it provides the programmer with more control over the
types of expressions than is typical in object-oriented programming
languages. In this talk a generalization of partial equivalence
relations, known as omega-sets, are used in combination with modest sets
(p.e.r.'s) to provide the first known model of Bounded Fun (with explicit
polymorphism). The partial equivalence relations support a very natural
and intuitive interpretation of records and inheritance which still preserves
the necessary complexities of inheritance as it is used in object-oriented
languages.
[Joint work with Giuseppe Longo]
============================================================
Luca Cardelli (DEC Systems Research Center)
TIME FOR A NEW LANGUAGE
Work in logic and type theory in the past 20 years has generated a
number of advanced concepts which have not yet been fully exploited
in (practical) programming languages (the main partial exception being
Standard ML). It seems that the times are mature for embedding
these developments in a coherent design.
These concepts include type quantifiers (encompassing polymorphism
and abstract types), higher kinds, a general notion of subtyping,
structural type matching, and a generalized correspondence principle.
All of this should be useful in the context of a practical
sequential language.
However, a language is not just a formal system. Although many ideas
>from logic can be adopted without change, others have to be modified
for notational convenience, or restricted to allow practical realization
(e.g. ability to carry out compilation). We discuss how some theoretical
concepts go too far, while others do not go far enough.
============================================================
PETER J. FREYD (University of Pennsylvania)
SEMANTIC PARAMETRICITY IN POLYMORPHIC LAMBDA CALCULUS II
Among various notions of polymorphism delineated by Strachey, perhaps
the most influential is the notion of parametric polymorphism. In-
tuitively, a parametric polymorphic function is one that has a uniformly
given algorithm for all types. A semantic condition necessary for
parametricity was proposed by Reynolds as a kind of invariance under
relations between type values. For example, a parametric function
t of type ALL p. ((p=>p) => (p=>p)) should be invariant at least
under isomorphisms between values of type parameter p , i.e., given
type values A and B and an isomorphism f: A --> B , t should
send related maps to related maps. That is, the instances t[A] of
type (A=>A) => (A=>A) and t[B] of type (B=>B) => (B=>B) should
satisfy the condition that given any g: A --> A and h: B --> B
such that g;f = f;h , it must be the case that t[A](g);f = f;t[B](h).
This strongly suggests that in order to capture parametricity seman-
tically, the value of a type abstraction should not be an entire
product, but only that part consisting of parametric polymorphic
functions. A categorical framework for parametricity may be given
by means of uniform (or: dinatural) transformations (see abstract
of P.J. Scott's talk). In general, composition of uniform trans-
formations is problematic. We resolve this problem in the context
of partial equivalence relations on natural numbers and discuss
a semantics for parametric polymorphism in this setting.
This is joint work with E.S. Bainbridge, A. Scedrov, and P.J. Scott.
============================================================
John Gray (University of Illinois at Urbana)
ABSTRACT SEMANTICS FOR DEPENDENT TYPES
The talk will describe some ongoing attempts to use the category of sketches
as a model for Martin-Lof type theory.
============================================================
Carl Gunter (University of Pennsylvania)
COHERENCE AND CONSISTENCY IN DOMAINS
Almost all of the domains normally used as a mathematical
foundation for denotational semantics satisfy a condition known as
CONSISTENT COMPLETENESS. The goal of this paper is to explore the
possibility of using a different condition---that of COHERENCE---which
has its origins in topology and logic. In particular, we concentrate
on those posets whose principal ideals are algebraic lattices and
whose topologies are coherent. These form a cartesian closed category
which has fixed points for domain equations. It is shown that a
``universal domain'' exists. Since the construction of this domain
seems to be of general significance, a categorical treatment is
provided and its relationship to other applications discussed.
[Joint work with Achim Jung, Technische Hochschule, Darmstadt]
============================================================
John C. Mitchell (Stanford University)
TYPED LAMBDA MODELS AND CARTESIAN CLOSED CATEGORIES
This talk will survey basic facts about the interpretation
of typed lambda calculi in both set-theoretic models and
cartesian closed categories (ccc's). We will discuss general
and specialized completeness theorems, and compare
interpretation functions associated with both kinds of
models. It will be pointed out that ccc's satisfy the
non-equational property of extensionality, provided one
is content with the internal logic of the structure.
[Joint work with Philip Scott]
============================================================
Andre Scedrov (University of Pennsylvania)
SEMANTIC PARAMETRICITY IN POLYMORPHIC LAMBDA CALCULUS III
We consider a semantic framework for Strachey's parametric poly-
morphism, in which the crucial semantic condition for parametricity
is given as invariance or uniformity in mappings between type values
(see abstracts of talks by P.J. Scott and by P.J. Freyd). We explore
this semantic notion of parametricity in the context of coherent
spaces and linear maps. Every function definable in second-order
polymorphic lambda calculus is shown to satisfy our uniformity
condition. This result yields an inherently parametric interpre-
tation of second-order polymorphic lambda calculus which satisfies
many additional desirable equations between terms, e.g. commutation
rules for definable disjunction and existential type abstraction.
We also show that our uniformity condition arises already in the
restricted setting of coherent spaces and embeddings: it is equivalent
to the pullback condition for elements of variable type, an essential
ingredient in Girard's coherent semantics.
[Joint work with P.J. Freyd, J.Y. Girard, and P.J. Scott]
============================================================
P.J. Scott (University of Ottawa)
SEMANTIC PARAMETRICITY IN POLYMORPHIC LAMBDA CALCULUS, Part I
We introduce a general categorical framework for interpreting
types and terms in polymorphic languages which accounts for
natural compatibility conditions related to parametricity.
In general, types will be interpreted as certain multivariate
functors (on an appropriately complete ccc) and terms as certain
kinds of generalized ("uniform" or "dinatural") transformations
between types. Quantifiers interpret as "Ends" or "Co-ends"
of functors.Although this framework is geometrically and
conceptually satisfying (e.g. the type constructor A ==> B
retains its essential character of being contravariant in A
and covariant in B) , there is an inherent problem with
compositionality. But this difficulty can be overcome in
numerous significant cases (Syntax, Per-models, Girard's
Coherent domains, etc.): this will be further discussed
in Parts II and III by Freyd and Scedrov. There also appear
to be connections with proof theory and Girard's Linear Logic.
============================================================
Rick Statman
COMBINATORS AND THE THEORY OF PARTITIONS
Our main result is that the unification problem for the untyped
lambda calculus based on B and I alone (with suitable combinatory axioms
equivalent to beta or beta eta conversion) is undecidable. The proof
depends on a new normal form for B,I combinations which puts these
combinators into one to one correspondence with integer partitions.
The correspondence is exactly the one that is obtained between integer
partitions (with a fixed "triangle number") and binary trees through
the "walks below the diagonal" construction familiar from elementary
combinatorics. The normal form permits us to encode Hilbert's 10th
problem into unification. In addition, it follows that any model
of this calculus either contains the free model or has B = I (so
application is associative and the model is just a monoid). We also
derive certain properties of the B,I monoid such as the right
cancellation law.