Exercising Nuprl’s Open-Endedness (Q2819194): Difference between revisions

@@ Property / describes a project that uses @@
+Agda
@@ Property / describes a project that uses: Agda / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Irdis
@@ Property / describes a project that uses: Irdis / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Nuprl
@@ Property / describes a project that uses: Nuprl / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Idris
@@ Property / describes a project that uses: Idris / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2469929958
@@ Property / OpenAlex ID: W2469929958 / rank @@
+Normal rank
@@ Property / cites work @@
+Innovations in computational type theory using Nuprl
+Normal rank
@@ Property / cites work @@
+Towards a Formally Verified Proof Assistant
@@ Property / cites work: Towards a Formally Verified Proof Assistant / rank @@
+Normal rank
@@ Property / cites work @@
+On the computational content of the axiom of choice
+Normal rank
@@ Property / cites work @@
+A Brief Overview of Agda – A Functional Language with Dependent Types
+Normal rank
@@ Property / cites work @@
+Q3754620
@@ Property / cites work: Q3754620 / rank @@
+Normal rank
@@ Property / cites work @@
+Interacting with Modal Logics in the Coq Proof Assistant
+Normal rank
@@ Property / cites work @@
+Q4492739
@@ Property / cites work: Q4492739 / rank @@
+Normal rank
@@ Property / cites work @@
+The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
+Normal rank
@@ Property / cites work @@
+Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis
+Normal rank
@@ Property / cites work @@
+Q3204055
@@ Property / cites work: Q3204055 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4375633
@@ Property / cites work: Q4375633 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5343325
@@ Property / cites work: Q5343325 / rank @@
+Normal rank
@@ Property / cites work @@
+On weak completeness of intuitionistic predicate logic
+Normal rank
@@ Property / cites work @@
+Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
+Normal rank
@@ Property / cites work @@
+When is a functional program not a functional program?
+Normal rank
@@ Property / cites work @@
+Formalizing Type Operations Using the “Image” Type Constructor
+Normal rank
@@ Property / cites work @@
+Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types
+Normal rank
@@ Property / cites work @@
+Q5310885
@@ Property / cites work: Q5310885 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4145690
@@ Property / cites work: Q4145690 / rank @@
+Normal rank
@@ Property / cites work @@
+Constructivism in mathematics. An introduction. Volume I
+Normal rank
@@ Property / cites work @@
+Homotopy Type Theory: Univalent Foundations of Mathematics
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:2819194