Program extraction from normalization proofs

DOI10.1007/S11225-006-6604-5MaRDI QIDQ817701zbMATH OpenOpenAlexFDO

Authors Ulrich Berger, Stefan Berghofer, Pierre Letouzey, Helmut Schwichtenberg

Publication date 17 March 2006

Published in Studia Logica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11225-006-6604-5

zbMATH Keywords

Normalization by evaluationprogram extraction from proofsproof assistantsrealizabilitytyped lambda calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

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

Cites work

• Artificial Intelligence and Symbolic Computation
• scientific article; zbMATH DE number 512774 (Why is no real title available?)
• scientific article; zbMATH DE number 2003148 (Why is no real title available?)
• scientific article; zbMATH DE number 2003158 (Why is no real title available?)
• scientific article; zbMATH DE number 1555179 (Why is no real title available?)
• scientific article; zbMATH DE number 3216998 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Intuitionistic model constructions and normalization proofs
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Synthesis of ML programs in the system Coq
• Term rewriting for normalization by evaluation.
• Using information systems to solve recursive domain equations

Cited in

(21)

• Proof normalization with nonstandard objects
• Mechanized metatheory revisited
• Intuitionistic model constructions and normalization proofs
• A context-based approach to proving termination of evaluation
• Eliminating proofs from programs
• Program extraction from proofs of weak head normalization
• Normalization for the simply-typed lambda-calculus in Twelf
• scientific article; zbMATH DE number 4014708 (Why is no real title available?)
• Extracting a DPLL algorithm
• Extraction in Coq: An Overview
• scientific article; zbMATH DE number 512774 (Why is no real title available?)
• Two \textit{different} strong normalization proofs?
• Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
• POPLMark reloaded: mechanizing proofs by logical relations
• Program extraction from nested definitions
• Types for Proofs and Programs
• Extraction of expansion trees
• Mechanized metatheory revisited: an extended abstract (invited paper)
• Constructive validity of a generalized Kreisel-Putnam rule
• Verified program extraction in number theory: the fundamental theorem of arithmetic and relatives
• Coq formalization of the higher-order recursive path ordering

Describes a project that uses

Uses Software

• Isabelle/HOL
• Coq

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

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