Detail výsledku

A Calculus of Coercive Subtyping

KOLLÁR, M.; PETERKA, O.; RYŠAVÝ, O.; ŠKARVADA, L. A Calculus of Coercive Subtyping. Brno: Masaryk University, 2009. 17 p.
Typ
zpráva odborná
Jazyk
anglicky
Autoři
Kollár Matej, Mgr.
Peterka Ondřej, Ing., UIFS (FIT)
Ryšavý Ondřej, doc. Ing., Ph.D., UIFS (FIT)
Škarvada Libor
Abstrakt

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.

Klíčová slova

type systems, subtyping, dependent types

URL
Rok
2009
Strany
17
Vydavatel
Masaryk University
Místo
Brno
BibTeX 
@misc{BUT191871,
  author="Matej {Kollár} and Ondřej {Peterka} and Ondřej {Ryšavý} and Libor {Škarvada}",
  title="A Calculus of Coercive Subtyping",
  year="2009",
  pages="17",
  publisher="Masaryk University",
  address="Brno",
  url="https://www.fit.vut.cz/research/publication/8212/"
}
Soubory
Projekty
Typový systém s hodnotově-závislými typy pro objektově-orientované programovací jazyky, GAČR, Standardní projekty, GA201/09/1316, zahájení: 2009-01-01, ukončení: 2009-12-31, ukončen
Výzkumné skupiny
NES@FIT - Výzkumná skupina počítačové sítě (VZ NES@FIT)
Pracoviště
Ústav informačních systémů (UIFS)
Nahoru