Type classes for mathematics in type theory (Q3094177): Difference between revisions

@@ Property / describes a project that uses @@
+AXIOM
@@ Property / describes a project that uses: AXIOM / 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 @@
+CLEAN
@@ Property / describes a project that uses: CLEAN / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+C-CoRN
@@ Property / describes a project that uses: C-CoRN / 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 / cites work @@
+The calculus of constructions
@@ Property / cites work: The calculus of constructions / 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 @@
+Setoids in type theory
@@ Property / cites work: Setoids in type theory / rank @@
+Normal rank
@@ Property / cites work @@
+User interaction with the Matita proof assistant
@@ Property / cites work: User interaction with the Matita proof assistant / rank @@
+Normal rank
@@ Property / cites work @@
+Hints in Unification
@@ Property / cites work: Hints in Unification / rank @@
+Normal rank
@@ Property / cites work @@
+Extending Coq with Imperative Features and Its Application to SAT Verification
+Normal rank
@@ Property / cites work @@
+Partial Horn logic and Cartesian categories
@@ Property / cites work: Partial Horn logic and Cartesian categories / rank @@
+Normal rank
@@ Property / cites work @@
+A computer-verified monadic functional implementation of the integral
+Normal rank
@@ Property / cites work @@
+Certified Exact Transcendental Real Number Computation in Coq
+Normal rank
@@ Property / cites work @@
+First-Class Type Classes
@@ Property / cites work: First-Class Type Classes / rank @@
+Normal rank
@@ Property / cites work @@
+A type system for computer algebra
@@ Property / cites work: A type system for computer algebra / rank @@
+Normal rank
@@ Property / cites work @@
+Working with Mathematical Structures in Type Theory
+Normal rank
@@ Property / cites work @@
+Dependently typed records in type theory
@@ Property / cites work: Dependently typed records in type theory / rank @@
+Normal rank
@@ Property / cites work @@
+A constructive algebraic hierarchy in Coq.
@@ Property / cites work: A constructive algebraic hierarchy in Coq. / rank @@
+Normal rank
@@ Property / cites work @@
+Packaging Mathematical Structures
@@ Property / cites work: Packaging Mathematical Structures / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1017/s0960129511000119
+Normal rank
@@ Property / OpenAlex ID @@
+W2164688709
@@ Property / OpenAlex ID: W2164688709 / rank @@
+Normal rank