Eliminating proofs from programs

MaRDI QIDQ2844809zbMATH OpenFDO

Authors Femke van Raamsdonk, Paula Severi

Publication date 19 August 2013

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

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 512774
• Program extraction from proofs of weak head normalization
• Program extraction from normalization proofs
• Proofs and programs: A naïve approach to program extraction
• scientific article; zbMATH DE number 2003148

Cited in

(11)

• Program extraction from proofs of weak head normalization
• scientific article; zbMATH DE number 2185653 (Why is no real title available?)
• An operational approach to program extraction in the calculus of constructions
• scientific article; zbMATH DE number 3850462 (Why is no real title available?)
• Attributive Types for Proof Erasure
• A Proof-Theoretic Account of Programming and the Role of Reduction Rules
• scientific article; zbMATH DE number 2085175 (Why is no real title available?)
• Elimination Techniques for Program Analysis
• A Formal Proof of Square Root and Division Elimination in Embedded Programs
• scientific article; zbMATH DE number 3212023 (Why is no real title available?)
• Program extraction from normalization proofs

This page was built for publication: Eliminating proofs from programs

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