Completed ProjectsBelow you find some implementations of lambda calculi and logics that are no longer actively developed.
Tutch is apparently used for teaching logics at some universities; email me if you find bugs.
Type-checking is easy for fully type-annotated (Church-style) terms of Girard's System Fω but undecidable for non-annotated (Curry-style) terms. Hence, the type checker we implemented is necessary incomplete. Nevertheless, it succeeds on most typical terms occurring in Fω programs and has proven to be a practical tool for my own purposes.
This type checker does the (rather) simple job of checking fully annotated lambda-terms of System Fω. It is envisioned as a double-checking backend to the Fomega checker (see above).
tutch is a proof CHecker for TUTorial purposes. It is based on intutionistic logic and supports the following proof forms:
Publication on tutch
foetus is a type-theoretic functional programming language, a simplification of MuTTI (Munich Type Theory Implementation), designed to investigate termination checking of recursive functions. An implementation of the termination checker has been carried out in 1997/1998 and is accessible via the WWW. In my diploma thesis (1999), I proved wellfoundedness of the structural term ordering used in foetus. A predicative version (in the sense of Martin-Löf's type theory) of the proof appeared in the Journal of Functional Programming (2002) and a soundness proof of the static analysis algorithm of foetus has been published in the proceedings of TYPES'99.
Drafts and Publications on foetus
[ Home | CV | Professional Service | Projects | Publications | Talks | Teaching | Supervision ]