APLAS 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
co-located with SPLASH 2022
Mon 5 Dec 2022 16:30 - 17:00 at Seminar Room G007 - Types Chair(s): Atsushi Igarashi

Calculi with subtyping, a form of record concatenation and recursive types are useful to model objects with multiple inheritance. Surprisingly, almost no existing calculi supports the three features together, partly because the combination of subtyping and record concatenation is already known to be troublesome. Recently, a line of work on \emph{disjoint intersection types} with a \emph{merge operator} has emerged as a new approach to deal with the interaction between subtyping and record concatenation. However, the addition of recursive types has not been studied.

In this paper we present a calculus that combines \emph{iso-recursive types} with disjoint intersection types and a merge operator. The merge operator generalizes symmetric record concatenation, and the calculus supports subtyping as well as recursive types. We build on recent developments on the theory of iso-recursive subtyping using the so-called \emph{nominal unfolding} rules to add iso-recursive types to a calculus with disjoint intersection types and a merge operator. The main challenge lies in the disjointness definition with iso-recursive subtyping. We show the type soundness of the calculus, decidability of subtyping, as well as the soundness and completeness of our disjointness definition. All the proofs are mechanized in the Coq theorem prover.

Mon 5 Dec

Displayed time zone: Auckland, Wellington change

15:30 - 17:30
TypesAPLAS at Seminar Room G007
Chair(s): Atsushi Igarashi Kyoto University
15:30
30m
Talk
Characterizing functions mappable over GADTs
APLAS
Patricia Johann Appalachian State University, Pierre Cagne Appalachian State University
16:00
30m
Talk
Applicative Intersection Types
APLAS
Xu Xue University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Ningning Xie University of Toronto
16:30
30m
Talk
A Calculus with Recursive Types, Record Concatenation and Subtyping
APLAS
Yaoda Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Andong Fan Hong Kong University of Science and Technology
17:00
30m
Talk
Novice Type Error Diagnosis with Natural Language Models
APLAS
Chuqin Geng McGill University, Haolin Ye McGill University, Yixuan Li McGill University, Tianyu Han McGill University, Brigitte Pientka McGill University, Xujie Si McGill University, Canada