A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
From MaRDI portal
Publication:5372007
DOI10.1017/S0956796817000028zbMATH Open1418.68185OpenAlexW2586911241MaRDI QIDQ5372007FDOQ5372007
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
Recommendations
Cites Work
- Dependently typed programming in Agda
- Mtac
- Idris, a general-purpose dependently typed programming language: Design and implementation
- ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter
- Crafting a Proof Assistant
- Contextual modal type theory
- A Machine-Oriented Logic Based on the Resolution Principle
- How to make ad hoc proof automation less ad hoc
- Unification: a multidisciplinary survey
- A New Approach to Incremental Cycle Detection and Related Problems
- Packaging Mathematical Structures
- A Machine-Checked Proof of the Odd Order Theorem
- Higher-order unification with dependent function types
- A Linear Spine Calculus
- A bi-directional refinement algorithm for the calculus of (co)inductive constructions
- Hints in Unification
- Verifying the unification algorithm in LCF
- Type checking with universes
- Canonical Structures for the Working Coq User
- Mtac: A monad for typed tactic programming in Coq
- A unification algorithm for Coq featuring universe polymorphism and overloading
- Higher-order dynamic pattern unification for dependent types and records
- Universe Polymorphism in Coq
- Title not available (Why is that?)
- How to make ad hoc proof automation less ad hoc
- Title not available (Why is that?)
Cited In (3)
Uses Software
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)
