Uniform Heyting arithmetic
type: Item
instance of: scholarly article
title: Uniform Heyting arithmetic
zbMATH Open document ID: 1081.03057
author: Ulrich Berger
published in: Annals of Pure and Applied Logic
publication date: 2005-04-21T00:00:00Z
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 03B70
zbMATH DE Number: 2160244
zbMATH Keywords: extraction of programs from proofs
zbMATH Keywords: extension of Heyting arithmetic in finite types
MaRDI profile type: Publication
full work available at URL: j.apal.2004.10.006
OpenAlex ID: W1999810448
cites work: Q4281464
cites work: Q4524766
cites work: On the computational content of the axiom of choice
cites work: Total sets and objects in domain theory
cites work: Q5702662
cites work: Refined program extraction from classical proofs
cites work: Q4012886
cites work: Q4225148
cites work: A new method for establishing conservativity of classical systems over their intuitionistic version
cites work: Q5625124
cites work: ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
cites work: Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
cites work: Q5344164
cites work: Classical logic, storage operators and second-order lambda-calculus
cites work: Q4255509
cites work: Q5600870
cites work: Synthesis of ML programs in the system Coq
cites work: Q3395521
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
cites work: Q4215635
cites work: Constructivism in mathematics. An introduction. Volume II
Wikidata QID: Q126372103
DOI: 10.1016/J.APAL.2004.10.006
description: scientific article; zbMATH DE number 2160244