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: a monad for typed tactic programming in Coq
- 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 (5)
- The \textsc{MetaCoq} project
- GNUC: a new universal composability framework
- A unification algorithm for Coq featuring universe polymorphism and overloading
- Sharing proofs with predicative theories through universe-polymorphic elaboration
- Unifiers as equivalences: proof-relevant unification of dependently typed data
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)
