Sebastian Sturm: Formalisation of Normalisation of the Simply Typed Lambda Calculus in F*

Es spricht Sebastian Sturm über:
Formalisation of Normalisation of the Simply Typed Lambda Calculus in F*

Abstract:
As the implementations of program transformations grow in size and
complexity, the importance of formal correctness arguments rises. One
option is a formal verification using interactive theorem provers.
POPLmark-Reloaded is a theorem prover challenge from the field of
programming meta-theory, precisely normalisation for the simply typed
lambda calculus (STLC), and as such particularly suited for testing
theorem provers on that field.

This paper presents a partial solution for the POPLmark-Reloaded
challenge in F*. F* is a dependently typed programming language usable
both for verification and as a proof assistant. It combines
interactive proving with automatic, SMT based, approaches. After a
short introduction to F* and an overview for POPLmark-Reloaded we will
describe the formalisation and some benefits and drawbacks of using F*
for programming meta-theory proofs.