Technical Reports

A List by Author: Matej Kollár


A Calculus of Coercive Subtyping

by Matej Kollár, Ondřej Peterka, Ondřej Ryšavý, Libor Škarvada, November 2009, 17 pages.

FIMU-RS-2009-11. Available as Postscript, PDF.


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.

Responsible contact:

Please install a newer browser for this site to function properly.

More information