Formal compiler construction in a logical framework

DOI10.1007/S10990-006-8746-6zbMATH Open1105.68020OpenAlexW2154518226WikidataQ122446240 ScholiaQ122446240MaRDI QIDQ853741FDOQ853741

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

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

zbMATH Keywords

Formal compilerHigher-order abstract syntaxLogical programming environment

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Edinburgh LCF. A mechanized logic of computation
• Stack-based typed assembly language
• Title not available (Why is that?)
• Representing Control: a Study of the CPS Transformation
• The categorical abstract machine
• Title not available (Why is that?)
• Theorem Proving in Higher Order Logics

Cited In (7)

• Title not available (Why is that?)
• Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
• TSFC: A Structure-Preserving Form Compiler
• Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic
• A formal development of an efficient supercombination compiler
• A higher-order abstract syntax approach to verified transformations on functional programs
• Title not available (Why is that?)

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)