Exercising Nuprl’s Open-Endedness

DOI10.1007/978-3-319-42432-3_3zbMath1434.68644MaRDI QIDQ2819194

Vincent Rahli

Publication date: 28 September 2016

Published in: Mathematical Software – ICMS 2016 (Search for Journal in Brave)

Full work available at URL: http://pure-oai.bham.ac.uk/ws/files/77243031/71144969_from_vincent_rahli.pdf

zbMATH Keywords

continuity; semantics; axiom of choice; Coq; bar induction; choice sequences; Nuprl; open-endedness

Mathematics Subject Classification ID

03F60: Constructive and recursive analysis

03B35: Mechanization of proofs and logical operations

03E25: Axiom of choice and related propositions

68V20: Formalization of mathematics in connection with theorem provers

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Uses Software

• Coq
• Nuprl
• Agda
• Irdis
• Idris