Universe Polymorphism in Coq

By Matthieu Sozeau, N. Tabareau. 2014

66 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Hardware and Architecture

Citations in the corpus

• Heterogeneous substitution systems revisited (2016, neutral): “The proof assistant Coq has recently gained a form of universe polymorphism [28].”