| A Machine-assisted Proof of the Property for a Small Typed Functional Language (1995) | |||||||||||||||
Abstract | |||||||||||||||
| 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-Lof'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 analyze is a small typed functional language. We present its syntax, its dynamic semantics and its type system. Among other properties, we present a formalization of the Subject Reduction property for the language. The proof assistant we use is ALF. Contents 1 Introduction 1 1.1 About this Paper . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2 Informal Presentation 3 2.1 The Syntax of the Language . . . . . . . . . . . . . . . . . . . . . . . . . . . .... | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||