[Club2] Talk by Simon Wimmer (today, 14:00): Formally Verified Complexity Analysis of a Functional Language

[Lars Noschinski]

Hi everyone,

Today (Wednesday, Aug. 6) on 14:00 , Simon Wimmer will present his B.Sc.
thesis on

Formally Verified Complexity Analysis of a Functional Language
Wednesday, 2014-08-06, 14:00, Room: Turing (00.09.038).

This thesis describes a framework for the formally verified runtime
complexity analysis of functional programs with the help of
Isabelle/HOL. A simple, deeply embedded ML-style programming language
PMλ is defined together with a corresponding smallstep operational
semantics. Additionally, a complexity measure for general terminating
PMλ-programs is defined. In order to enable employment of the framework
for practical complexity analyses, fundamental properties of the
language, its semantics, and the complexity measure are shown.

-- Lars