Program development by proof transformation.

MaRDI QIDQ3083675zbMATH OpenFDO

Authors Luca Chiarabini

Publication date 23 March 2011

Full work available at URL http://edoc.ub.uni-muenchen.de/11064/

zbMATH Keywords

automatic and semi-automatic methodscomputational biologyextraction of efficient codemanipulation of formal proofsprogram extraction from proof

Mathematics Subject Classification ID

Edge subsets with special properties (factorization, matching, partitioning, covering and packing, etc.) (05C70) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Computational learning theory (68Q32) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Extraction and verification of programs by analysis of formal proofs
• Proofs and programs: A naïve approach to program extraction
• scientific article; zbMATH DE number 2003148
• scientific article; zbMATH DE number 1617311
• Program development in constructive type theory

Cited in

(2)

• Code-carrying theories
• scientific article; zbMATH DE number 140006 (Why is no real title available?)

Describes a project that uses

Uses Software

• Isabelle
• Agda
• Coq

This page was built for publication: Program development by proof transformation.

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