scientific article; zbMATH DE number 2079040
From MaRDI portal
Publication:4474853
zbMATH Open1044.68546MaRDI QIDQ4474853FDOQ4474853
Authors: David R. Lester, Sava Mintchev 
Publication date: 21 July 2004
Title of this publication is not available (Why is that?)
Recommendations
- The correctness of a higher-order lazy functional language implementation: An exercise in mechanical theorem proving
- A verified compiler for an impure functional language
- scientific article; zbMATH DE number 3846848
- Proving correctness of a compiler using step-indexed logical relations
- Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
Theory of compilers and interpreters (68N20) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)
Cited In (12)
- The correctness of a higher-order lazy functional language implementation: An exercise in mechanical theorem proving
- Proving correctness of a compiler using step-indexed logical relations
- A certified extension of the Krivine machine for a call-by-name higher-order imperative language
- Pilsner: a compositionally verified compiler for a higher-order imperative language
- Biorthogonality, step-indexing and compiler correctness
- A list-machine benchmark for mechanized metatheory (extended abstract)
- A verified compiler for an impure functional language
- Compilation as Rewriting in Higher Order Logic
- The correctness of a code generator for a functional language
- A list-machine benchmark for mechanized metatheory
- Correctness of procedure representations in higher-order assembly language
- A provably correct compilation of functional languages into scripting languages
Uses Software
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4474853)
