| A Machine-assisted Proof that Well Typed Expressions Cannot Go Wrong (1998) | |||||||||||||||
Abstract | |||||||||||||||
| This paper deals with the application of constructive type theory to the theory of programming languages. By constructive type theory we understand ørst and foremost Martin-L#f's theory of logical types. The main aim of this work is to investigate constructive formalisations of the mathematics of programs. Here, we consider a small typed functional language and prove some properties about it, arriving at the property that establishes that well typed (closed) expressions cannot go wrong. First, we give all the deønitions and proofs in an informal style, and then we present and explain the formalisation of these deønitions and proofs. For the formalisation, we use the proof editor ALF and its pattern matching facility. Department of Computing Science, Chalmers University of Technology, G#teborg, Sweden Contents 1 Introduction 1 1.1 About this Paper : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 1 2 Informal Presentation 3 2.1 The Syntax of the Language : : ... | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||