Extracting Purely Functional Contents from Logical Inductive Types

DOI10.1007/978-3-540-74591-4_7MaRDI QIDQ3523167zbMATH OpenOpenAlexFDO

Authors David Delahaye, Catherine Dubois, Jean-Frédéric Étienne

Publication date 2 September 2008

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

Full work available at URL https://doi.org/10.1007/978-3-540-74591-4_7

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Producing certified functional code from inductive specifications
• Verifying programs in the calculus of inductive constructions
• scientific article; zbMATH DE number 2003158
• Extraction in Coq: An Overview
• scientific article; zbMATH DE number 2003148

Cited in

(5)

• A list-machine benchmark for mechanized metatheory
• Mechanized semantics for the clight subset of the C language
• Turning Inductive into Equational Specifications
• Towards a Theory of Extractable Functions
• Producing certified functional code from inductive specifications

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Extracting Purely Functional Contents from Logical Inductive Types

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