Wed 18 Jan 2023 11:35 - 12:00 at Avenue34 - Types I Chair(s): Neel Krishnaswami

Recursive types and bounded quantification are prominent features in many modern programming languages, such as Java, C#, Scala or TypeScript. Unfortunately, the interaction between recursive types, bounded quantification and subtyping has shown to be problematic in the past. Consequently, defining a simple foundational calculus that combines those features and has desirable properties, such as \emph{decidability}, \emph{transitivity} of subtyping, \emph{conservativity} and a sound and complete algorithmic formulation has been a long time challenge.

This paper presents an extension of $\textrm{kernel}~F_{\le}$, called $F_{\le}^{\mu}$, with iso-recursive types. $F_\le$ is a well-known polymorphic calculus with bounded quantification. In $F_{\le}^{\mu}$ we add iso-recursive types, and correspondingly extend the subtyping relation with iso-recursive subtyping using the recently proposed nominal unfolding rules. We also add two smaller extensions to $F_\le$. The first one is a generalization of the $\textrm{kernel}~F_{\le}$ rule for bounded quantification that accepts \emph{equivalent} rather than \emph{equal} bounds. The second extension is the use of so-called \emph{structural} folding/unfolding rules, inspired by the structural unfolding rule proposed by Abadi, Cardelli, and Viswanathan [1996]. The structural rules add expressive power to the more conventional folding/unfolding rules in the literature, and they enable additional applications. We present several results, including: type soundness; transitivity and decidability of subtyping; the conservativity of $F_{\le}^{\mu}$ over $F_\le$; and a sound and complete algorithmic formulation of $F_{\le}^{\mu}$. Moreover, we study an extension of $F_{\le}^{\mu}$, called $F_{\le\ge}^{\mu}$, which includes \emph{lower bounded quantification} in addition to the conventional (upper) bounded quantification of $F_\le$. All the results in this paper have been formalized in the Coq theorem prover.

#### Wed 18 JanDisplayed time zone: Eastern Time (US & Canada) change

 10:45 - 12:00 Types IPOPL at Avenue34 Chair(s): Neel Krishnaswami University of Cambridge 10:4525mTalk Higher-Order Leak and Deadlock Free LocksDistinguished PaperPOPLJules Jacobs Radboud University Nijmegen, Stephanie Balzer Carnegie Mellon University DOI 11:1025mTalk Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited ContinuationsPOPLTaro Sekiyama National Institute of Informatics, Hiroshi Unno University of Tsukuba; RIKEN AIP DOI 11:3525mTalk Recursive Subtyping for AllPOPLLitao Zhou University of Hong Kong, Yaoda Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI