Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
  Lokale TagsFreigabegeschichteDetailsÜbersicht

Freigegeben
Konferenzbeitrag

Fa with Recursive Types: "Types-as-Propositions" Interpretations in M. Rabin's S2S

MPG-Autoren
/persons/resource/persons45677

Vorobyov,  Sergei
Computational Biology and Applied Algorithmics, MPI for Informatics, Max Planck Society;
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)
Es sind keine frei zugänglichen Volltexte in PuRe verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Vorobyov, S. (1995). Fa with Recursive Types: "Types-as-Propositions" Interpretations in M. Rabin's S2S. In Proceedings of JFLA'95: Journées Francophones des Langages Applicatifs (pp. 49-73). Rocquencourt, France: INRIA.


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-0014-AD00-C
Zusammenfassung
Subtyping judgments of the polymorphic second-order typed
lambda-calculus Fsub extended by recursive types and different known
inference rules for these types could be interpreted in S2S, M.Rabin's
monadic second-order theory of two successor functions. On the one hand,
this provides a comprehensible model of the parametric and inheritance
polymorphisms over recursive types, on the other, proves that the
corresponding subtyping theories are not essentially undecidable, i.e.,
possess consistent decidable extensions.