http://www.cedar-forest.org/forest/events/inaugural-workshop2000/ina-abstracts2.html

ULTRA group Useful Logics, Types, Rewriting, and Applications |
UKII UK Institute of Informatics, UK |

The list of abstracts of the lectures is as follows:

Henk Barendregt **Catholic University of Nijmegen **

Stefano Berardi ** University of Turin**

N.G. de Bruijn **Eindhoven University of Technology**:

Alan Bundy ** University of Edinburgh**

Gilles Dowek **INRIA**

Martin Hofmann
** University of Edinburgh**

We present this both as a ``design pattern'' for writing C-code in a functional style and as a compilation process from linearly typed first-order functional programs into malloc()-free C code.

The main technical result is the correctness of this compilation.

The crucial innovation over previous linear typing schemes consists of the introduction of a resource type <> which controls the number of constructor symbols such as cons in recursive definitions and ensures linear space while restricting expressive power surprisingly little.

While the space efficiency brought about by the new typing scheme and the compilation into C can also be realised by with state-of-the-art optimising compilers for functional languages such as Ocaml, the present method provides guaranteed bounds on heap space which will be of use for applications such as languages for embedded systems or proof carrying code.

We discuss various extensions, in particular an extension with FIFO queues admitting constant time catenation and enqueuing, and an extension of the type system to fully-fledged intuitionistic linear logic.

Helene Kirchner **University of Nancy**

Jan-Willem Klop
** Free University of Amsterdam **

Gordon Plotkin **University of Edinburgh**

It is based on their Fraenkel-Mostowski (FM) set model. Inspired by this work, we present a very similar language based instead on the Fiore-Plotkin-Turi presheaf model (over the category of finite cardinals).

The main difference is in the approach to the type theory. For Gabbay and Pitts the judgments are that a value has a certain type and that it does not depend on certain atoms. We rather take a positive approach and the judgment is that the atoms depended on are included in a certain set (cf. analogous statements about free variables in languages with binders). This positive judgment is then part of the structural logic of the type theory and is internalised by the abstraction functor, yielding a straightforward semantics (just as commas in contexts are internalised by products).

It may be that the two approaches are equivalent, apart from a certain linearity restriction inherent in the FM model. We have at any rate shown that one is not restricted to the FM model for the semantics of variable-binding metalanguages, and it remains unclear which model is to be preferred.

Simona Ronchi Della Rocca
** University of Turin **

- fixing the degree of parallelism of every rule in it;
- modifying its structure by introducing some conjunction introduction rules;
- decorating the resulting proof schema by logical formulas.

Jonathan Seldin
**Lethbridge University**

\begin{thebibliography}{}

\bibitem[Berardi 1993]{berardi:EDTP} Stefano Berardi. (1993) \newblock Encoding of data types in pure construction calculus: a semantic justification. \newblock In G\'{e}rard Huet and Gordon Plotkin, editors, {\em Logical Environments}, pages 30--60. Cambridge University Press.

\bibitem[Pfenning and Paulin-Mohring 1989]{pfenning/paulin-mohring:IDTC} Frank Pfenning and Christine Paulin-Mohring. (1989) \newblock Inductively defined types in the calculus of constructions. \newblock In M.~Main, A.~Melton, M.~Mislove, and D.~Schmidt, editors, {\em Mathematical Foundations of Programming Semantics: 5th International Conference, Tulane University, New Orleans, Louisiana, USA, March 29--April 1, 1989, Proceedings}, volume 442 of {\em Lecture Notes in Computer Science}, pages 209--228. Springer-Verlag.

\bibitem[Seldin 1997]{seldin:PTCC} Jonathan~P. Seldin. (1997) \newblock On the proof theory of {C}oquand's calculus of constructions. \newblock {\em Annals of Pure and Applied Logic}, 83:23--101.

\end{thebibliography}

Joe Wells **Heriot-Watt University**

While there is a rich theory of universal/existential quantifiers, there are two important difficulties in practice. (1) Systems with these quantifiers generally do not have a strong principality property, i.e., there is no most general analysis for each program fragment. This makes it difficult to perform type analysis compositionally (i.e., where program fragments are analyzed independently) and sometimes even makes type analysis impossible. (2) These quantifiers hide information, making it hard to extend type analysis to flow analysis and to perform type/flow-directed program transformations.

To address these difficulties, I have designed type systems which support type polymorphism with intersection and union types instead of universal/existential types. In collaboration with my colleagues in the Church Project, I have developed analysis and transformation algorithms using these systems. Overcoming difficulty (1), we have used intersection type systems with strong principality properties to develop new type analysis algorithms which are compositional and also accept many safe programs rejected as ill-typed by earlier algorithms. Overcoming difficulty (2), we have shown how to use a system with intersection/union types to express polyvariant flow analyses and to guide a new style of program transformation and optimization: type/flow-directed compilation. This new technology is the foundation for an experimental compiler we are developing. I will discuss how our new approach to compilation will contribute to efficient, reliable, and modular compilation.

Maintained by Fairouz Kamareddine ()