#
Abstract of my Master's 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.