SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Wed 18 Nov 2020 08:00 - 08:20 at SPLASH-I - W-1 Chair(s): Karim Ali, Sophia Drossopoulou
Wed 18 Nov 2020 20:00 - 20:20 at SPLASH-I - W-1 Chair(s): Patrick Lam, Julia Belyakova

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) 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.

Conference Day
Wed 18 Nov

Displayed time zone: Central Time (US & Canada) change

07:00 - 08:20
W-1OOPSLA at SPLASH-I +12h
Chair(s): Karim AliUniversity of Alberta, Sophia DrossopoulouImperial College London
07:00
20m
Talk
Mossad: Defeating Software Plagiarism Detection
OOPSLA
Breanna Devore-McDonaldUniversity of Massachusetts at Amherst, Emery D. BergerUniversity of Massachusetts at Amherst
Link to publication DOI Media Attached
07:20
20m
Talk
Precise Inference of Expressive Units of Measurement Types
OOPSLA
Tongtong XiangUniversity of Waterloo, Jeff Y. LuoUniversity of Waterloo, Werner DietlUniversity of Waterloo
Link to publication DOI Media Attached
07:40
20m
Talk
Program Equivalence for Assisted Grading of Functional Programs
OOPSLA
Joshua CluneCarnegie Mellon University, Vijay RamamurthyCarnegie Mellon University, Ruben MartinsCarnegie Mellon University, Umut A. AcarCarnegie Mellon University
Link to publication DOI Media Attached
08:00
20m
Talk
Revisiting Iso-Recursive Subtyping
OOPSLA
Yaoda ZhouUniversity of Hong Kong, Bruno C. d. S. OliveiraUniversity of Hong Kong, Jinxu ZhaoUniversity of Hong Kong
Link to publication DOI Media Attached
19:00 - 20:20
W-1OOPSLA at SPLASH-I
Chair(s): Patrick LamUniversity of Waterloo, Julia BelyakovaNortheastern University
19:00
20m
Talk
Mossad: Defeating Software Plagiarism Detection
OOPSLA
Breanna Devore-McDonaldUniversity of Massachusetts at Amherst, Emery D. BergerUniversity of Massachusetts at Amherst
Link to publication DOI Media Attached
19:20
20m
Talk
Precise Inference of Expressive Units of Measurement Types
OOPSLA
Tongtong XiangUniversity of Waterloo, Jeff Y. LuoUniversity of Waterloo, Werner DietlUniversity of Waterloo
Link to publication DOI Media Attached
19:40
20m
Talk
Program Equivalence for Assisted Grading of Functional Programs
OOPSLA
Joshua CluneCarnegie Mellon University, Vijay RamamurthyCarnegie Mellon University, Ruben MartinsCarnegie Mellon University, Umut A. AcarCarnegie Mellon University
Link to publication DOI Media Attached
20:00
20m
Talk
Revisiting Iso-Recursive Subtyping
OOPSLA
Yaoda ZhouUniversity of Hong Kong, Bruno C. d. S. OliveiraUniversity of Hong Kong, Jinxu ZhaoUniversity of Hong Kong
Link to publication DOI Media Attached