SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Fri 9 Dec 2022 11:30 - 12:00 at Seminar Room LG004 - OOPSLA Papers Chair(s): Manas Thakur

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 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 sound, complete and decidable algorithmic formulation of subtyping that employs a novel double unfolding rule. Compared to the Amber rules, the double unfolding rule has the advantage of: 1) being modular; 2) not requiring reflexivity to be built in; and 3) leading to an 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. As far as we know, this is the first comprehensive treatment of iso-recursive subtyping dealing with unrestricted recursive types in a theorem prover.

Fri 9 Dec

Displayed time zone: Auckland, Wellington change

10:30 - 12:30
OOPSLA PapersCOVID Time Papers In Person at Seminar Room LG004
Chair(s): Manas Thakur IIT Bombay
10:30
30m
Talk
Label dependent lambda calculus and gradual typing
COVID Time Papers In Person
Weili Fu University of Freiburg, Germany, Fabian Krause University of Freiburg, Peter Thiemann University of Freiburg, Germany
Link to publication DOI
11:00
30m
Talk
Modular Specification and Verification of Closures in Rust
COVID Time Papers In Person
Fabian Wolff , Aurel Bílý ETH Zurich, Christoph Matheja ETH Zurich, Peter Müller ETH Zurich, Alexander J. Summers University of British Columbia
Link to publication DOI
11:30
30m
Talk
Revisiting Iso-Recursive SubtypingVirtual
COVID Time Papers In Person
Yaoda Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Jinxu Zhao University of Hong Kong
Link to publication DOI
12:00
30m
Talk
Symbolic value-flow static analysis: deep, precise, complete modeling of Ethereum smart contracts
COVID Time Papers In Person
Yannis Smaragdakis University of Athens, Neville Grech University of Malta, Sifis Lagouvardos University of Athens, Konstantinos Triantafyllou ETH Zurich, Ilias Tsatiris University of Athens
Link to publication DOI