Output details
11 - Computer Science and Informatics
Royal Holloway, University of London
Return to search
Output 0 of 0 in the submission
Article title
Coercive subtyping: theory and implementation
Type
D - Journal article
Title of journal
Information and Computation
Article number
-
Volume number
223
Issue number
-
First page of article
18
ISSN of journal
0890-5401
Year of publication
2013
Number of additional authors
2
Additional information
<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.
Interdisciplinary
-
Cross-referral requested
-
Research group
C - Centre for Software Language Engineering
Citation count
2
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
