Realizability interpretation of proofs in constructive analysis

DOI10.1007/s00224-007-9027-4zbMath1166.03035OpenAlexW2030292569MaRDI QIDQ1015381

Helmut Schwichtenberg

Publication date: 8 May 2009

Published in: Theory of Computing Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00224-007-9027-4

zbMATH Keywords

realizabilityprogram extractionintermediate value theoremcontinuous inverse functionnon-computational quantifier

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Mechanization of proofs and logical operations (03B35)

Related Items

Unnamed Item ⋮ Proofs, programs, processes ⋮ Program extraction in exact real arithmetic ⋮ A computer-verified monadic functional implementation of the integral ⋮ From Coinductive Proofs to Exact Real Arithmetic

Cites Work

• Continuity of monotone functions
• Term rewriting for normalization by evaluation.
• Uniform Heyting arithmetic
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Exact calculation of inverse functions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item