Lambda-Kalkül-und-Typen-Club

Wintersemester 2001/02

Freitag, 8. Februar
Peter Schuster
From Spectra to Sheaves in Formal Topology
Freitag, 1. Februar
Frédéric Blanqui
Type Theory and Rewriting, Part II (Part I is presented in the Colloquium of the GKLI)
Freitag, 25. Januar
Tarmo Uustalu
CPS translating inductive and coinductive types
Freitag, 18. Januar
Thorsten Altenkirch
Normalization by evaluation for typed lambda calculus with coproducts
Freitag, 11. Januar
Jan Jürjens
Bridging the gap: Formal vs. complexity-theoretical reasoning about cryptography
Freitag, 7. Dezember
Andreas Abel
Termination and Guardedness Checking with Types
Freitag, 30. November
Peter Schuster
Apartness as a Constructive Road to Topology
Freitag, 23. November
Felix Joachimski
Syntactic Analysis of Eta-Expansions in Pure Type Systems
Freitag, 16. November
Michal Konecny
Continuity of non-extensional computation in TTE
Freitag, 9. November
Stefan Berghofer
Beweisterme für Isabelle
Freitag, 2. November
Markus Wenzel
Isabelle/Isar - Eine Umgebung zur Entwicklung formaler Beweis-Dokumente
Freitag, 19. Oktober
Semestereröffnung mit dem neuen Lehrstuhlinhaber Martin Hofmann

Sommersemester 2001

Freitag, 22. Juni
Wilfried Buchholz
Anmerkungen zu einem Artikel von Th.Altenkirch und Th.Coquand
Freitag, 15. Juni
Felix Joachimski
Standardization for PIE^co-systems or: Enjoying notations for reduction
Freitag, 25. Mai
informelle Diskussion zur Koiteration über Koterme, zur Koiteration über der Eins und zur Koiteration von Rang 2
Freitag, 18. Mai
Tarmo Uustalu
Recursion schemes from comonads
Freitag, 11. Mai
Berichte von der Konferenz TLCA 2001, Semesterplanung

Wintersemester 2000/01

Freitag, 19. Januar
Stefan Berghofer
Induktive Typen in Isabelle/HOL
Freitag, 12. Januar
Ralph Matthes
Chris Okasaki's adventure in types
Freitag, 22. Dezember
entfällt wegen der Arbeitstagung Bern-München am 21. und 22. Dezember
Freitag, 15. Dezember
entfällt zugunsten eines Vortrags von Michael Möllerfeld (HS133, Theresienstraße)
Freitag, 8.Dezember
Second-Order Pre-Logical Relations and Representation Independence, 2. Teil
Freitag, 24. November
Ralph Matthes
Hereditarily monotone inductive constructors of finite kind
Freitag, 17. November
Hans Leiß
Second-Order Pre-Logical Relations and Representation Independence
Freitag, 10. November
Peter Hancock
"Positions" in wellfounded and non-wellfounded objects
Freitag, 3. November
Parigots Lambda-Mu-Kalkül und induktive Typen, 2. Teil
Freitag, 27. Oktober
Es wird empfohlen, die Tagung über Intensionalität zu besuchen.
Freitag, 20. Oktober
Ralph Matthes
Parigots Lambda-Mu-Kalkül und induktive Typen

Weiter zurückliegende Themen und Vorträge (unvollständig)


Winter term 98/99

26.2.99, 14:15, Raum Z1.09, Oettingenstr.
Andreas Abel
A semantical analysis of structural recursion
19.2.99, 14:15, Raum Z1.09, Oettingenstr.
Bernhard Reus
Fortsetzung: Einführung in die formale Topologie
oder Topologia formale alla Padova
12.2.99, 14:15, Raum Z1.09, Oettingenstr.
Peter Schuster
Can choice principles really be constructive?
5.2.99, 14:15, Raum Z1.09, Oettingenstr.
Bernhard Reus
Einführung in die formale Topologie
oder Topologia formale alla Padova
18.12.98, 14:15, Raum 0.37, Oettingenstr. (gemeinsam mit Oberseminar PST)
Thomas Streicher
Full abstraction via realizability
11.12.98, 14:15, Raum Z1.09, Oettingenstr.
Thorsten Altenkirch
Extensional Equality in Intensional Type Theory
20.11.98, 15:15, Raum Z1.09, Oettingenstr.
Monika Seisenberger
Higmans Lemma in MINLOG

