Fabian Kunze: Bachelor's Thesis

Saarland University Computer Science

Verified Compilation of Weak Call-by-Value Lambda-Calculus into Combinators and Closures

Advisor: Gert Smolka


In this thesis, we relate the weak call-by-value λ-calculus L to two other systems: a call-by-value combinatory logic called SKv and a variant of L with closures, called LC. All proofs are carried out in the proof assistant Coq.

We show that L can be fully embedded into SKv by giving an injective mapping from L to SKv that preserves term equivalence and irreducibility in both directions.

We show that LC refines the semantics of L: It is sound and complete with respect to L, while allowing to postpone certain parts of computations until they become necessary.

We give a sound and complete interpreter for LC that can be used to interpret L.

Documents and Proof Scripts

Legal notice, Privacy policy