MPI-INF Logo
MPI-INF/SWS Research Reports 1991-2021

2. Number - only D2

MPI-I-95-2-001

Proof normalization and subject reduction in extensions of Fsub

Vorobyov, Sergei

January 1995, 18 pages.

.
Status: available - back from printing

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.

  • 95-2-001.pdf95-2-001.pdfMPI-I-95-2-001.dvi.Z
  • Attachement: MPI-I-95-2-001.dvi.Z (52 KBytes); 95-2-001.pdf (205 KBytes)

URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1995-2-001

Hide details for BibTeXBibTeX
@TECHREPORT{Vorobyov95-RR-2-001,
  AUTHOR = {Vorobyov, Sergei},
  TITLE = {Proof normalization and subject reduction in extensions of Fsub},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-95-2-001},
  MONTH = {January},
  YEAR = {1995},
  ISSN = {0946-011X},
}