Result Details

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.
Type
report
Language
English
Authors
Kollár Matej, Mgr.
Peterka Ondřej, Ing., DIFS (FIT)
Ryšavý Ondřej, doc. Ing., Ph.D., DIFS (FIT)
Škarvada Libor
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.

Keywords

type systems, subtyping, dependent types

URL
Published
2009
Pages
17
Publisher
Masaryk University
Place
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/"
}
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
Research groups
NES@FIT - Networks and distributed systems research group (RG NES@FIT)
Departments
Department of Information Systems (DIFS)
Back to top