Formal compiler construction in a logical framework

DOI10.1007/S10990-006-8746-6MaRDI QIDQ853741zbMATH OpenOpenAlexWikidataFDO

Authors Jason Hickey, Aleksey Nogin

Publication date 17 November 2006

Published in Higher-Order and Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10990-006-8746-6

zbMATH Keywords

Formal compilerHigher-order abstract syntaxLogical programming environment

Mathematics Subject Classification ID

Logic programming (68N17) Theory of compilers and interpreters (68N20)

Recommendations

• Compilation as Rewriting in Higher Order Logic
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• A Framework for Formal Verification of Compiler Optimizations
• scientific article; zbMATH DE number 2043526
• scientific article; zbMATH DE number 2090288

Cites work

• scientific article; zbMATH DE number 1612495 (Why is no real title available?)
• scientific article; zbMATH DE number 578226 (Why is no real title available?)
• scientific article; zbMATH DE number 1927428 (Why is no real title available?)
• Edinburgh LCF. A mechanized logic of computation
• Representing Control: a Study of the CPS Transformation
• Stack-based typed assembly language
• The categorical abstract machine
• Theorem Proving in Higher Order Logics

Cited in

(7)

• scientific article; zbMATH DE number 1543038 (Why is no real title available?)
• Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
• scientific article; zbMATH DE number 3874650 (Why is no real title available?)
• A higher-order abstract syntax approach to verified transformations on functional programs
• A formal development of an efficient supercombination compiler
• TSFC: A Structure-Preserving Form Compiler
• Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic

Describes a project that uses

Uses Software

• ML
• MetaPRL
• OCaml
• LCF
• YACC
• TALx86

This page was built for publication: Formal compiler construction in a logical framework

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q853741)