Before October 98


Deepak Kapur (SUNY at Albany)

Mechanizing Reasoning about Regular Data Structures

(Joint GKLI/Lambda-Kalkül-und-Typen-Club Seminar)
Freitag, den 3.7.98, 14:00-15:00, TUM, Südbau, S2229

An algebraic method for specifying regular and semantic data structures including complete binary trees, sorted lists, square matrices, powerlists, is proposed. It is shown that this method generalizes the equational approach to specifying data types. The specification method allows constructors of a data type to be partial in the sense that their behavior may be meaningful only on a subset of syntactically specified input domain. Equational and inductive reasoning techniques based on rewrite rules can be generalized to exploit this information about constructors. The use and effectiveness of this approach are illustrated with parallel algorithms and hardware circuit descriptions using Misra's powerlists. Properties of such algorithms can be verified using the theorem prover Rewrite Rule Laboratory (RRL). Machine proofs generated preserve the clarity and succinctness, to a large extent, of a hand proof.


Thorsten Altenkirch

Ralph Loader: Equational Theories for Inductive Types (2.Teil)

Freitag, den 26.06.98, 16:15-17:15, Oettingenstr. 67, Raum Z1.09

Fortsetzung vom 29.5. Neueinsteiger willkommen !

Fortsetzung voraussichtlich am 17.7.


Healfdene Goguen (University of Edinburgh)

Structural Properties in Type Theory

Freitag, den 19.06.98, 16:15-17:15, Oettingenstr. 67, Raum Z1.09
(Joint GKLI/Lambda-Kalkül-und-Typen-Club Seminar)

Structural properties of type theory, such as weakening and substitution, are traditionally verified individually by induction on derivations. In this talk we present a simple model construction that allows most of the interesting structural properties to be shown at once.


Andreas Abel

foetus - Termination Checker for Simple Functional Programs

Montag, den 15.6.98, 16:15-17:15, Oettingenstr. 67, Raum Z1.09

First, we briefly introduce a simple functional language "foetus" (lambda calculus with tupels, constructors and pattern matching), for which we have implemented a termination checker.

This checker tries to find a well-founded structural order on the parameters for a given function. The components of the check algorithm are: function call extraction out of the program text, call graph completion and finding a lexical order for the function parameters.

We hope to be able to demonstrate "foetus" in action using a video beamer.

A draft version of the description can be found here.


Thorsten Altenkirch

Ralph Loader: Equational Theories for Inductive Types

Freitag, den 29.05.98, 16:15-17:15, Oettingenstr. 67, Raum Z1.09

Wie schon im Februar besprochen, wenden wir uns nun Loader's Papier zu, in dem er eine Form des Kreisel-Lacombe-Schönfield Theorems benutzt, um zu zeigen, daß das PER Modell für einen lambda-Kalkül mit strikt positiven Typen voll abstrakt ist.

Besonders interessant ist, daß die Frage, ob das PER Modell für System F voll abstrakt ist, noch offen ist. Eine andere (bescheidenere) Frage ist, ob sich Loader's Resultat auch mit Ulrich Berger's Ansatz beweisen läßt.

Es ist empfehlenswert, vorher einen Blick auf das Papier zu werfen.

Der Vortrag wird voraussichtlich am 25.6. fortgesetzt.


Markus Wenzel
(TU München)

Extensible records with structural subtyping in Church's Simple Type Theory (HOL)

(Joint work with Wolfgang Naraschewski)
Freitag, den 08.05.98, 16:15-17:15, Oettingenstr. 67, Raum Z1.09

We show how extensible records with structural subtyping can be represented directly in Church's Simple Type Theory (also known as HOL). Exploiting some specific properties of HOL, in particular the Isabelle/HOL dialect, this encoding turns out to be extremely simple. Structural subtyping is subsumed by naive parametric polymorphism, while overridable generic functions ('methods' in object-oriented parlance) may be based on ordinary overloading.

This talk aims at giving an understanding of *why* record subtyping actually works in HOL. We will point out special features (peculiarities?) of HOL that are absent in other type theories. We will also hint at the general lessons learned from this example of doing applied logic in the context of a real working environment like Isabelle.

Wolfgang Naraschewski and Markus Wenzel. Object-Oriented Verification based on Record Subtyping in Higher-Order Logic. To appear on TPHOLs'98.

