SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Wed 18 Nov 2020 08:00 - 08:20 at OOPSLA/ECOOP - W-1
Wed 18 Nov 2020 20:00 - 20:20 at OOPSLA/ECOOP - W-1

The Amber rules are well-known and widely used for subtyping iso-recursive types. They were first briefly and informally introduced in 1985 by Cardelli in a manuscript describing the Amber language. Despite their use over many years, important aspects of the metatheory of the iso-recursive style Amber rules have not been studied in depth or turn out to be quite challenging to formalize. This paper aims to revisit the problem of subtyping iso-recursive types. We start by introducing a novel declarative specification that we believe captures the “spirit” of Amber-style iso-recursive subtyping. Informally, the specification states that two recursive types are subtypes \emph{if all their finite unfoldings are subtypes}. The Amber rules are shown to be sound with respect to this declarative specification. We then derive a \emph{sound}, \emph{complete} and \emph{decidable} algorithmic formulation of subtyping that employs a novel \emph{double unfolding} rule. Compared to the Amber rules, the double unfolding rule has the advantage of: 1) \emph{being modular}; 2) \emph{not requiring reflexivity} to be built in; and 3) leading to an \emph{easy proof of transitivity of subtyping}. This work sheds new insights on the theory of subtyping iso-recursive types, and the new double unfolding rule has important advantages over the original Amber rules for both implementations and metatheoretical studies involving recursive types. All results are mechanically formalized in the Coq theorem prover. Furthermore, as far as we know, this is the first comprehensive treatment of iso-recursive subtyping in a theorem prover, which can deal with \emph{unrestricted} recursive types.

Wed 18 Nov
Times are displayed in time zone: Central Time (US & Canada) change

07:00 - 08:20: W-1OOPSLA at OOPSLA/ECOOP +12h
07:00 - 07:20
Talk
OOPSLA
Breanna Devore-McDonaldUniversity of Massachusetts Amherst, Emery BergerUniversity of Massachusetts Amherst
07:20 - 07:40
Talk
OOPSLA
Tongtong XiangUniversity of Waterloo, Jeff LuoUniversity of Waterloo, Werner DietlUniversity of Waterloo, Canada
07:40 - 08:00
Talk
OOPSLA
Joshua CluneCarnegie Mellon University, Vijay RamamurthyCarnegie Mellon University, Ruben MartinsCarnegie Mellon University, Umut A. AcarCarnegie Mellon University, USA
08:00 - 08:20
Talk
OOPSLA
Yaoda ZhouThe University of Hong Kong, Bruno C. d. S. OliveiraThe University of Hong Kong, Hong Kong, Jinxu ZhaoThe University of Hong Kong
19:00 - 20:20: W-1OOPSLA at OOPSLA/ECOOP
19:00 - 19:20
Talk
OOPSLA
Breanna Devore-McDonaldUniversity of Massachusetts Amherst, Emery BergerUniversity of Massachusetts Amherst
19:20 - 19:40
Talk
OOPSLA
Tongtong XiangUniversity of Waterloo, Jeff LuoUniversity of Waterloo, Werner DietlUniversity of Waterloo, Canada
19:40 - 20:00
Talk
OOPSLA
Joshua CluneCarnegie Mellon University, Vijay RamamurthyCarnegie Mellon University, Ruben MartinsCarnegie Mellon University, Umut A. AcarCarnegie Mellon University, USA
20:00 - 20:20
Talk
OOPSLA
Yaoda ZhouThe University of Hong Kong, Bruno C. d. S. OliveiraThe University of Hong Kong, Hong Kong, Jinxu ZhaoThe University of Hong Kong