A large-scale experiment in executing extracted programs

MaRDI QIDQ2852042zbMATH OpenFDO

Authors Luís Cruz-Filipe, Pierre Letouzey

Publication date 7 October 2013

Full work available at URL http://www.sciencedirect.com/science/article/pii/S1571066106001101

Mathematics Subject Classification ID

Recommendations

• Program extraction from large proof developments
• Extraction and verification of programs by analysis of formal proofs
• Computer Aided Systems Theory – EUROCAST 2005
• scientific article; zbMATH DE number 2003158
• Refined program extraction from classical proofs: Some case studies

Cited in

(10)

• Formally proving size optimality of sorting networks
• Tool support for proof engineering
• Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
• Extraction in Coq: An Overview
• Certified Exact Transcendental Real Number Computation in Coq
• Program extraction from large proof developments
• scientific article; zbMATH DE number 1897134 (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

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A large-scale experiment in executing extracted programs

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