Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2019 / Oberseminar / Sebastian Sturm: Formalisation of Normalisation of the Simply Typed Lambda Calculus in F*


Inhaltsbereich

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

Oberseminarvortrag von Sebastian Sturm über Formalisation of Normalisation of the Simply Typed Lambda Calculus in F*
Wann 14:15 16:00 14.06.2019
von bis
Wo Raum L109, Oettingenstr. 67
Termin übernehmen vCal
iCal

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.

Artikelaktionen


Funktionsleiste