A unification algorithm for Coq featuring universe polymorphism and overloading

DOI10.1145/2784731.2784751MaRDI QIDQ2981954zbMATH OpenOpenAlexFDO

Authors Beta Ziliani, Matthieu Sozeau

Publication date 10 May 2017

Published in Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2784731.2784751

zbMATH Keywords

Coqinteractive theorem provingoverloadingunificationuniverse polymorphism

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
• A mechanized textbook proof of a type unification algorithm
• Higher-order unification with dependent function types
• A higher-order unification algorithm for inductive types and dependent types
• Unifiers as equivalences: proof-relevant unification of dependently typed data

Cited in

(8)

• Functions-as-constructors higher-order unification: extended pattern unification
• A mechanized textbook proof of a type unification algorithm
• Unifiers as equivalences: proof-relevant unification of dependently typed data
• A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
• A type checker for a logical framework with union and intersection types (system description)
• Design and implementation of the andromeda proof assistant
• The rewster: type preserving rewrite rules for the Coq proof assistant
• The Rewster: type preserving rewrite rules for the Rocq Prover. Extended version of the ITP 2024 paper

Describes a project that uses

Uses Software

• Agda
• Coq
• Mtac

This page was built for publication: A unification algorithm for Coq featuring universe polymorphism and overloading

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