Séminaire Cambium, Inria Paris
                                 Amphi Lions
                            Mercredi 28 mai, 10h30

                                  Litao Zhou
                           University of Hong Kong

                         Recursive Subtyping for All

Recursive types are a common feature in type systems, used to model algebraic
data types and recursive objects. A well-known formulation of iso-recursive
subtyping, the Amber rules, was proposed by Amadio and Cardelli in the 1990s.
More recently, alternative formulations have been developed to improve formal
reasoning and efficiency.

This talk reviews these developments and focuses on a new calculus, Fμ≤, which
combines iso-recursive subtyping with bounded quantification by extending the
polymorphic system F≤. I will discuss its key properties, including type
soundness, conservativity, and decidability, and show how it supports advanced
programming features like F-bounded quantification and subtyping between
algebraic data types. All results are formalized in the Rocq proof assistant.

This work, joint with Yaoda Zhou, Qianyong Wan, and Bruno Oliveira, appeared
at POPL 2023, with an extended version recently published in JFP.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.