Bachelor Theses


Cubint - an interpreter for typed lambda calculi

Cubint is an interpreter for typed lambda calculi to be used for educational purposes. It offers typing modes for the simply types lambda calculus, System F, F-omega and the Calculus of constructions. The underlying theorie is the Lambda-Cube. There are various extensions integrated into its uniform syntax. So Cubint offers numbers, booleans, unit, records, variants, iso-recursive types, a fix point combinator and references. The type system of Cubint ensures that the extensions do not conflict with the usual definition of S, F and Fw.
Additionally a simple form of subtyping can be enabled in S, F, Fw and CC and there are two modes R and RG that offer type reconstruction for a restricted calculus in ML-like style.


Linux archive with source code, test files and documentation Windows archiv with source code, test files and documentation


There are three possibilities to learn more about Cubint.
  1. Look at the user guide (html) or userguide.pdf .
  2. Have a look at the example library
  3. Read the final report (pdf version, written in german) for further information about the type system and architecture.

Christian Müller, 03.12.2004