# 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/ System Fω OCaml 3.06 portable 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/ System Fω Haskell 98 Linux, Windows 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/ Intuitionistic Logic, Heyting Arithmetic Standard ML of New Jersey, Version 110 Linux (portable) 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/ lambda-calculus with inductive datatypes Web, Linux, ... Standard ML of New Jersey 1997 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

[ Home | CV | Professional Service | Projects | Publications | Talks | Teaching | Supervision ]