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

DOI10.1017/S0956796817000028MaRDI QIDQ5372007zbMATH OpenOpenAlexFDO

Authors Beta Ziliani, Matthieu Sozeau

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

Coqunificationcalculus of inductive constructions

Mathematics Subject Classification ID

Recommendations

• A unification algorithm for Coq featuring universe polymorphism and overloading
• Higher-order unification with dependent function types
• A mechanized textbook proof of a type unification algorithm
• A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
• Universe polymorphism in Coq

Cites work

• scientific article; zbMATH DE number 1231700 (Why is no real title available?)
• scientific article; zbMATH DE number 1927411 (Why is no real title available?)
• A Linear Spine Calculus
• A Machine-Oriented Logic Based on the Resolution Principle
• A bi-directional refinement algorithm for the calculus of (co)inductive constructions
• A machine-checked proof of the odd order theorem
• A new approach to incremental cycle detection and related problems
• A unification algorithm for Coq featuring universe polymorphism and overloading
• Canonical structures for the working Coq user
• Contextual modal type theory
• Crafting a Proof Assistant
• Dependently typed programming in Agda
• ELPI: fast, embeddable, \(\lambda \)Prolog interpreter
• Higher-order dynamic pattern unification for dependent types and records
• Higher-order unification with dependent function types
• Hints in Unification
• How to make ad hoc proof automation less ad hoc
• How to make ad hoc proof automation less ad hoc
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Mtac: a monad for typed tactic programming in Coq
• Mtac: a monad for typed tactic programming in Coq
• Packaging Mathematical Structures
• Type checking with universes
• Unification: a multidisciplinary survey
• Universe polymorphism in Coq
• Verifying the unification algorithm in LCF

Cited in

(5)

• A unification algorithm for Coq featuring universe polymorphism and overloading
• Unifiers as equivalences: proof-relevant unification of dependently typed data
• Sharing proofs with predicative theories through universe-polymorphic elaboration
• The \textsc{MetaCoq} project
• GNUC: a new universal composability framework

Describes a project that uses

Uses Software

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

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

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