Records are finite functions from keys to values. In this work we
focus on two main distinct usages of records: structs and maps. The
former associate different keys to values of different types, they are
accessed by providing nominal keys, and trying to access a
non-existent key yields an error. The latter associate all keys to
values of the same type, they are accessed by providing expressions
that compute a key, and trying to access a non-existent key usually
yields some default value such as \texttt{Null} or \texttt{nil}. Here, we propose a
type theory that covers both kinds of usage, where record \emph{types}
may associate to different types either single keys (as for structs)
or sets of keys (as for maps) and where the same
record \emph{expression} can be accessed and used both in the
struct-like style and in the map-like style we just described. Since
we target dynamically-typed languages our type theory includes union
and intersection types, characterized by a subtyping relation. We
define the subtyping relation for our record types via a semantic
interpretation and derive the decomposition rules to decide it, define
a backtracking-free subtyping algorithm that we prove to be correct,
and provide a canonical representation for record types that is used
to define various type operators needed to type record operations such
as selection, concatenation, and field deletion.

Giuseppe Castagna is a researcher at the French National Centre for Scientific Research (CNRS). In 1994, he received a PhD degree in theoretical computer science from the University Paris 7. The same year he was appointed research scientists at the Computer Science Laboratory of the École Normale Supérieure de Paris where, since 2001, he directed the “Programming Languages” group. In 2006, he was appointed senior research scientist and posted at the Institut de Recherche en Informatique Fondamentale (IRIF: Research Institute on the Foundations of Computer Science) of the Université Paris Cité. He is the director of IRIF since January 2023 after having served as deputy director for 5 years.

His main research interests and contributions are in the definition, design, and implementation of type systems for programming languages.