Hints in Unification

DOI10.1007/978-3-642-03359-9_8MaRDI QIDQ3183522zbMATH OpenOpenAlexFDO

Authors Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi

Publication date 20 October 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-03359-9_8

Mathematics Subject Classification ID

Recommendations

• Canonical structures for the working Coq user
• Nonuniform coercions via unification hints
• A mechanized textbook proof of a type unification algorithm
• Higher-order unification with dependent function types
• Type Reconstruction for Type Classes

Cites work

• A constructive and formal proof of Lebesgue's dominated convergence theorem in the interactive theorem prover Matita
• A Modular Formalisation of Finite Group Theory
• Canonical Big Operators
• Coercive subtyping
• First-Class Type Classes
• scientific article; zbMATH DE number 1696760 (Why is no real title available?)
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Working with Mathematical Structures in Type Theory

Cited in

(23)

• Relaxed unification -- proposal
• Functions-as-constructors higher-order unification: extended pattern unification
• Essential unifiers
• Automated Reasoning in Higher-Order Regular Algebra
• Formalising overlap algebras in Matita
• Type classes for mathematics in type theory
• Generic literals
• Nonuniform coercions via unification hints
• Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
• Validating Mathematical Structures
• Interfacing Coq + SSReflect with GAP
• The Matita interactive theorem prover
• Computer Certified Efficient Exact Reals in Coq
• Implementing type theory in higher order constraint logic programming
• Canonical structures for the working Coq user
• A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
• scientific article; zbMATH DE number 2232298 (Why is no real title available?)
• Mathematical structures in dependent type theory (invited talk)
• Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi (system description)
• Machine-checked categorical diagrammatic reasoning
• Rapid prototyping formal systems in MMT: 5 case studies
• Use and abuse of instance parameters in the Lean mathematical library.
• A formalization of multi-tape Turing machines

Describes a project that uses

Uses Software

• Coq
• Haskell
• Matita

This page was built for publication: Hints in Unification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3183522)