Program extraction from large proof developments

DOI10.1007/10930755_14MaRDI QIDQ3559767zbMATH OpenOpenAlexFDO

Authors Luís Cruz-Filipe, Bas Spitters

Publication date 7 May 2010

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

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

zbMATH Keywords

constructive mathematicsformalized mathematicsprogram extractiontype theory

Mathematics Subject Classification ID

Recommendations

• A large-scale experiment in executing extracted programs
• Extraction and verification of programs by analysis of formal proofs
• Computer Aided Systems Theory – EUROCAST 2005
• Program Extraction in Constructive Analysis
• Refined program extraction from classical proofs: Some case studies

Cited in

(12)

• Program extraction for mutable arrays
• Code-carrying theories
• A large-scale experiment in executing extracted programs
• Practical program extraction from classical proofs
• Certified Exact Transcendental Real Number Computation in Coq
• scientific article; zbMATH DE number 512774 (Why is no real title available?)
• Extracting functional programs from Coq, in Coq
• Computer Certified Efficient Exact Reals in Coq
• Computer Aided Systems Theory – EUROCAST 2005
• Program extraction in exact real arithmetic
• Program extraction from classical proofs
• A computer-verified monadic functional implementation of the integral

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Program extraction from large proof developments

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