4 papers
Formal Small-step Verification of a Call-by-value Lambda Calculus Machine
Fabian Kunze, Gert Smolka, Yannick Forster
We formally verify an abstract machine for a call-by-value lambda-calculus with de Bruijn terms, simple substitution, and small-step semantics. We follow a stepwise refinement appr…
Constructive Analysis of S1S and Büchi Automata
Moritz Lichter, Gert Smolka
We study S1S and Büchi automata in the constructive type theory of the Coq proof assistant. For UP semantics (ultimately periodic sequences), we verify Büchi's translation of formu…
A Linear First-Order Functional Intermediate Language for Verified Compilers
Sigurd Schneider, Gert Smolka, Sebastian Hack
We present the linear first-order intermediate language IL for verified compilers. IL is a functional language with calls to a nondeterministic environment. We give IL terms a seco…
Correctness of an Incremental and Worst-Case Optimal Decision Procedure for Modal Logic with Eventualities
Mark Kaminski, Gert Smolka
We present a simple theory explaining the construction and the correctness of an incremental and worst-case optimal decision procedure for modal logic with eventualities. The proce…