Bachelor Theses
Aufgabenstellung
Verlauf
Cubint
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.
Downloads
Documentation
There are three possibilities to learn more
about Cubint.
- Look at the
user guide (html) or
userguide.pdf .
- Have a look at the
example library
- Read the
final report (pdf version, written in german) for further
information about the type system and architecture.
Christian Müller, 03.12.2004