Program extraction from normalization proofs

DOI10.1007/s11225-006-6604-5zbMath1095.03016OpenAlexW2020747436MaRDI QIDQ817701

Pierre Letouzey, Stefan Berghofer, Ulrich Berger, 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

realizabilitytyped lambda calculusproof assistantsprogram extraction from proofsNormalization by evaluation

Mathematics Subject Classification ID

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

Related Items (8)

Coq formalization of the higher-order recursive path ordering ⋮ Extracting a DPLL Algorithm ⋮ Extraction in Coq: An Overview ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Extraction of expansion trees ⋮ A Context-based Approach to Proving Termination of Evaluation ⋮ Mechanized metatheory revisited ⋮ Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention

Uses Software

• Coq
• Isabelle/HOL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Using information systems to solve recursive domain equations
• Synthesis of ML programs in the system Coq
• Term rewriting for normalization by evaluation.
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Intuitionistic model constructions and normalization proofs
• Artificial Intelligence and Symbolic Computation

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