18 citations · 46 across the 8 of their papers we have counts for
9 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…
Verification of PCP-Related Computational Reductions in Coq
Yannick Forster, Edith Heiter, Gert Smolka
We formally verify several computational reductions concerning the Post correspondence problem (PCP) using the proof assistant Coq. Our verifications include a reduction of a strin…
An Inductive Proof Method for Simulation-based Compiler Correctness
Sigurd Schneider, Gert Smolka, Sebastian Hack
We study induction on the program structure as a proof method for bisimulation-based compiler correctness. We consider a first-order language with mutually recursive function defin…
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…
Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies
Mark Kaminski, Sigurd Schneider, Gert Smolka
We present a terminating tableau calculus for graded hybrid logic with global modalities, reflexivity, transitivity and role hierarchies. Termination of the system is achieved thro…
Analytic Tableaux for Simple Type Theory and its First-Order Fragment
Chad E. Brown, Gert Smolka
We study simple type theory with primitive equality (STT) and its first-order fragment EFO, which restricts equality and quantification to base types but retains lambda abstraction…
A Minimal Propositional Type Theory
Mark Kaminski, Gert Smolka
Propositional type theory, first studied by Henkin, is the restriction of simple type theory to a single base type that is interpreted as the set of the two truth values. We show t…