Structure of a proof-producing compiler for a subset of higher order logic. (English) Zbl 1187.68141
De Nicola, Rocco (ed.), Programming languages and systems. 16th European symposium of programming, ESOP 2007, held as part of the joint European conferences on theory and practice of software, ETAPS 2007, Braga, Portugal, March 24 – April 1, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-71314-2/pbk). Lecture Notes in Computer Science 4421, 205-219 (2007).
Summary: We give an overview of a proof-producing compiler which translates recursion equations, defined in higher-order logic, to assembly language. The compiler is implemented and validated with a mix of translation validation and compiler verification techniques. Both the design of the compiler and its mechanical verification are implemented in the same logic framework.
For the entire collection see [Zbl 1116.68003].
For the entire collection see [Zbl 1116.68003].
MSC:
| 68N20 | Theory of compilers and interpreters |
