Publication Details

A Calculus of Coercive Subtyping

KOLLÁR Matej, PETERKA Ondřej, RYŠAVÝ Ondřej and ŠKARVADA Libor. A Calculus of Coercive Subtyping. Brno: Masaryk University, 2009.
Czech title
A Calculus of Coercive Subtyping
Type
technical report
Language
english
Authors
Kollár Matej (FI MUNI)
Peterka Ondřej, Ing. (DIFS FIT BUT)
Ryšavý Ondřej, doc. Ing., Ph.D. (DIFS FIT BUT)
Škarvada Libor, RNDr. (FI MUNI)
URL
Keywords

type systems, subtyping, dependent types

Abstract

This report deals with a type system that merges subtyping and dependent types. We define a calculus that instead of term overloading employs coercion mappings. This enables to detach the subtyping from other parts of the calculus, so that the mutual dependence between subtyping, typing and kinding can be reduced. We analyze basic properties of the calculus and show several examples that demonstrate the mechanism of coercive subtyping.

Published
2009
Pages
17
Publisher
Masaryk University
Place
Brno, CZ
BibTeX 
@TECHREPORT{FITPUB8212,
   author = "Matej Koll\'{a}r and Ond\v{r}ej Peterka and Ond\v{r}ej Ry\v{s}av\'{y} and Libor \v{S}karvada",
   title = "A Calculus of Coercive Subtyping",
   pages = 17,
   year = 2009,
   location = "Brno, CZ",
   publisher = "Masaryk University",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8212"
}
Back to top