Result 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.
Type
conference paper
Language
English
Authors
Škarvada Libor
Peterka Ondřej, Ing., FIT (FIT), DIFS (FIT)
Ryšavý Ondřej, doc. Ing., Ph.D., DIFS (FIT)
Kolář Dušan, doc. Dr. Ing., DIFS (FIT)
and others
Peterka Ondřej, Ing., FIT (FIT), DIFS (FIT)
Ryšavý Ondřej, doc. Ing., Ph.D., DIFS (FIT)
Kolář Dušan, doc. Dr. Ing., DIFS (FIT)
and others
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.
Keywords
type theory, lambda calculus,coercive subtyping
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
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/"
}
Files
Projects
Dependent type system for object-oriented programming languages, GACR, Standardní projekty, GA201/09/1316, start: 2009-01-01, end: 2009-12-31, completed
Departments