Andreas Abel

LMU Informatik TCS

Termination and Guardedness Checking with Continuous Types

A type system is presented which provides syntax for approximations of

inductive datatype and thus incorporates a notion of relative size

of types. Typing rules force recursive functions to be

strongly normalizing while allowing them to be written in a natural

fashion known from functional programming. In the same way,

infinite objects like stream are ensured to be productive. Special

emphasis is on higher-order inductive and coinductive types (like

infinite trees) which require careful treatment. To give sound

typing rules, we develop a new notion of continuity. While the

focus is on proving strong normalization, also extensions like

lexicographic orderings and parametric polymorphism are sketched.

Ralph Matthes

LMU Informatik TCS

Recursion and Corecursion for Nested Datatypes

Inspired by initial algebras and final coalgebras in functor

categories, a notion of (co-)inductive constructors of rank 2 is

presented inside the framework of system F_omega of higher-order

impredicative polymorphism. Since the applicability to as wide a

range of nested datatypes as possible is intended, the issue of

monotonicity becomes delicate and the solution departs significantly

from the obvious approach. Many closure properties of these nested

datatypes could be established but, surprisingly, a diagonal

construction seems impossible. An explicit representation of

substitution for non-wellfounded term trees will show the usefulness

of corecursion as opposed to coiteration only.

Dirk Pattinson

LMU Informatik, PST

Canonical Models and Compactness for Coalgebraic Modal Logic

We investigate issues of definablilty and compactness for coalgebraic modal

logic. This neccessitates to generalise the so-called canonical model

constructiuon to coalgebras for an endofunctor. The validity of a

compactness theorem for coalgebraic modal logic then turns out to be

equivalent to the existence of a canonical model, which is compact in

a natural topology.

Felix Joachimski

LMU Mathematik

Standardization for the Coinductive Lambda-Calculus

Klaus Aehlig

LMU Mathematik

On Continuous Normalization

This work aims at explaining the syntactical properties of

continuous normalization, as introduced in proof theory by Mints and

further studied by Buchholz, Schwichtenberg and others.

In an extension of the untyped coinductive Lambda-calculus by

void constructors (so-called repetition rules), a primitive

recursive normalization function is defined. Compared with other

formulations of continuous normalization, this definition is much

simpler and therefore suitable for analysis in a coalgebraic

setting. It is shown to be continuous w.r.t. the natural topology

on non-wellfounded terms with the identity as modulus of continuity.

The number of repetition rules is locally related to the number of

beta-reductions necessary to reach and the number of applications

appearing in the normal form, as represented by the Böhm tree.

Laura Crosilla

LMU Mathematik

Constructive Set Theory with Urelements

In this talk we shall consider constructive set theories (in the

sense of Aczel [Ac78]) with the addition of urelements. Roughly

speaking, urelements are primitives which are not sets but can be

used in the formation of sets. Urelements were an integral part of

the subject in the early days of set theory, at least in the work of

Zermelo. In recent years a particularly strong support for

urelements has come through the work of J. Barwise, who has claimed

for their naturalness in the development of the theory of admissible

sets [Ba75]. More recently Barwise has asserted the usefulness

of urelements in the frame of non-well-founded sets (see for example

[Bamo96]).

It is plausible that also in a constructive setting one could take

the move of eliminating the urelements, for example by `modeling'

them in the universe of pure sets as suggested in [Ac88].

Nonetheless, we here aim at a constructive set theory with

non-well-founded sets which is suitable for an implementation in a

theorem prover. In this context it seems preferable to consider

urelements as primitives.

We assume that an integral part of the devising of a new

constructive set theory a la Aczel is the formulation of a natural

extension of Aczel's interpretation of constructive set theory in

Martin Löf Type theory [Ac78], as through this interpretation

the notion of set gains its constructive meaning. Therefore the

addition of urelements will have to be accompanied with an

appropriate extension of Aczel's interpretation in Martin Löf type

theory.

We shall present some work in progress on this Themes.

[Ac78] P. Aczel: The Type Theoretic Interpretation of

Constructive Set Theory, in: A. MacIntyre, L. Pacholski, J. Paris

(eds.), Logic Colloquium '77 (North-Holland, Amsterdam, 1978).

[Ac88] P. Aczel: Non-well-founded sets, CSLI Lecture Notes

14 (Stanford 1988).

[ba75] J. Barwise: Admissible sets and structures.

An approach to definability theory,

(Springer Verlag, Berlin, 1975).

[Bamo96] J. Barwise, L.Moss: Vicious Circles

CSLI Lecture Notes 60 (Stanford 1996).

Martin Kübler

LMU Mathematik

Unifikation und Fallunterscheidung

Es wird das Zusammenspiel von Unifikation und Fallunterscheidung im

einfach getypten Lambdakalkül untersucht. Insbesondere wird gezeigt,

dass in einem Lambdakalkül mit Fallunterscheidung keine endlichen,

vollständigen Mengen von Unifikatoren existieren

können. Desweiteren wird demonstriert, wie man Fallunterscheidung

zur Konstruktion allgemeinster Unifikatoren benutzen kann. Hierbei

werden lineare Terme betrachtet, die eine nützliche Erweiterung der

Muster von Dale Miller darstellen.

Favio Miranda-Perea

LMU Informatik TCS

A Curry-style Realizability Interpretation for Monotone Inductive

Definitions

We present a logical system of monotone inductive definitions and

prove the soundness of a realizability interpretation in the style

of Krivine, where the realizers are terms of a Curry-style system of

lambda-calculus.