Subtyping Recursive Games

Using methods drawn from Game Semantics, we build a sound and computationally adequate model of a simple calculus that includes both subtyping and recursive types. Our model solves recursive type equations up to equality, and is shown to validate a subtyping rule for recursive types proposed by Amadio and Cardelli.

• Type: Conference
• Year: 2001
• Where: TLCA
• Authors: Juliusz Chroboczek
• Keywords: Recursive Type Equations, Recursive Types, Subtyping, Theoretical Computer Science, TLCA 2001