18 citations · 46 across the 8 of their papers we have counts for
Showing 2018Show all
2 papers · 1 filter
cs.LO2018★ 3 cited
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…
cs.LO2018
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…