Atlas home || Conferences | Abstracts | about Atlas

First St.Petersburg Days of Logic and Computability
May 26-29, 1999
Steklov Institute of Mathematics
St. Petersburg, Russia

Organizers
Evgeny Dantsin, Gennadii Davydov, Dima Grigoriev, Eduard Karavaev, Nickolai Kossovskii, Vladimir Lifschitz, Maurice Margenstern, Yuri Matiyasevich (chairman), Grigori Mints, Vladimir Orevkov, Anatol Slissenko, Maxim Vsemirnov

View Abstracts
Conference Homepage

Coercion completion and conservativity in coercive subtyping
by
Sergei Soloviev
Université Paul Sabatier, Toulouse, IRIT
Coauthors: Zhaohui Luo (University of Durham, U.K.)

Coercive subtyping offers a general approach to subtyping and inheritance by introducing a simple abbreviational mechanism to constructive type theories. (Coercions are functions that represent the ``conversion'' of the elements of a subtype into the elements of its supertype.) In this paper, we study coercion completion in coercive subtyping for dependent type systems and prove that the formal extension with coercive subtyping of a type theory such as Martin-Löf's type theory and UTT is a conservative extension. The importance of coherence conditions for the conservativity result is discussed. Coercive subtyping mechanisms are used in some interactive proof-development systems, such as a version of Lego implemented at Durham University.

http://www.irit.fr/~Sergei.Soloviev/types.ps.gz

Date received: March 30, 1999

Copyright © 1999 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # cacs-23.