Skip to main content

All Questions

14 votes
2 answers
136 views

Formal description of algorithmic subtyping/cumulativity

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 ...
ionchy's user avatar
  • 1,026