8 citations · 9 across the 3 of their papers we have counts for
Showing cs.PLShow all
2 papers · 1 filter
cs.PL2016★ 1 cited
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…
cs.PL2015
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…