Program extraction from proofs of weak head normalization

MaRDI QIDQ2852349zbMATH OpenFDO

Authors Małgorzata Biernacka, Olivier Danvy, Kristian Støvring

Publication date 8 October 2013

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

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05)

Recommendations

• scientific article; zbMATH DE number 512774
• Program extraction from normalization proofs
• Types for Proofs and Programs
• Eliminating proofs from programs
• Extraction and verification of programs by analysis of formal proofs

Cited in

(12)

• Proof normalization with nonstandard objects
• Head linear reduction and pure proof net extraction
• A context-based approach to proving termination of evaluation
• Eliminating proofs from programs
• scientific article; zbMATH DE number 512774 (Why is no real title available?)
• Two \textit{different} strong normalization proofs?
• First order marked types
• Normalization by Evaluation for Typed Weak lambda-Reduction
• Types for Proofs and Programs
• Program extraction from normalization proofs
• Coq formalization of the higher-order recursive path ordering
• Abbreviation templates

This page was built for publication: Program extraction from proofs of weak head normalization

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