Proof normalization and subject reduction in extensions of Fsub

Vorobyov, Sergei

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Report

Proof normalization and subject reduction in extensions of Fsub

MPS-Authors

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

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

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: https://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.