Completed Projects

Below 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.

Fomega - Type Checker for Curry-style System F_ω

Web page:	http://www.cse.chalmers.se/~abela/fomega/
Theory:	System F_ω
Implementation:	OCaml 3.06
Platform:	portable
Author:	Andreas Abel

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.

Related Projects

B. Pierce's fomega: Church-style type checker (no longer supported)
C. Raffalli's type checkers for System F^η

church - Type Checker for Church-style System F_ω

Web page:	http://www.cse.chalmers.se/~abela/church/
Theory:	System F_ω
Implementation:	Haskell 98
Platform:	Linux, Windows
Authors:	Jan Peter Gutzmann, Andreas Abel and Klaus Aehlig

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 - Tutorial Proof Checker

Web page:	http://www.cse.chalmers.se/~abela/tutch/
Theory:	Intuitionistic Logic, Heyting Arithmetic
Implementation:	Standard ML of New Jersey, Version 110
Platform:	Linux (portable)
Authors:	Andreas Abel and Frank Pfenning

tutch is a proof CHecker for TUTorial purposes. It is based on intutionistic logic and supports the following proof forms:

natural deduction (ND) proofs
ND proofs annotated with proof terms
proof terms

...and the following theories:

intuitionistic and classical propositional logic
intuitionistic pure first-order logic
Heyting Arithmetic (booleans, natural numbers, lists)

Publication on tutch

Human-Readable Machine-Verifiable Proofs for Teaching Constructive Logic: Andreas Abel, Bor-Yuh Evan Chang and Frank Pfenning
Proof Transformations, Proof Presentations and Complexity of Proofs (PTP-01). Workshop Proceedings.

foetus - Termination Checker for Functional Programs

Web page:	http://www.cse.chalmers.se/~abela/foetus/
Theory:	lambda-calculus with inductive datatypes
Platform:	Web, Linux, ...
Implementation:	Standard ML of New Jersey 1997
Authors:	Andreas Abel and Thorsten Altenkirch

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

A Predicative Analysis of Structural Recursion: Andreas Abel and Thorsten Altenkirch (2002)
Journal of Functional Programming 12(1):1-41. ©Cambridge University Press
.pdf .ps.gz .dvi .bib
Specification and Verification of a Formal System for Structurally Recursive Functions: Andreas Abel (2000)
Types for Proofs and Programs, International Workshop, TYPES '99
Lökeberg, Sweden, June 1999. LNCS 1956. ©Springer-Verlag
.pdf .ps.gz .dvi .bib
A Semantic Analysis of Structural Recursion: Andreas Abel (1999)
Diploma Thesis, Ludwig-Maximilians-University, Munich.
.pdf .ps.gz .dvi .bib
foetus - Termination Checker for Simple Functional Programs: Andreas Abel (1998)
Implementation and Documentation.
.pdf .ps.gz .dvi .bib
Executable web version

Andreas Abel, http://www.cse.chalmers.se/~abela
Last modified: 2019-01-22 19:55>