Institut für Informatik der Ludwig-Maximilians-Universität München

* LICS99
*

We present a new approach to introducing an extensional propositional equality in Intensional Type Theory. Our construction is based on the observation that there is a sound, intensional setoid model in Intensional Type theory with a proof-irrelevant universe of propositions and eta-rules for Pi- and Sigma-types. The Type Theory corresponding to this model is decidable, has no irreducible constants and permits large eliminations, which are essential for universes.

**Available**:- Postscript (64KB,comp) DVI-File (35KB,comp) BibTeX Entry

* Annual Conference of the European Association for Computer Science Logic 99
*

We present a definition of untyped lambda-terms using a heterogeneous datatype, i.e. an inductively defined operator. This operator can be extended a Kleisli triple, which is a concise way to verify the substitution laws for lambda-calculus. We also observe that repetitions in the definition of the monad as well as in the proofs can be avoided by using well-founded recursion and induction instead of structural induction. We extend the construction to the simply typed lambda-calculus using dependent types, and show that this is an instance of a generalisation of Kleisli triples. The proofs for the untyped case have been checked using the LEGO system.

**Available**:- Postscript (119KB,comp) DVI-File (35KB,comp) BibTeX Entry

* International Workshop, Types 98, Selected Papers
*

This book contains a selection of papers presented at the second annual workshop held under the auspices of the Esprit Working Group 21900 TYPES. The workshop took place in Irsee, Germany, from the 27th of March to the 31th of March 1998 and was attended by 89 people.

**Available**:-
Table
of Contents
*(not yet available)*BibTeX Entry

* Annual Conference of the European Association for Computer Science Logic 98
*

We investigate a lambda calculus with positive inductive and coinductive types , which we call lambda^mu,nu using logical relations. As an application we show that using the principle of monotone inductive definitions on positive type schemes no new functions can be defined.

**Available**:- Postscript (100KB,comp) DVI-File (25KB,comp) BibTeX Entry

* Manuscript submitted to Information and Computation
*

In this paper we give a semantical proof of reduction-free normalisation for a version of Girard's system F with full beta-eta-equality for both kinds of abstraction. This generalizes the semantical normalisation algorithms for simply-typed systems to polymorphism.

**Available**:- Postscript (170KB,comp) DVI-File (64KB,comp) BibTeX Entry

* Lecture Notes, ESSLLI 96, Prague
*

These notes present some simple examples of mechanic program verification in Type Theory. The examples have been developed using the ALF proof editor.

Type Theory is a basic formalism which can be viewed as a constructive alternative to set theory. The important ideas were developed by the Swedish logician Per Martin-Löf in the early 70's. Due to its constructive character Type Theory can be viewed as a pure functional programming language whose type system is so powerful that specifications can be expressed as types. Verifying correctness is then reduced to type checking.

We shall present Type Theory based on this (modern) point of view. Intuitionistic logic can be encoded inside the theory using the idea of propositions as sets (and proofs as programs). We emphasize in particular the idea of integrated verification, i.e. where the program and the correctness proof are considered as a unit.

The material presented here is the background to some lectures I gave: First in February '95 as a postgraduate course at Chalmers University of Technology, then in October '95 as a one week seminar at the University of Kent and during summer term '96 as a course at the Ludwig-Maximilian-University in München. I prepare these notes especially for a course at the summer school ESSLLI '96 which is taking place in August '96 in Prague.

**Available**:- Postscript (229KB,comp) BibTeX Entry

* 11th Annual IEEE Symposium on Logic in Computer Science, pages 98-106
*

We give a semantic proof that every term of a combinator version of system F has a normal form. As the argument is entirely formalisable in an impredicative constructive type theory a reduction-free normalisation algorithm can be extracted from this. The proof is presented as the construction of a model of the calculus inside a category of presheaves. Its definition is given entirely in terms of the internal language.

**Available**:- Postscript (109KB,comp) DVI-File (37KB,comp) BibTeX Entry

* Proceedings of Category Theory and Computer Science 95, pages 182-199
*

We present a categorical construction of a normalisation function for the simply type lambda calculus which does not use term rewriting. The construction uses a variation of glueing for presheaf categories.

**Available**:- Postscript (71KB,comp) BibTeX Entry

* Proceedings of the worskhop Types for Proofs and Programs 94, pages 3-18
*

We present an extendible strong normalisation proof for the Calculus of Constructions by modifying the standard realizability semantics based on omega sets. This construction also works for extension of the calculus which introduce real dependency.

**Available**:- Postscript (100KB,comp) DVI-File (35KB,comp) BibTeX Entry

* User manual for the ALF system
*

ALF ("Another Logical Framework") is a structure editor for Martin-Löf's monomorphic type theory; i.e. it ensures that the constructed objects are wellformed and welltyped. It can be used for the development of proofs and programs and for the integrated verification of functional programs. ALF emphasizes the interactive development of type-theoretic constructions, i.e. proof objects and programs, using a window-based user interface. Thus ALF supports an arbitrary mixture of top-down and bottom-up development.

**Available**:- Postscript (164KB,comp) BibTeX Entry

* PhD thesis, University of Edinburgh, 1993
*

This thesis contains an investigation of Coquand's Calculus of Constructions, a basic impredicative Type Theory. We review syntactic properties of the calculus, in particular decidability of equality and type-checking, based on the equality-as-judgement presentation. We present a set-theoretic notion of model, CC-structures, and use this to give a new strong normalization proof based on a modification of the realizability interpretation. An extension of the core calculus by inductive types is investigated and we show, using the example of infinite trees, how the realizability semantics and the strong normalization argument can be extended to non-algebraic inductive types. We emphasize that our interpretation is sound for large eliminations, e.g. allows the definition of sets by recursion. Finally we apply the extended calculus to a non-trivial problem: the formalization of the strong normalization argument for Girard's System F. This formal proof has been developed and checked using the LEGO system, which has been implemented by Randy Pollack. We include the LEGO files in the appendix.

**Available**:- Postscript (573KB,comp) DVI-File (204KB,comp) BibTeX Entry

* Proceedings of Typed Lambda Calculi and Applications 93, pages 13 - 28
*

We describe a complete formalization of a strong normalization proof for the Curry style presentation of System F in LEGO. The underlying type theory is the Calculus of Constructions enriched by inductive types. The proof follows Girard et al "Proofs and Types, i.e. we use the notion of candidates of reducibility, but we make essential use of general inductive types to simplify the presentation. We discuss extensions and variations of the proof: the extraction of a normalization function, the use of saturated sets instead of candidates, and the extension to a Church Style presentation. We conclude with some general observations about Computer Aided Formal Reasoning.

**Available**:- Postscript (65KB,comp) DVI-File (26KB,comp) BibTeX Entry

Home Page TCS Computer Science Institute University

Don Feb 1 14:07:42 CET 2001