A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading

DOI10.1017/S0956796817000028zbMath1418.68185OpenAlexW2586911241MaRDI QIDQ5372007

Matthieu Sozeau, Beta Ziliani

Publication date: 23 October 2017

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796817000028

zbMATH Keywords

unificationCoqcalculus of inductive constructions

Mathematics Subject Classification ID

Related Items (1)

The \textsc{MetaCoq} project

Uses Software

• Coq
• LCF
• Agda
• Irdis
• Mtac
• Idris
• ELPI

Cites Work

• Unnamed Item
• Unnamed Item
• Verifying the unification algorithm in LCF
• Type checking with universes
• Universe Polymorphism in Coq
• A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions
• A unification algorithm for Coq featuring universe polymorphism and overloading
• Higher-Order Dynamic Pattern Unification for Dependent Types and Records
• Hints in Unification
• Packaging Mathematical Structures
• ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter
• Crafting a Proof Assistant
• Dependently Typed Programming in Agda
• Unification: a multidisciplinary survey
• A Linear Spine Calculus
• A New Approach to Incremental Cycle Detection and Related Problems
• Higher-order unification with dependent function types
• How to make ad hoc proof automation less ad hoc
• Mtac
• Contextual modal type theory
• Canonical Structures for the Working Coq User
• A Machine-Checked Proof of the Odd Order Theorem
• Mtac: A monad for typed tactic programming in Coq
• How to make ad hoc proof automation less ad hoc
• Idris, a general-purpose dependently typed programming language: Design and implementation
• A Machine-Oriented Logic Based on the Resolution Principle

This page was built for publication: A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading