Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / WS 2018/19 / Oberseminar / Sebastian Sturm: Verification and Theorem Proving in F*


Inhaltsbereich

Sebastian Sturm: Verification and Theorem Proving in F*

Oberseminarvortrag von Sebastian Sturm über Verification and Theorem Proving in F*
Wann 14:15 16:00 16.11.2018
von bis
Wo Raum L109, Oettingenstr. 67
Termin übernehmen vCal
iCal

Es spricht Sebastian Sturm über:
Verification and Theorem Proving in F*

Abstract:
F* is a dependently typed programming language usable both for
verification and as a proof assistant. It combines manual proving with
automatic, SMT based, approaches.

The goal of this thesis is to test F*'s verification and proving
capabilities on two illustrative examples. First I implemented and
verified insertion and deletion into and from red-black trees using
the refinement types feature. The main contribution then was an
implementation of the Poplmark-Reloaded theorem proving challenge in
F*. These challenge mainly consists of proving normalisation of a
version of the simply typed lambda calculus using logical relations.
In that part I mostly used Curry-Horward style proofs.

Artikelaktionen


Funktionsleiste