Formal compiler construction in a logical framework

DOI10.1007/s10990-006-8746-6zbMath1105.68020OpenAlexW2154518226WikidataQ122446240 ScholiaQ122446240MaRDI QIDQ853741

Aleksey Nogin, Jason Hickey

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

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

Related Items

A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The categorical abstract machine
• Edinburgh LCF. A mechanized logic of computation
• Stack-based typed assembly language
• Representing Control: a Study of the CPS Transformation
• Theorem Proving in Higher Order Logics