14
$\begingroup$

Are there any references (papers, documentation, etc.) for how proof assistants with subtyping due to cumulativity actually implement algorithmic subtyping? Coq, for instance, has subtyping, but the manual's description doesn't seem to be complete (e.g. you wouldn't be able to derive (λ_: Prop. Set) True ≤ (λ_: Prop. Type) True from what it lists alone), and refers to transitivity, which as a rule wouldn't be algorithmic anyway, I don't think. The only other proof assistant I know with cumulativity is Arend, but their docs don't detail rules either. (Are there more?)

I've seen formal descriptions of subtyping and their derivation rules in papers like pCuIC and the ones it cites, but they all seem to include some form of a transitivity rule (either A ≼ B ≼ C or A ≈ B ≼ C ≈ D). I'm particularly interested in an algorithmic presentation that's known to be sound wrt these usual presentations of subtyping with a transitivity rule.

Improve this question
$\endgroup$

2 Answers 2

Reset to default
5
$\begingroup$

For more recent references for, you can look at what MetaCoq does, either the code (there’s now a proof of correctness and completeness of an actual checker wrt. a declarative spec) or the papers (the ones around are starting to be quite behind the formalization, hopefully there will be a new one soon).

Improve this answer
$\endgroup$
2
  • $\begingroup$ Neat! I'm guessing you're referring to this: metacoq.github.io/html/MetaCoq.PCUIC.PCUICTyping.html#lab96; I can't find this declarative spec you're referring to though, which definition is that? $\endgroup$
    – ionchy
    Commented Feb 10, 2022 at 4:52
  • 1
    $\begingroup$ Ah sorry, I should have been more precise: the active development branch is currently coq.8.14. The declarative spec is here, it is proven equivalent to the one you’ve found (now named CumulAlgo) here, and the certified conversion checker is here. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Feb 10, 2022 at 8:36
8
$\begingroup$

See Universe Polymorphism in Coq (ITP 2014) by Matthieu Sozeau and Nicolas Tabareau (freely available draft) which explains in detail what Coq is doing.

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.