Validating Mathematical Structures (Q5048998): Difference between revisions

@@ Property / describes a project that uses @@
+GitHub
@@ Property / describes a project that uses: GitHub / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PCM library
@@ Property / describes a project that uses: PCM library / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W3040202382
@@ Property / OpenAlex ID: W3040202382 / rank @@
+Normal rank
@@ Property / cites work @@
+Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
+Normal rank
@@ Property / cites work @@
+A hierarchy of monadic effects for program verification using equational reasoning
+Normal rank
@@ Property / cites work @@
+Hints in Unification
@@ Property / cites work: Hints in Unification / 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 @@
+Implicit coercions in type systems
@@ Property / cites work: Implicit coercions in type systems / rank @@
+Normal rank
@@ Property / cites work @@
+Coquelicot: a user-friendly library of real analysis for Coq
+Normal rank
@@ Property / cites work @@
+Telescopic mappings in typed lambda calculus
@@ Property / cites work: Telescopic mappings in typed lambda calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
+Normal rank
@@ Property / cites work @@
+The calculus of constructions
@@ Property / cites work: The calculus of constructions / rank @@
+Normal rank
@@ Property / cites work @@
+Packaging Mathematical Structures
@@ Property / cites work: Packaging Mathematical Structures / 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 @@
+The undecidability of the second-order unification problem
+Normal rank
@@ Property / cites work @@
+A Machine-Checked Proof of the Odd Order Theorem
@@ Property / cites work: A Machine-Checked Proof of the Odd Order Theorem / rank @@
+Normal rank
@@ Property / cites work @@
+How to make ad hoc proof automation less ad hoc
@@ Property / cites work: How to make ad hoc proof automation less ad hoc / rank @@
+Normal rank
@@ Property / cites work @@
+Constructive Type Classes in Isabelle
@@ Property / cites work: Constructive Type Classes in Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Canonical Structures for the Working Coq User
@@ Property / cites work: Canonical Structures for the Working Coq User / rank @@
+Normal rank
@@ Property / cites work @@
+The Lean Theorem Prover (System Description)
@@ Property / cites work: The Lean Theorem Prover (System Description) / rank @@
+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 @@
+Q3497625
@@ Property / cites work: Q3497625 / rank @@
+Normal rank
@@ Property / cites work @@
+First-Class Type Classes
@@ Property / cites work: First-Class Type Classes / rank @@
+Normal rank
@@ Property / cites work @@
+Type classes for mathematics in type theory
@@ Property / cites work: Type classes for mathematics in type theory / rank @@
+Normal rank