Publication Details

A Calculus of Coercive Subtyping

ŠKARVADA, L.; PETERKA, O.; RYŠAVÝ, O.; KOLÁŘ, D. A Calculus of Coercive Subtyping. Draft Proceedings of the 21st International Symposium on Implementation and Application of Functional Languages. SHU-TR-CS-2009-09-01. South Orange: Seton Hall University, 2009. p. 182-192.
Czech title
Jazyk s podtypováním na bázi koercí
Type
conference paper
Language
English
Authors
Škarvada Libor
Peterka Ondřej, Ing.
Ryšavý Ondřej, doc. Ing., Ph.D. (DIFS)
Kolář Dušan, doc. Dr. Ing. (DIFS)
and others
Keywords

type theory, lambda calculus,coercive subtyping

Abstract

Our work that stems, in particular, from the research done by Aspinall and Compagnoni, and Luo attempts to provide a framework for systematical studying coercive subtyping in dependent type systems. Contrary to Aspinall and Compagnoni we define subtyping based on coercions instead of allowing term overloading. Contrary to Luo we implemented coercive subtyping as direct extension of \lambda P type system instead of introducing definitional mechanism, which is more powerfull but leads to more complicated presentation of a system.

Published
2009
Pages
182–192
Proceedings
Draft Proceedings of the 21st International Symposium on Implementation and Application of Functional Languages
Series
SHU-TR-CS-2009-09-01
Publisher
Seton Hall University
Place
South Orange
BibTeX 
@inproceedings{BUT34397,
  author="Libor {Škarvada} and Ondřej {Peterka} and Ondřej {Ryšavý} and Dušan {Kolář}",
  title="A Calculus of Coercive Subtyping",
  booktitle="Draft Proceedings of the 21st International Symposium on Implementation and Application of Functional Languages",
  year="2009",
  series="SHU-TR-CS-2009-09-01",
  pages="182--192",
  publisher="Seton Hall University",
  address="South Orange",
  url="https://www.fit.vut.cz/research/publication/9111/"
}
Back to top