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


[ Home | CV | Projects | Publications | Talks | Teaching | Sharing ]

Valid HTML 4.01! Andreas Abel, http://www.cse.chalmers.se/~abela
Last modified: Mon Dec 15 19:00:53 CET 2008
Valid CSS!