Calculating Certified Compilers for Non-deterministic Languages

DOI10.1007/978-3-319-19797-5_8zbMath1432.68066OpenAlexW1188080205WikidataQ58061581 ScholiaQ58061581MaRDI QIDQ2941174

P. Bähr

Publication date: 27 August 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-19797-5_8

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Coq

Cites Work

• Unnamed Item
• On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion
• Constructivism in mathematics. An introduction. Volume I
• A functional correspondence between call-by-need evaluators and lazy abstract machines
• Program Calculation in Coq
• Algebra of programming in Agda: Dependent types for relational program derivation
• Deriving Target Code as a Representation of Continuation Semantics
• Formal certification of a compiler back-end or
• Calculating correct compilers
• What is the meaning of these constant interruptions?
• Programming in Haskell

This page was built for publication: Calculating Certified Compilers for Non-deterministic Languages