Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
  Lokale TagsFreigabegeschichteDetailsÜbersicht

Freigegeben
Bericht

Proof normalization and subject reduction in extensions of Fsub

MPG-Autoren

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

Externe Ressourcen
Es sind keine externen Ressourcen hinterlegt
Volltexte (beschränkter Zugriff)
Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.
Volltexte (frei zugänglich)

95-2-001.pdf
(beliebiger Volltext), 206KB

Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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.


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-0014-A1CC-6
Zusammenfassung
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.