ComputingComputer EngineeringComputer ScienceCompilersFormal MethodsProgramming LanguagesDeductive VerificationFunctional ProgrammingPredicate LogicSpecification LanguagesType SystemsVerificationAbstract MachinesCategorical SemanticsCompiler DesignCorrectness CheckingLanguage VerificationLogical Framework ApproachProgram CorrectnessProgram Verification
A methodology for the verification of compiler correctness based on the LF logical framework as realized within the Elf programming language is presented. This technique is used to specify, implement, and verify a compiler from a simple functional programming language to a variant of the Categorical Abstract Machine (CAM).< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>
12
Gilles Kahn · Symposium on Theoretical Aspects of Computer Science · 1987 · 523 citations
M. Abadi, Luca Cardelli, Pierre-Louis Curien et al. · Journal of Functional Programming · 1991 · 366 citations · Full text
A simple applicative language: mini-ML
Dominique Clement, Thierry Despeyroux, Gilles Kahn et al. · 1986 · 161 citations · Full text
Elf: a language for logic definition and verified metaprogramming
Frank Pfenning · 2003 · 115 citations
Computing, Computer Science, Logic +15