Publication Details
A Calculus of Coercive Subtyping
ŠKARVADA Libor, PETERKA Ondřej, RYŠAVÝ Ondřej and KOLÁŘ Dušan. A Calculus of Coercive Subtyping. In: 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, pp. 182-192.
Czech title
Jazyk s podtypováním na bázi koercí
Type
conference paper
Language
english
Authors
Škarvada Libor, RNDr. (FI MUNI)
Peterka Ondřej, Ing. (DIFS FIT BUT)
Ryšavý Ondřej, doc. Ing., Ph.D. (DIFS FIT BUT)
Kolář Dušan, doc. Dr. Ing. (DIFS FIT BUT)
Peterka Ondřej, Ing. (DIFS FIT BUT)
Ryšavý Ondřej, doc. Ing., Ph.D. (DIFS FIT BUT)
Kolář Dušan, doc. Dr. Ing. (DIFS FIT BUT)
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
Conference
21st Symposium on Implementation and Application of Functional Languages, South Orange, NJ, US
Publisher
Seton Hall University
Place
South Orange, US
BibTeX
@INPROCEEDINGS{FITPUB9111, author = "Libor \v{S}karvada and Ond\v{r}ej Peterka and Ond\v{r}ej Ry\v{s}av\'{y} and Du\v{s}an Kol\'{a}\v{r}", title = "A Calculus of Coercive Subtyping", pages = "182--192", booktitle = "Draft Proceedings of the 21st International Symposium on Implementation and Application of Functional Languages", series = "SHU-TR-CS-2009-09-01", year = 2009, location = "South Orange, US", publisher = "Seton Hall University", language = "english", url = "https://www.fit.vut.cz/research/publication/9111" }