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

realizabilityproof assistantstyped lambda calculusprogram extraction from proofsNormalization by evaluation

Mathematics Subject Classification ID

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

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

• 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?)
• Artificial Intelligence and Symbolic Computation
• 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

(17)

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

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)