English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Report

Proof normalization and subject reduction in extensions of Fsub

MPS-Authors

Vorobyov,  Sergei
Programming Logics, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)

95-2-001.pdf
(Any fulltext), 206KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Vorobyov, S.(1995). Proof normalization and subject reduction in extensions of Fsub (MPI-I-1995-2-001). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-A1CC-6
Abstract
System Fsub, the second-order polymorphic typed lambda-calculus with subtyping [Cardelli-Wegner, 85], [Bruce-Longo, 90], [Curien-Ghelli, 92], appeared to be undecidable because of the undecidability of its subtyping component [Pierce, 92]. The discovery of decidable extensions of the Fsub-subtyping relation [Vorobyov 94] put forward a challenging problem of incorporating these extensions into an Fsub-like typing in a decidable and coherent manner. In this paper we describe a family of systems combining the standard Fsub-typing rules with converging hierarchies of decidable extensions of the Fsub-subtyping and give decidable criteria for successful proof normalization and subject reduction.