A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading (Q5372007): Difference between revisions

@@ Property / cites work @@
+Higher-Order Dynamic Pattern Unification for Dependent Types and Records
+Normal rank
@@ Property / cites work @@
+Crafting a Proof Assistant
@@ Property / cites work: Crafting a Proof Assistant / rank @@
+Normal rank
@@ Property / cites work @@
+Hints in Unification
@@ Property / cites work: Hints in Unification / rank @@
+Normal rank
@@ Property / cites work @@
+A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions
+Normal rank
@@ Property / cites work @@
+A New Approach to Incremental Cycle Detection and Related Problems
+Normal rank
@@ Property / cites work @@
+Idris, a general-purpose dependently typed programming language: Design and implementation
+Normal rank
@@ Property / cites work @@
+A Linear Spine Calculus
@@ Property / cites work: A Linear Spine Calculus / rank @@
+Normal rank
@@ Property / cites work @@
+ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter
+Normal rank
@@ Property / cites work @@
+Higher-order unification with dependent function types
+Normal rank
@@ Property / cites work @@
+Packaging Mathematical Structures
@@ Property / cites work: Packaging Mathematical Structures / 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 @@
+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 @@
+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 @@
+Type checking with universes
@@ Property / cites work: Type checking with universes / rank @@
+Normal rank
@@ Property / cites work @@
+Q4484328
@@ Property / cites work: Q4484328 / rank @@
+Normal rank
@@ Property / cites work @@
+Unification: a multidisciplinary survey
@@ Property / cites work: Unification: a multidisciplinary survey / rank @@
+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 @@
+Contextual modal type theory
@@ Property / cites work: Contextual modal type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Dependently Typed Programming in Agda
@@ Property / cites work: Dependently Typed Programming in Agda / rank @@
+Normal rank
@@ Property / cites work @@
+Verifying the unification algorithm in LCF
@@ Property / cites work: Verifying the unification algorithm in LCF / rank @@
+Normal rank
@@ Property / cites work @@
+Q4223031
@@ Property / cites work: Q4223031 / rank @@
+Normal rank
@@ Property / cites work @@
+A Machine-Oriented Logic Based on the Resolution Principle
+Normal rank
@@ Property / cites work @@
+Universe Polymorphism in Coq
@@ Property / cites work: Universe Polymorphism in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+A unification algorithm for Coq featuring universe polymorphism and overloading
+Normal rank
@@ Property / cites work @@
+Mtac
@@ Property / cites work: Mtac / rank @@
+Normal rank
@@ Property / cites work @@
+Mtac: A monad for typed tactic programming in Coq
@@ Property / cites work: Mtac: A monad for typed tactic programming in Coq / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1017/s0956796817000028
+Normal rank
@@ Property / OpenAlex ID @@
+W2586911241
@@ Property / OpenAlex ID: W2586911241 / rank @@
+Normal rank