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

Vorobyov, Sergei

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

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

MPS-Authors

/persons/resource/persons45677

Vorobyov, Sergei
Computational Biology and Applied Algorithmics, MPI for Informatics, Max Planck Society;
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)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

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.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-AD00-C

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.