Types for Proofs and Programs

DOI10.1007/11617990MaRDI QIDQ5897608zbMATH OpenOpenAlexFDO

Authors Thomas Meyer, Burkhart Wolff

Publication date 13 November 2006

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

Full work available at URL https://doi.org/10.1007/11617990

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55)

Recommendations

• A verified compiler from Isabelle/HOL to CakeML
• Proving the correctness of compiler optimisations based on a global analysis: a study of strictness analysis^†
• Trusted Source Translation of a Total Function Language
• scientific article; zbMATH DE number 512903
• scientific article; zbMATH DE number 3995026

Cited in

(2)

• Optimizing structural recursion in functional programs
• scientific article; zbMATH DE number 1161584 (Why is no real title available?)

Describes a project that uses

Uses Software

• TVOC

This page was built for publication: Types for Proofs and Programs

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