Producing certified functional code from inductive specifications

DOI10.1007/978-3-642-35308-6_9MaRDI QIDQ4916053zbMATH OpenOpenAlexFDO

Authors Pierre-Nicolas Tollitte, David Delahaye, Catherine Dubois

Publication date 19 April 2013

Published in Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-35308-6_9

zbMATH Keywords

Coqexecutable specificationsfunctional code generationinductive relationssoundness proof generation

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 2003158
• Verifying programs in the calculus of inductive constructions
• Extracting Purely Functional Contents from Logical Inductive Types
• Synthesis of ML programs in the system Coq
• scientific article; zbMATH DE number 1420787

Cited in

(9)

• Foundational property-based testing
• Certifying and Reasoning on Cost Annotations of Functional Programs
• Turning Inductive into Equational Specifications
• Extracting Purely Functional Contents from Logical Inductive Types
• scientific article; zbMATH DE number 1927413 (Why is no real title available?)
• Automated Deduction – CADE-19
• Verified runtime assertion checking for memory properties
• Sound runtime assertion checking for memory properties via program transformation
• Towards a certified reference monitor of the android 10 permission system

Describes a project that uses

Uses Software

• Coq
• Twelf

This page was built for publication: Producing certified functional code from inductive specifications

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