Program extraction from normalization proofs
type: Item
instance of: scholarly article
title: Program extraction from normalization proofs
zbMATH Open document ID: 1095.03016
author: Ulrich Berger
author: Stefan Berghofer
author: Pierre Letouzey
author: Helmut Schwichtenberg
published in: Studia Logica
publication date: 2006-03-17T00:00:00Z
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 68N30
zbMATH DE Number: 5013035
zbMATH Keywords: Normalization by evaluation
zbMATH Keywords: typed lambda calculus
zbMATH Keywords: realizability
zbMATH Keywords: program extraction from proofs
zbMATH Keywords: proof assistants
describes a project that uses: Isabelle/HOL
describes a project that uses: Coq
MaRDI profile type: Publication
full work available at URL: s11225-006-6604-5
OpenAlex ID: W2020747436
cites work: Q4281467
cites work: Term rewriting for normalization by evaluation.
cites work: Q4435458
cites work: Q4525278
cites work: Intuitionistic model constructions and normalization proofs
cites work: Q5667469
cites work: Q5344164
cites work: Using information systems to solve recursive domain equations
cites work: Q4435471
cites work: Synthesis of ML programs in the system Coq
cites work: Artificial Intelligence and Symbolic Computation
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
DOI: 10.1007/S11225-006-6604-5
description: scientific article; zbMATH DE number 5013035