Bachelor Theses
Aufgabenstellung
Verlauf
Cubint
Fortgeschrittenenpraktikum:
Interpreter für getypte Lambda-Kalküle
Christian Müller
Betreuer: Guido Tack, Prof. Gert Smolka
Motivation
Die theoretische Fundierung von Programmiersprachen gewinnt mit zunehmender
Komplexität der Programmiersysteme immer mehr an Bedeutung. Typsysteme
bieten die Möglichkeit zum Entwurf stabiler und sicherer Systeme. Der
Lambda-Cube von Barendregt stellt eine allgemeine Basis von getypten
Lambda-Kalkülen, die beim Entwurf von Programmiersprachen
interessant sind.
Unter Verlauf kann der
aktuelle Stand der Arbeit abgerufen werden.
Aufgabenstellung
Interpreter for Typed Lambda Calculi
The goal of this project is the design and the
implementation of an interpreter for typed lambda
calculi to be used for educational purposes. The
interpreter should offer different calculi, including S
(simply typed lambda calculus), F, F-omega, and the
Calculus of Constructions. The interpreter should
provide for non-recursive definitions. Iso-recursive
types and builtin integers should be available on
demand. The interpreter should be based on the
Lambda-Cube.
The criteria of success is not efficiency, but
elegance, compactness, modularity and educational
support. The interpreter should be useful for students
studying typed lambda calculi. It should come with an
explicitly defined internal language so that its parser
and pretty-printer can be reused for student projects.
As extra and challenge type reconstruction should be
addressed. This is easy for S but difficult for richer
calculi. Reconstruction of Prenex polymorphism as in
ML seems feasible. A more ambitious goal would be to
adapt the techniques of MLF, a extension of ML with
full F-polymorphism that has been investigated by Le
Botlan and Remy.
References
Benjamin C. Pierce, Types and Programming
Languages. The MIT Press, 2003.
Simon Peyton Jones and Erik Meijer, Henk: A typed
intermediate language. 1997.
Henk Barendregt and Herman Geuvers, Proof-checking
using Dependent Type Systems. Handbook of Artificial
Reasoning, Volume II, Ch. 18 (2001), 1149--1240.
Didier Le Botlan and Didier Rémy, MLF: Raising ML to
the Power of System F. Proceedings of the
International Conference on Functional Programming
(ICFP 2003), Uppsala, Sweden
Didier Le Botlan, MLF.
http://cristal.inria.fr/~lebotlan/mlf/mlf_eng.html
Ergebnis
Software und Abschlußbericht stehen unter
Cubint zum Download bereit.
Christian Müller, 03.04.2006