Output details
11 - Computer Science and Informatics
Royal Holloway, University of London
Coercive subtyping: theory and implementation
<11>This paper studies coercive subtyping as implemented in the proof assistants Coq. Lego, Matita and Plastic. The paper gives the first correct proof of conservativity of the coercive subtyping extension and makes important contributions to the foundations of its implementations and applications. It also shows, systematically for the first time, that the coercive subtyping approach is adequate to modern type theories as used in proof assistants (as opposed to subsumptive subtyping, which is adequate for programming languages but not for MTTs). The work was partially supported by EPSRC grant GR/R84092, EU project 510996 and, in particular, Leverhulme grant F/07-537/AJ.