| 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. 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 expressions cannot go wrong. First, we give the definitions and proofs in an informal style, and then we present and explain the formalisation of these definitions and proofs. For the formalisation, we use the proof editor ALF and its pattern matching facility. | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||