SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Mon 16 Nov 2020 10:20 - 11:00 at SPLASH-VII - Posters Session 2
Mon 16 Nov 2020 22:20 - 23:00 at SPLASH-VII - Posters Session 2 Mirror

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.

Mon 16 Nov

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

10:20 - 11:00
Posters Session 2Posters at SPLASH-VII +12h
10:20
40m
Poster
Resolution as Intersection Subtyping via Modus PonensOOPSLA
Posters
Koar Marntirosian KU Leuven, Tom Schrijvers KU Leuven, Bruno C. d. S. Oliveira University of Hong Kong, Georgios Karachalias Tweag
10:20
40m
Poster
Macros For Domain-Specific LanguagesOOPSLA
Posters
Michael Ballantyne Northeastern University, Alexis King Northwestern University, Matthias Felleisen Northeastern University
10:20
40m
Poster
Precise Inference of Expressive Units of Measurement TypesOOPSLA
Posters
Tongtong Xiang University of Waterloo, Jeff Y. Luo University of Waterloo, Werner Dietl University of Waterloo
10:20
40m
Poster
Guiding Dynamic Programing via Structural Probability for Accelerating Programming by ExampleOOPSLA
Posters
Ruyi Ji Peking University, Yican Sun Peking University, Yingfei Xiong Peking University, Zhenjiang Hu Peking University
10:20
40m
Poster
A Sparse Iteration Space Transformation Framework for Sparse Tensor AlgebraOOPSLA
Posters
Ryan Senanayake Reservoir Labs, Changwan Hong Massachusetts Institute of Technology, Ziheng Wang Massachusetts Institute of Technology, Amalee Wilson Stanford University, Stephen Chou Massachusetts Institute of Technology, Shoaib Kamil Adobe Research, Saman Amarasinghe Massachusetts Institute of Technology, Fredrik Kjolstad Stanford University
DOI Pre-print Media Attached File Attached
10:20
40m
Poster
Learning Semantic Program Embeddings with Graph Interval Neural NetworkOOPSLA
Posters
Yu Wang Nanjing University, China, Ke Wang Visa Research, Fengjuan Gao Nanjing University, Linzhang Wang Nanjing University
10:20
40m
Poster
Statically Verified Refinements for Multiparty ProtocolsOOPSLA
Posters
Fangyi Zhou Imperial College London, Francisco Ferreira Imperial College London, Raymond Hu University of Hertfordshire, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London
10:20
40m
Poster
Towards a Formal Foundation of Intermittent ComputingOOPSLA
Posters
Milijana Surbatovich Carnegie Mellon University, Brandon Lucia Carnegie Mellon University, Limin Jia Carnegie Mellon University
10:20
40m
Poster
Incremental Predicate Analysis for Regression VerificationOOPSLA
Posters
Qianshan Yu Tsinghua University, Fei He Tsinghua University, Bow-Yaw Wang Academia Sinica
10:20
40m
Poster
StreamQL: A Query Language for Processing Streaming Time SeriesOOPSLA
Posters
Lingkun Kong Rice University, Konstantinos Mamouras Rice University
10:20
40m
Poster
SATUNE: Synthesizing Efficient SAT EncodersOOPSLA
Posters
Hamed Gorjiara University of California at Irvine, Guoqing Harry Xu University of California at Los Angeles, Brian Demsky University of California at Irvine
10:20
40m
Poster
Scaling Exact Inference for Discrete Probabilistic ProgramsOOPSLA
Posters
Steven Holtzen University of California at Los Angeles, Guy Van den Broeck University of California at Los Angeles, Todd Millstein University of California, Los Angeles
10:20
40m
Poster
Certified and Efficient Instruction SchedulingOOPSLA
Posters
Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, Cyril Six Kalray / Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, David Monniaux Grenoble Alps University / CNRS / Grenoble INP / VERIMAG
10:20
40m
Poster
Revisiting Iso-Recursive SubtypingOOPSLA
Posters
Yaoda Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Jinxu Zhao University of Hong Kong
10:20
40m
Poster
Guided Linking: Dynamic Linking Without the CostsOOPSLA
Posters
Sean Bartell University of Illinois at Urbana-Champaign, Will Dietz University of Illinois at Urbana-Champaign, Vikram S. Adve University of Illinois at Urbana-Champaign
10:20
40m
Poster
Unifying Execution of Imperative Generators and Declarative SpecificationsOOPSLA
Posters
Pengyu Nie University of Texas at Austin, Marinela Parovic University of Texas at Austin, Zhiqiang Zang University of Texas at Austin, Sarfraz Khurshid University of Texas at Austin, Aleksandar Milicevic Microsoft, Milos Gligoric University of Texas at Austin
10:20
40m
Poster
CompCertELF: Verified Separate Compilation of C Programs into ELF Object FilesOOPSLA
Posters
Yuting Wang Shanghai Jiao Tong University, Xiangzhe Xu Nanjing University, Pierre Wilke CentraleSupélec, Zhong Shao Yale University
22:20 - 23:00
Posters Session 2 MirrorPosters at SPLASH-VII
22:20
40m
Poster
Learning Semantic Program Embeddings with Graph Interval Neural NetworkOOPSLA
Posters
Yu Wang Nanjing University, China, Ke Wang Visa Research, Fengjuan Gao Nanjing University, Linzhang Wang Nanjing University
22:20
40m
Poster
Towards a Formal Foundation of Intermittent ComputingOOPSLA
Posters
Milijana Surbatovich Carnegie Mellon University, Brandon Lucia Carnegie Mellon University, Limin Jia Carnegie Mellon University
22:20
40m
Poster
StreamQL: A Query Language for Processing Streaming Time SeriesOOPSLA
Posters
Lingkun Kong Rice University, Konstantinos Mamouras Rice University
22:20
40m
Poster
Incremental Predicate Analysis for Regression VerificationOOPSLA
Posters
Qianshan Yu Tsinghua University, Fei He Tsinghua University, Bow-Yaw Wang Academia Sinica
22:20
40m
Poster
SATUNE: Synthesizing Efficient SAT EncodersOOPSLA
Posters
Hamed Gorjiara University of California at Irvine, Guoqing Harry Xu University of California at Los Angeles, Brian Demsky University of California at Irvine
22:20
40m
Poster
A Sparse Iteration Space Transformation Framework for Sparse Tensor AlgebraOOPSLA
Posters
Ryan Senanayake Reservoir Labs, Changwan Hong Massachusetts Institute of Technology, Ziheng Wang Massachusetts Institute of Technology, Amalee Wilson Stanford University, Stephen Chou Massachusetts Institute of Technology, Shoaib Kamil Adobe Research, Saman Amarasinghe Massachusetts Institute of Technology, Fredrik Kjolstad Stanford University
DOI Pre-print Media Attached File Attached
22:20
40m
Poster
Unifying Execution of Imperative Generators and Declarative SpecificationsOOPSLA
Posters
Pengyu Nie University of Texas at Austin, Marinela Parovic University of Texas at Austin, Zhiqiang Zang University of Texas at Austin, Sarfraz Khurshid University of Texas at Austin, Aleksandar Milicevic Microsoft, Milos Gligoric University of Texas at Austin
22:20
40m
Poster
Statically Verified Refinements for Multiparty ProtocolsOOPSLA
Posters
Fangyi Zhou Imperial College London, Francisco Ferreira Imperial College London, Raymond Hu University of Hertfordshire, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London
22:20
40m
Poster
Guiding Dynamic Programing via Structural Probability for Accelerating Programming by ExampleOOPSLA
Posters
Ruyi Ji Peking University, Yican Sun Peking University, Yingfei Xiong Peking University, Zhenjiang Hu Peking University
22:20
40m
Poster
Revisiting Iso-Recursive SubtypingOOPSLA
Posters
Yaoda Zhou University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong, Jinxu Zhao University of Hong Kong
22:20
40m
Poster
Macros For Domain-Specific LanguagesOOPSLA
Posters
Michael Ballantyne Northeastern University, Alexis King Northwestern University, Matthias Felleisen Northeastern University
22:20
40m
Poster
CompCertELF: Verified Separate Compilation of C Programs into ELF Object FilesOOPSLA
Posters
Yuting Wang Shanghai Jiao Tong University, Xiangzhe Xu Nanjing University, Pierre Wilke CentraleSupélec, Zhong Shao Yale University
22:20
40m
Poster
Certified and Efficient Instruction SchedulingOOPSLA
Posters
Sylvain Boulmé Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, Cyril Six Kalray / Grenoble Alps University / CNRS / Grenoble INP / VERIMAG, David Monniaux Grenoble Alps University / CNRS / Grenoble INP / VERIMAG
22:20
40m
Poster
Resolution as Intersection Subtyping via Modus PonensOOPSLA
Posters
Koar Marntirosian KU Leuven, Tom Schrijvers KU Leuven, Bruno C. d. S. Oliveira University of Hong Kong, Georgios Karachalias Tweag
22:20
40m
Poster
Precise Inference of Expressive Units of Measurement TypesOOPSLA
Posters
Tongtong Xiang University of Waterloo, Jeff Y. Luo University of Waterloo, Werner Dietl University of Waterloo
22:20
40m
Poster
Guided Linking: Dynamic Linking Without the CostsOOPSLA
Posters
Sean Bartell University of Illinois at Urbana-Champaign, Will Dietz University of Illinois at Urbana-Champaign, Vikram S. Adve University of Illinois at Urbana-Champaign
22:20
40m
Poster
Scaling Exact Inference for Discrete Probabilistic ProgramsOOPSLA
Posters
Steven Holtzen University of California at Los Angeles, Guy Van den Broeck University of California at Los Angeles, Todd Millstein University of California, Los Angeles