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

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

Cited in

(20)

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

Describes a project that uses

Uses Software

• Matita
• Haskell
• Coq

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)