Calculating correct compilers

DOI10.1017/S0956796815000180zbMath1420.68053WikidataQ58061572 ScholiaQ58061572MaRDI QIDQ5371953

P. Bähr, G. Hutton

Publication date: 23 October 2017

Published in: Journal of Functional Programming (Search for Journal in Brave)

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Functional programming and lambda calculus (68N18)

Related Items (5)

Cutting Out Continuations ⋮ Calculating Certified Compilers for Non-deterministic Languages ⋮ Programming language semantics: It’s easy as 1,2,3 ⋮ Compiling a 50-year journey ⋮ Flag-based big-step semantics

Uses Software

• Coq
• HERMIT

Cites Work

• Unnamed Item
• Unnamed Item
• A functional theory of exceptions
• Inductive families
• Comparing control constructs by double-barrelled CPS
• A functional correspondence between call-by-need evaluators and lazy abstract machines
• Extraction in Coq: An Overview
• Deriving Target Code as a Representation of Continuation Semantics
• Deriving a lazy abstract machine
• Proving Correctness of Compilers Using Structured Graphs
• Mathematics of Program Construction
• What is the meaning of these constant interruptions?
• Programming in Haskell

This page was built for publication: Calculating correct compilers