Diskussion (Totalität und Domains)

Freitag, 20.2.98, 16:15-17:15, Oettingenstr. 67, Raum Z1.09

Wie versprochen, wollen wir Fragen und Ideen, die zu Uli Berger's Vortrag am 6.2. aufgetaucht sind, diskutieren

Uli kann den Satz, daß die Elemente von Realizability Modellen genau die totalen Elemente des Domainmodells sind, erläutern.

Als Fortsetzung schlage ich vor gemeinsam Ralph Loader's Papier Equational Theories for Inductive Types zu lesen und zu verstehen. Loader zeigt hier eine interessante Anwendung eines (etwas anderen) Totalitätsbegriffs: Für strikt positive induktive Typen ist die Theorie des PER Modells minimal. Die Erweiterung für System F steht noch aus.


Thorsten Altenkirch

Von Adäquatheit zur Normalisierung

Freitag, 13.2.98, 16:15-17:15, Oettingenstr. 67, Raum Z1.09

Ich werde an zwei Beispielen zeigen, wie man aus konstruktiven Adäquatheitsresultaten (= Korrektheit + Vollständigkeit) Normalisierungsresultate ablesen kann:

  1. Kripke Modelle für minimale intuitionistische Aussagenlogik
  2. Eine Variante von Beth Modellen für die volle intuitionistische Aussagenlogik

1. ist Folklore, 2. vermutlich weniger bekannt. Die Erweiterung für die Prädikatenlogik scheint unproblematisch. Um Entscheidbarkeitsresultate für Lambda-Kalküle abzuleiten, ist die Verwendung von kategoriellen Modellen sinnvoll (nämlich Prägarben, bzw. Garben): Für 1. wurde das in unserem CTCS-Artikel getan, 2. ist noch in Arbeit.


Ulrich Berger

Der Totalit"atsbegriff f"ur Funktionale h"oheren Typs

Freitag, 6.2.98, 16:15-17:15, Oettingenstr. 67, Raum Z1.09
Die Bereichstheorie nach Scott und Ershov erm"oglicht einen eleganten
Zugang zu einer konstruktiven mengentheoretischen Modellierung von
Funktionalen h"oheren Typs. Man definiert zun"achst Bereiche von
partiellen Funktionalen, um daraus dann die totalen Funktionale, an
denen man eigentlich interessiert ist, auszusondern. Diese totalen
Objekte besitzen gewisse ordnungstheoretische bzw. topologische
Eigenschaften (Dichtheit, Codichtheit), mit deren Hilfe man zum
Beispiel ein konstruktives Auswahlprinzip sowie die Isomorphie zu
Beesons Realisierbarkeitsmodell zeigen kann.  Der Nachweis dieser
Eigenschaften gelingt mittels einer Verallgemeinerung des
Dichtheitssatz von Kleene und Kreisel, der besagt, dass die "ublichen
Typkonstruktoren x, ->, Pi und Sigma, aber auch Universums- und
Superuniversumsoperatoren die Dichtheit und die Codichtheit vererben.
Im Vortrag werde ich die Definitionen von Dichtheit und Codichtheit
insbesondere f"ur abh"angige Typen erl"autern und den Beweis des
Satzes skizzieren.
    

Ralph Matthes

A MODULAR proof of strong normalization for permutative conversions in lambda calculus

Freitag, 30.1.98, 16:15-17:15, Oettingenstr. 67, Raum Z1.09
Adding coproducts to lambda calculus destroys the subformula property
for normal forms w.r.t. beta reduction. This problem may be
operationally resolved by adding permutative conversions.
The aim of this talk is to convince the audience that adding
permutative conversions to a lambda calculus with coproducts
(i.e. sums of types) does preserve strong normalization. The proof
will be shown for the simplest case where only arrow and sum types are
assumed to be present in the system. Felix Joachimski has given a
proof for this system back in 1995 which rests on this restriction. 
In contrast to this the proof to be presented is modular in the sense
that a proof by the computability predicate method due to Tait only
has to be adjusted by some minor changes in the definition of
candidates (i.e. saturated sets). They only necessitate local changes
in the reasoning and hence allow for a much richer set of type
constructs to be studied (e.g. universal and existential
quantification and inductive types) without having to rework the proof
parts covering those extensions. 
The talk is also intended to advocate the use of (general) inductive
definitions for constructing normalization proofs.
    

