PLClub Discussion Group

Coq Universes

This is a talk on universes—well, Coq universes, which may be more/less exciting to you than other “universes”. The talk covers parts of the theory side (e.g. how inference works) as well as parts of the practice side (e.g. debugging).

Your homework is: (1) Read Adam Chlipala’s CPDT chapter on universes before the “Axiom” section: http://adam.chlipala.net/cpdt/html/Cpdt.Universes.html (2) (Optional) Send me some examples that you had before with universe inconsistency or other bizarre universe issues, the smaller the better. I might be using them during my talk. There is no guarantee that I will figure out the issues though! :)