- A Predictable Unification A...
- Edit Event
- Cancel Event
- Preview Reminder
- Send Reminder
- Other events happening in April 2015
A Predictable Unification Algorithm for Coq Featuring Universe Polymorphism and Overloading
Speaker:
Matthieu Sozeau
, INRIA
Date: Wednesday, April 29, 2015
Time: 11:00 AM to 12:00 PM Note: all times are in the Eastern Time Zone
Public: Yes
Location: 32-G449 (Patil/Kiva)
Event Type:
Room Description:
Host: Adam Chlipala, CSAIL
Contact: Adam Chlipala, adamc@csail.mit.edu
Relevant URL: http://www.pps.univ-paris-diderot.fr/~sozeau/
Speaker URL: None
Speaker Photo:
None
Reminders to:
seminars@csail.mit.edu, pl@csail.mit.edu
Reminder Subject:
TALK: A Predictable Unification Algorithm for Coq Featuring Universe Polymorphism and Overloading
Unification is a core component of every proof assistant or programming language featuring dependent types. In many cases, it must deal with higher-order problems up to conversion. Since unification in such conditions is undecidable, unification algorithms may include several heuristics to solve common problems. However, when the stack of heuristics grows large, the result and complexity of the algorithm can become unpredictable.
We present a full description of a new unification algorithm for the Calculus of Inductive Constructions (the base logic of Coq), including universe polymorphism, canonical structures (the overloading mechanism baked into Coqs unification), and a small set of useful heuristics. We implemented our algorithm, and tested it on several libraries, providing evidence that the selected set of heuristics suffices for large developments.
Joint work with Beta Ziliani (MPI Saarbrucken)
Research Areas:
Impact Areas:
Created by Adam Chlipala at Sunday, April 26, 2015 at 8:09 PM.