Hostname: page-component-745bb68f8f-cphqk Total loading time: 0 Render date: 2025-01-12T10:17:39.541Z Has data issue: false hasContentIssue false
  • English
  • Français

Recursive subtyping revealed

Published online by Cambridge University Press:  06 November 2002

VLADIMIR GAPEYEV ,
MICHAEL Y. LEVIN  and
BENJAMIN C. PIERCE
VLADIMIR GAPEYEV
Affiliation:
Department of Computer & Information Science, University of Pennsylvania, 200 South 33rd Street, Philadelphia, PA 19104-6389, USA
MICHAEL Y. LEVIN
Affiliation:
Department of Computer & Information Science, University of Pennsylvania, 200 South 33rd Street, Philadelphia, PA 19104-6389, USA
BENJAMIN C. PIERCE
Affiliation:
Department of Computer & Information Science, University of Pennsylvania, 200 South 33rd Street, Philadelphia, PA 19104-6389, USA
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Algorithms for checking subtyping between recursive types lie at the core of many programming language implementations. But the fundamental theory of these algorithms and how they relate to simpler declarative specifications is not widely understood, due in part to the difficulty of the available introductions to the area. This tutorial paper offers an ‘end-to-end’ introduction to recursive types and subtyping algorithms, from basic theory to efficient implementation, set in the unifying mathematical framework of coinduction.

Type
Research Article
Information
Journal of Functional Programming , Volume 12 , Issue 6 , November 2002 , pp. 511 - 548
Copyright
© 2002 Cambridge University Press

Footnotes

This article also appears as chapter 21 of Types and Programming Languages by Benjamin C. Pierce (MIT Press, 2002).
Submit a response

Discussions

No Discussions have been published for this article.