Abstract of Master Thesis
A Machine-assisted Proof of the Subject Reduction Property for a Small Typed Functional Language.
We present an experiment in formally describing a programming language and its properties in constructive type theory. By constructive type theory we understand primarily the formulation of Martin-Löf's set theory. Constructive type theory can also be seen as a programming language where we write types, and objects of these types that can be view as functional programs. Thus, practical applicability of type theory depends on the availability of programming environments or proof assistants. The language we analyse is a small typed functional language. We present its syntax, its dynamic semantics and its type system. Among other properties, we present a formalisation of the Subject Reduction property for the language. The proof assistant we use is ALF.