On Choice Rules in Dependent Type Theory (Q2988806): Difference between revisions

@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Matita
@@ Property / describes a project that uses: Matita / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2598762888
@@ Property / OpenAlex ID: W2598762888 / rank @@
+Normal rank
@@ Property / cites work @@
+The Matita Interactive Theorem Prover
@@ Property / cites work: The Matita Interactive Theorem Prover / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Q5753923
@@ Property / cites work: Q5753923 / rank @@
+Normal rank
@@ Property / cites work @@
+Sheaves in geometry and logic: a first introduction to topos theory
+Normal rank
@@ Property / cites work @@
+Modular correspondence between dependent type theories and categories including pretopoi and topoi
+Normal rank
@@ Property / cites work @@
+A minimalist two-level foundation for constructive mathematics
+Normal rank
@@ Property / cites work @@
+Elementary quotient completion
@@ Property / cites work: Elementary quotient completion / rank @@
+Normal rank
@@ Property / cites work @@
+Quotient completion for the foundation of constructive mathematics
+Normal rank
@@ Property / cites work @@
+Unifying exact completions
@@ Property / cites work: Unifying exact completions / rank @@
+Normal rank
@@ Property / cites work @@
+Q5718565
@@ Property / cites work: Q5718565 / rank @@
+Normal rank
@@ Property / cites work @@
+An extensional Kleene realizability semantics for the Minimalist Foundation
+Normal rank
@@ Property / cites work @@
+Q3688389
@@ Property / cites work: Q3688389 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3999860
@@ Property / cites work: Q3999860 / rank @@
+Normal rank
@@ Property / cites work @@
+Realizability. An introduction to its categorical side
+Normal rank
@@ Property / cites work @@
+Q4247310
@@ Property / cites work: Q4247310 / rank @@
+Normal rank
@@ Property / cites work @@
+Independence of the induction principle and the axiom of choice in the pure calculus of constructions
+Normal rank
@@ Property / cites work @@
+Constructivism in mathematics. An introduction. Volume I
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:2988806