English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
  Fsub with Recursive Types: `Types-as-Propositions' Interpretations M. Rabin's S2S

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

Item is

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Vorobyov, Sergei1, 2, Author           
Affiliations:
1Computational Biology and Applied Algorithmics, MPI for Informatics, Max Planck Society, ou_40046              
2Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 Abstract: 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.

Details

show
hide
Language(s): eng - English
 Dates: 2010-03-121995
 Publication Status: Issued
 Pages: -
 Publishing info: Rocquencourt, France : INRIA
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519617
Other: Local-ID: C1256104005ECAFC-D7347E97BF1DBC85C125615F0036C2F9-Vorobyov94b
 Degree: -

Event

show
hide
Title: Untitled Event
Place of Event: Bois d'Amont, France
Start-/End Date: 1995

Legal Case

show

Project information

show

Source 1

show
hide
Title: Proceedings of JFLA'95: Journées Francophones des Langages Applicatifs (JFLA'95)
Source Genre: Proceedings
 Creator(s):
Affiliations:
Publ. Info: Rocquencourt, France : INRIA
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 49 - 73 Identifier: -