Alexander Kurz

Specifying Coalgebras with Modal Logic

Freitag, 16.1.98, 16:15-17:15, Oettingenstr. 67, Raum Z1.09
  We propose to use modal logic as a logic for coalgebras and discuss it in
  view of the work done on coalgebras as a semantics of object-oriented
  programming. Two approaches are taken: First, standard concepts of modal
  logic are applied to coalgebras. For a certain kind of functor it is shown
  that the logic exactly captures the notion of bisimulation and a complete
  calculus is given. Second, we discuss the relationship of this approach with
  coalgebraic logic.
    

Martin Strecker (Universität Ulm)

Beweisverfahren in Typentheorie

Freitag, 18.7.97, 16:15-17:15, Oettingenstr. 67, Raum Z1.09
Dieser Vortrag besch"aftigt sich mit interaktiver Beweisf"uhrung in
Typentheorien und mit Methoden, Beweise in bestimmten Fragmenten zu
automatisieren.

H"aufig werden beim Beweisen in Typentheorie als Platzhalter f"ur zu
konstruierende Objekte Metavariablen eingef"uhrt. Es ist fraglich, wie
Termoperationen wie Substitution und Reduktion in einem Kalk"ul mit
Metavariablen zu definieren sind. Die Probleme eines naiven Ansatzes
werden diskutiert, zu ihrer L"osung wird ein Kalk"ul mit expliziten
Substitutionen vorgeschlagen und dessen Eigenschaften werden
analysiert.

