Exercising Nuprl’s Open-Endedness

DOI10.1007/978-3-319-42432-3_3zbMath1434.68644OpenAlexW2469929958MaRDI 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

continuitysemanticsaxiom of choiceCoqbar inductionchoice sequencesNuprlopen-endedness

Mathematics Subject Classification ID

Constructive and recursive analysis (03F60) Mechanization of proofs and logical operations (03B35) Axiom of choice and related propositions (03E25) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Coq
• Nuprl
• Agda
• Irdis
• Idris

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• Innovations in computational type theory using Nuprl
• Constructivism in mathematics. An introduction. Volume I
• When is a functional program not a functional program?
• Towards a Formally Verified Proof Assistant
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Interacting with Modal Logics in the Coq Proof Assistant
• On the computational content of the axiom of choice
• Formalizing Type Operations Using the “Image” Type Constructor
• The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
• Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
• On weak completeness of intuitionistic predicate logic

This page was built for publication: Exercising Nuprl’s Open-Endedness