Lehr- und Forschungseinheit für Theoretische Informatik,
Institut für Informatik der Ludwig-Maximilians-Universität München

Abstracts of Selected Publications

Thorsten Altenkirch

1999

Extensional Equality in Intensional Type Theory

Thorsten Altenkirch

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

Monadic presentations of lambda terms using generalized inductive types

Thorsten Altenkirch and Bernhard Reus

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

Types for Proofs and Programs (TYPES '98)

Thorsten Altenkirch, Wolfgang Naraschewski and Bernhard Reus (Eds.)

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

1998

Logical relations and inductive/coinductive types

Thorsten Altenkirch

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

1997

Reduction-free normalisation for system F

Thorsten Altenkirch, Martin Hofmann, Thomas Streicher

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

1996

Integrated Verification in Type Theory

Thorsten Altenkirch

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

Reduction-free normalisation for a polymorphic system

Thorsten Altenkirch, Martin Hofmann, Thomas Streicher

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

1995

Categorical reconstruction of a reduction free normalization proof

Thorsten Altenkirch, Martin Hofmann, Thomas Streicher

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

1994

Proving Strong Normalization of CC by Modifying Realizability Semantics

Thorsten Altenkirch

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

A user's guide to ALF

Thorsten Altenkirch, Veronica Gaspes, Bengt Nordstr"om and Bj"orn von Sydow

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

1993

Constructions, Inductive Types and Strong Normalization

Thorsten Altenkirch

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

A Formalization of the Strong Normalization Proof for System F in LEGO

Thorsten Altenkirch

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
Rolf Backofen
Don Feb 1 14:07:42 CET 2001