Extraction of structured programs from specification proofs

DOI10.1007/978-3-540-44616-3_24MaRDI QIDQ2722042zbMATH OpenFDO

Authors John N. Crossley, Iman Poernomo, Martin Wirsing

Publication date 11 July 2001

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

Full work available at URL https://kclpure.kcl.ac.uk/portal/en/publications/66723101-e687-4ffa-b275-26bd67170e4b

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Programs, proofs and parametrized specifications
• Proofs and programs: A naïve approach to program extraction
• Studies of a theory of specifications with built-in program extraction
• Extraction and verification of programs by analysis of formal proofs
• An operational approach to program extraction in the calculus of constructions

Cited in

(10)

• Practical program extraction from classical proofs
• scientific article; zbMATH DE number 2177628 (Why is no real title available?)
• An operational approach to program extraction in the calculus of constructions
• Program development by proof transformation.
• scientific article; zbMATH DE number 512774 (Why is no real title available?)
• scientific article; zbMATH DE number 2063221 (Why is no real title available?)
• Programs, proofs and parametrized specifications
• Program extraction applied to monadic parsing
• Studies of a theory of specifications with built-in program extraction
• Proofs and programs: A naïve approach to program extraction

Describes a project that uses

Uses Software

• Maude
• Nuprl

This page was built for publication: Extraction of structured programs from specification proofs

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