Eliminating proofs from programs

zbMATH Open1270.03056MaRDI QIDQ2844809FDOQ2844809

Authors: Femke van Raamsdonk, Paula Severi 

Publication date: 19 August 2013

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

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

Mathematics Subject Classification ID

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

Cited In (11)

• A Formal Proof of Square Root and Division Elimination in Embedded Programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Attributive Types for Proof Erasure
• An operational approach to program extraction in the calculus of constructions
• Title not available (Why is that?)
• Program extraction from proofs of weak head normalization
• Title not available (Why is that?)
• Elimination Techniques for Program Analysis
• Program extraction from normalization proofs
• A Proof-Theoretic Account of Programming and the Role of Reduction Rules

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)