The design and implementation of a certifying compiler
- 1 May 1998
- proceedings article
- Published by Association for Computing Machinery (ACM)
- Vol. 33 (5) , 333-344
- https://doi.org/10.1145/277650.277752
Abstract
No abstract availableThis publication has 11 references indexed in Scilit:
- Proof-carrying codePublished by Association for Computing Machinery (ACM) ,1997
- Safe kernel extensions without run-time checkingPublished by Association for Computing Machinery (ACM) ,1996
- TILPublished by Association for Computing Machinery (ACM) ,1996
- The VLISP verified PreScheme compilerHigher-Order and Symbolic Computation, 1995
- VLISP: A verified implementation of SchemeHigher-Order and Symbolic Computation, 1995
- A framework for defining logicsJournal of the ACM, 1993
- PVS: A prototype verification systemLecture Notes in Computer Science, 1992
- Deciding Linear Inequalities by Computing Loop ResiduesJournal of the ACM, 1981
- Simplification by Cooperating Decision ProceduresACM Transactions on Programming Languages and Systems, 1979
- Advice on structuring compilers and proving them correctPublished by Association for Computing Machinery (ACM) ,1973