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.