Publication result detail

A Calculus of Coercive Subtyping

ŠKARVADA, L.; PETERKA, O.; RYŠAVÝ, O.; KOLÁŘ, D.

Original Title

A Calculus of Coercive Subtyping

English Title

A Calculus of Coercive Subtyping

Type

Paper in proceedings outside WoS and Scopus

Original 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.

English 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

Key words in English

type theory, lambda calculus,coercive subtyping

Authors

ŠKARVADA, L.; PETERKA, O.; RYŠAVÝ, O.; KOLÁŘ, D.

Released

18.11.2009

Publisher

Seton Hall University

Location

South Orange

Book

Draft Proceedings of the 21st International Symposium on Implementation and Application of Functional Languages

Edition

SHU-TR-CS-2009-09-01

Pages from

182

Pages to

192

Pages count

11

URL

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

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/"
}

Documents

ifl_09_slides
oops_09_subfamilies