Detail publikace

A Calculus of Coercive Subtyping

KOLLÁR, M. PETERKA, O. RYŠAVÝ, O. ŠKARVADA, L.

Originální název

A Calculus of Coercive Subtyping

Typ

zpráva odborná

Jazyk

angličtina

Originální 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

Autoři

KOLLÁR, M.; PETERKA, O.; RYŠAVÝ, O.; ŠKARVADA, L.

Vydáno

28. 2. 2009

Nakladatel

Masaryk University

Místo

Brno

Strany počet

17

URL

https://www.fit.vut.cz/research/publication/8212/

BibTex

@techreport{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",
  publisher="Masaryk University",
  address="Brno",
  pages="17",
  url="https://www.fit.vut.cz/research/publication/8212/"
}

Dokumenty

FIMU-RS-2009-11.pdf