Ein derartiger Kalk"ul eignet sich zur interaktiven Beweisf"uhrung. Es soll
weiterhin untersucht werden, wie Beweissuche in (Fragmenten der)
Typentheorie durchgef"uhrt werden kann und wie bestimmte Anforderungen
(z.B. Variablenbedingungen in einem Sequenzen-Kalk"ul) in diesem Rahmen
interpretiert werden k"onnen.

Abschlie"send wird das Typelab-System vorgestellt, in dem einige der
vorgeschlagenen Konzepte implementiert sind.

Folien des Vortrages


Hans Leiss (CIS,LMU):

Haupttypen und Hauptbeweise in verschiedenen Typsystemen

Freitag, 20.6.97, 16:15-17:15, Oettingenstr. 67, Raum Z1.09
Es geht insbesondere darum, die Beweise von

- Haupttypisierungen im Curry-Hindley Kalk"ul ~=~ allgemeinste Unifikatoren
- Haupttypisierungen im Damas-Milner Kalk"ul  ~=~ allgemeinste     ??
- Haupttypisierungen im Milner-Mycroft Kalk"ul ~=~ allgem. Semiunifikatoren
-  ?? bei Milner-Mycroft + polym. Abstraktion  ~=~ allgem. Semiunifikatoren

zu diskutieren/vergleichen und zu vereinheitlichen.
    

John N Crossley
(Professor of Logic;Monash University;Australia):
Real programs from real proofs

Freitag, 23.5.97, 16:15-17:15, Oettingenstr. 67, Raum Z1.09
The main aim of the project is to be able to take a mathematics book and,
with a minimum of human interaction, produce correct programs from
the proofs in the book.

There are two aspects:1. technical and 2. psychological.

For the technical aspect we use a typed lambda calculus and
the Curry-Howard correspondence to code proofs.

For the psychological one we are interested in how people
construct proofs. 

(The project is not interested in theorem-proving as such:
we assume that we already have some sort of proof. The questions
are more about we get the machine to comprehend the proof.)

Stefan Merz:
Das Typsystem ML<

Freitag, 25.4.97, 16:15-17:15, Oettingenstr. 67, Raum Z1.09
ML< erweitert das klassische ML- (Hindley-Milner-) Typsystem um eine partielle
Ordnung auf atomaren Typen. Im allgemeinen hat ein ML<-Typ die Gestalt

            \forall v1...vn : k . m

fuer Variablen vi, eine Konjunktion k von Ungleichungen zwischen Monotypen
("constraint") und einem Monotyp m. Damit eignet sich ML< gut als Typsystem
fuer (funktionale) objektorientierte Sprachen, die parametrische Polymorphie a
la ML und dynamische Bindung (Polymorphie im objektorientierten Sinn) mischen.

Im Gegensatz zu ML ist die Aequivalenz zweier ML<-Typen nicht auf alpha-
Konvertierbarkeit zurueckzufuehren. Wir fuehren daher eine "semantisch"
motivierte partielle Ordnung (und Aequivalenz) auf Typen ein und formalisieren
diese durch eine geeignete Implikation von constraints.

Im Vortrag wird neben dem reinen Typsystem exemplarisch seine Anwendung auf
eine explizit getypte Sprache beschrieben, die wie CLOS oder Cecil auf
(hoeherstufigen) Multimethoden basiert, d.h. die dynamische Bindung bezieht
sich nicht nur auf ein ausgezeichnetes Empfaengerobjekt, sondern
beruecksichtigt alle Argumente. (Damit erhaelt man eine natuerliche
Verallgemeinerung sowohl funktionaler als auch objektorientierter Konzepte.)
Im Gegensatz zu der in der Literatur gebraeuchlicheren Codierung von Objekten
als records geben wir eine Interpretation von ML-Datentypdeklarationen als
Deklarationen von (abstrakten und konkreten) Objektklassen und von pattern
matching als dynamischer Bindung. Da Typen nur die Schnittstelle von Objekten
beschreiben, werden Implementierungsaspekte wie Vererbung und Verkapselung
nicht im Typsystem beschrieben, was existentielle bzw. rekursive Typen
ueberfluessig macht, sondern durch ein klassisches Modulsystem gewaehrleistet.

Wilfried Buchholz:
Zur Beweistheorie iterierter induktiver Definitionen

Freitag, 14.3.97, 16:15-17:15, Oettingenstr. 67, Raum Z1.09
Freitag, 11.4.97, 16:15-17:15, Oettingenstr. 67, Raum Z1.09
Es wird eine beweistheoretische Reduktion der klassischen Theorie ID^c_\nu
(\nu<\omega) auf eine konstruktiv akzeptable Theorie ID^i_\nu({\cal A})
mit strikt-positiver Definitionsklausel {\cal A} gegeben. 
Als Korollar erh\"alt man, dass in ID^i_\nu({\cal A}) dieselben
rekursiven Funktionen beweisbar total sind, wie in  ID^c_\nu.
Spezielle Hilfsmittel bei der Reduktion sind eine besondere 
Realisierbarkeitsinterpretation, sowie eine infinit"are
Schlussregel (\Omega_{\mu+1}) mit (in gewissem Sinn) "uberabz"ahlbar
vielen Pr"amissen.
      
Folien

Felix Joachimski:
Eta expansion

Freitag, 7.3.97, 16:15-17:15, Oettingenstr. 67, Raum Z1.09
  Using a canonical $\eta$-expansion-function the problem of strong
  normalisation and confluence of combined $\beta$-reduction and
  $\eta$-expansion is reduced to strong normalisation and confluence of
  the $\lambda$-calculus with $\beta$-reduction only. The universality
  of the method is demonstrated by applying it to 
  \begin{itemize}
    \item A simply typed $\lambda$-calculus with surjective pairing and sum
      types. To provide the premise of the method we also give an improved
      strong normalisation proof for $\beta$ plus permutative conversions that
      also allows to treat $\eta$-contractions elegantly.
    \item Arbitrary singly-sorted $\beta$-strongly-normalising pure type
      systems, including the systems $\FFF$, $\FFF^{\omega}$ and the
      calculus of constructions.
  \end{itemize}
      
Folien

Martin Hofmann:
Zur Konservativität der Gleichheitsreflexion in Martin-Löf's Typentheorie

Freitag, 31.1.97, 16:15-17:15, Oettingenstr. 67, Raum Z1.09
In Martin-Loef's intensionaler Typentheorie (ITT) unterscheidet man zwischen
der entscheidbaren *Urteilsgleichheit* und der unentscheidbaren,
beweisbeduerftigen *propositionalen Gleichheit* ausgedrueckt durch den
Identitaetstyp. So hat man z.B. in ITT die Urteilsgleichheit
1+3 = 2+2, und damit auch refl : Id(1+3,2+2), weil refl :
Id(1+3,1+3) und Id(1+3,1+3)=Id(1+3,2+2). Auf der anderen Seite gilt
z.B. nicht (x+y)(x-y)=x^2+y^2, wohl aber kann man (unter Verwendung
des Rekursionsoperators) Term t(x,y) konstruieren, mit

t(x,y) : Id((x+y)(x-y) , x^2+y^2)

In der extensionalen Typentheorie (ETT) hat man nun die
*Gleichheitsreflexionsregel*, welche es gestattet, aus p:Id(t1,t2) fuer
ein p schon t1=t2 zu folgern. Dadurch wird die Urteilsgleichheit
unentscheidbar; der (moeglicherweise komplizierte) Beweisterm p faellt
ja weg. Dies zieht aber auch die Unentscheidbarkeit aller anderen
Urteile, wie Typisierung und Typ-heit nach sich. 

Im Vortrag moechte ich zeigen, dass die Gleichheitsreflexionsregel
konservativ ist ueber einer  Erweiterung von ITT um zwei natuerliche
Axiome. Ich werde auch  moegliche Anwendungen dieses Resultats auf
computerunterstuetztes Beweisen in ITT diskutieren. 

Der groesste Teil des Vortrages stuetzt sich auf  meinen Artikel.Ich
hoffe allerdings, dass es mir bis zum 31.1. gelungen sein wird, das
Resultat auf eine Praesentierung von ITT mit Hilfe eines "logical
framework" zu erweitern und damit ein in op. cit. offen gelassenes
Problem zu loesen.

Bericht vom Annual Types workshop in Aussois

Freitag, 17.1.97, 16:15-17:15, Oettingenstr. 67, Raum Z1.09

Vom 15.12.-19.12.96 fand in Aussois der erste jährliche workshop der TYPES working group statt. Thorsten Altenkirch, Bernhard Reus und Wolfgang Naraschewski (evtl.) werden darüber berichten ( Programm des workshops (vorläufige Version) ).

Außerdem wollen wir die Ergebnisse der brainstorming session in konkrete Planung umsetzen.


Thorsten Altenkirch:
MuTTI - ein Experiment zur Implementation von Typtheorie

Freitag, 6.12.96, 16:15-17:15, Oettingenstr. 67, Raum Z1.09

MuTTI = Munich Type Theory Implementation ist eine experimentelle Implementation von Typtheorie am Lehrstuhl Clote. Das MuTTI System basiert auf der Sicht von Typtheorie als funktionaler Programmiersprache und realisiert einige Idee aus gemeinsamer Arbeit mit Thierry Coquand.


Open Problem Session

Fr, 29.11.96, 16:15 - 17:15, Oettingenstr. 67, Raum Z1.09

Für das nächste Treffen ist kein Thema festgelegt und ich habe vor eine "Open Problem Session" zu machen, wo jeder etwas über seine gegenwärtigen (oder zukünftigen) Interessen erzählen kann. Dabei werden wir hoffentlich auch einige Themen identifizieren, mit denen sich der Club in der nächsten Zukunft (also ab Anfang '97) beschäftigen soll.

Resultate des Brainstormings

Hans Leiß:
Milner-Style Type Inference for SML with Polymorphic Recursion

Di 5.11.96, 16:30-18:00, Oettingenstr. 67, Raum Z1.09
Fortsetzung: Di 19.11.96, 16:30-18:00, gleicher Ort

Es wird eine Erweiterung der SML-Typisierung um polymorphe Rekursion vorgestellt. Diese 'ML+'-Typisierbarkeit umfasst ML-Typisierbarkeit echt, sowohl was die Menge der typisierbaren Terme als auch was die Allgemeinheit der Haupttypen angeht. Dass sie im allgemeinen unentscheidbar ist, macht sich praktisch (bisher) nicht bemerkbar.

Bei der Typisierung mit ML+ besteht -im Unterschied zu ML- das Problem, die Quantorenstruktur von Typen (auch in den Annahmen!) zu finden. Das kann man entweder im Curry/Hindley-Stil durch Aufstellen und Loesen geeigneter (nicht lokaler) TypUNgleichungen zu einem Term erreichen, oder im sequentiellen Milner-Stil, mit Spezialisierung von Teilherleitungen (wie fuer ML in SML-Compilern ueblich).

Zur Konstruktion allgemeinster Typherleitungen braucht man fuer ML+ kompliziertere Beweisspezialisierungen als fuer ML, insbesondere den Umgang mit unbekannten quantifizierten Typannahmen und deren geeignete Abschwaechung.


Maintained by Thorsten Altenkirch until August 2000, since then by Ralph Matthes
Last modified: Tue Oct 8 13:39:19 CEST 2002