Reference. Parametric Subtyping for Structural Parametric Polymorphism
We study the interaction of structural subtyping with parametric polymorphism and recursively defined type constructors. Although structural subtyping is undecidable in this setting, we describe a notion of parametricity for type constructors and then exploit it to define parametric subtyping , a conceptually simple, decidable, and expressive fragment of structural subtyping that strictly generalizes rigid subtyping . We present and prove correct an effective saturation-based decision procedure for parametric subtyping, demonstrating its applicability using a variety of examples. We also provide an implementation of this decision procedure as an artifact.
Cite
Cites 83 works (1 here)
With notes (1)
Session Types as Intuitionistic Linear Propositions caires-2010-session
External (82)
- Parameterized Algebraic Protocols (2023)
- Subtyping Context-Free Session Types (2023)
- Recursive Subtyping for All (2023)
- Parametric Subtyping for Structural Parametric Polymorphism (arXiv extended version) (2023)
- Parametric Subtyping for Structural Parametric Polymorphism (Artifact) (2023)
- Standard ML Implementation of Parametric Subtyping Decision Procedure (2023)
- Polymorphic lambda calculus with context-free session types (2022)
- Bouncing Threads for Circular and Non-Wellfounded Proofs (2022)
- Nested Session Types (2022)
- The Different Shades of Infinite Session Types (2022)
- Polarized Subtyping (2022)
- Equivalence of pushdown automata via first-order grammars (2021)
- PARAMETRICITY FOR PRIMITIVE NESTED TYPES AND GADTS (2021)
- Subtyping on Nested Polymorphic Session Types (2021)
- Syntactically Restricting Bounded Polymorphism for Decidable Subtyping (2020)
- Deciding the Bisimilarity of Context-Free Session Types (2020)
- Practical Subtyping for Curry-Style Languages (2019)
- Context-Free Session Type Inference (2019)
- On Subtyping-Relation Completeness, with an Application to Iso-Recursive Types (2017)
- Well-founded recursion with copatterns and sized types (2016)
- Polymorphism, subtyping, and type inference in MLsub (2016)
- Java generics are turing complete (2016)
- Type soundness for dependent object types (DOT) (2016)
- Context-free session types (2016)
- Getting F-bounded polymorphism into shape (2014)
- Sequent calculi for induction and infinite descent (2010)
- Subtyping, Declaratively (2010)
- Logical Step-Indexed Logical Relations (2009)
- On Decidability of Nominal Subtyping with Variance (2007)
- Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types (2006)
- A gentle introduction to semantic subtyping (2005)
- Practical Refinement-Type Checking (2005)
- Subtyping for session types in the pi calculus (2005)
- Semantics of Types for Mutable State (2004)
- Tridirectional typechecking (2004)
- Semantic subtyping (2002)
- Types and Programming Languages (2002)
- The Subtyping Problem for Second-Order Types Is Undecidable (2002)
- An indexed model of recursive types for foundational proof-carrying code (2001)
- Call-By-Push-Value (Ph.D. dissertation, University of London) (2001)
- An Introduction to Decidability of DPDA Equivalence (2001)
- L(A)=L(B)? decidability results from complete formal systems (2001)
- Decidability of DPDA equivalence (2001)
- Generalizing generalized tries (2000)
- Polarized Higher-Order Subtyping (1999)
- Nested datatypes (1998)
- Coinductive Axiomatization of Recursive Type Equality and Subtyping (1998)
- Language primitives and type discipline for structured communication-based programming (1998)
- Datatypes and Subtyping (1998)
- Regular Böhm trees (1998)
- Some Decision Problems for ML Refinement Types (1997)
- An interpretation of objects and object types (1996)
- Putting type annotations to work (1996)
- A generalization of the trie data structure (1995)
- The Undecidability of Mitchell’s Subtyping Relationship (1995)
- An Extension of System F with Subtyping (1994)
- Decidable bounded quantification (1994)
- Undecidable Equivalences for Basic Process Algebra (1994)
- Bounded Quantification Is Undecidable (1994)
- Subtyping recursive types (1993)
- Decidability of bisimulation equivalence for process generating context-free languages (1993)
- Completely Bounded Quantification Is Decidable (1992)
- Refinement types for ML (1991)
- Theorems for free! (1989)
- Structural subtyping and the notion of power type (1988)
- Constraint logic programming (1987)
- Amber (1986)
- On understanding types, data abstraction, and polymorphism (1985)
- Three approaches to type structure (1985)
- Process algebra for synchronous communication (1984)
- A semantics of multiple inheritance (1984)
- Polymorphic type schemes and recursive definitions (1984)
- Types, Abstraction and Parametric Polymorphism (1983)
- An Efficient Unification Algorithm (1982)
- Recursive Type Operators Which Are More Than Type Schemes (1979)
- Type definitions with parameters (1978)
- The inclusion problem for simple languages (1976)
- Résolution d'Équations dans des Langages d'Ordre 1, 2, ..., ω (Ph.D. dissertation) (1976)
- Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur (1972)
- Simple deterministic languages (1966)
- A New Normal-Form Theorem for Context-Free Phrase Structure Grammars (1965)
- A Machine-Oriented Logic Based on the Resolution Principle (1965)