Calculating certified compilers for non-deterministic languages

DOI10.1007/978-3-319-19797-5_8MaRDI QIDQ2941174zbMATH OpenOpenAlexWikidataFDO

Authors Patrick Bahr

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)

Recommendations

• Calculating correct compilers
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• scientific article; zbMATH DE number 3947597
• A verified compiler for an impure functional language
• Certifiably Sound Parallelizing Transformations

Cites work

• scientific article; zbMATH DE number 4035108 (Why is no real title available?)
• A functional correspondence between call-by-need evaluators and lazy abstract machines
• Algebra of programming in Agda: Dependent types for relational program derivation
• Calculating correct compilers
• Constructivism in mathematics. An introduction. Volume I
• Deriving Target Code as a Representation of Continuation Semantics
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion
• Program calculation in Coq
• Programming in Haskell
• What is the meaning of these constant interruptions?

Cited in

(1)

• Calculating correct compilers

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Calculating certified compilers for non-deterministic languages

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