SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Sun 15 Nov 2020 08:20 - 09:00 at SPLASH-VII - Posters Session 1
Sun 15 Nov 2020 20:20 - 21:00 at SPLASH-VII - Posters Session 1 Mirror

There is a large gap between the specification of type systems and the implementation of their type checkers, which impedes reasoning about the soundness of the type checker with respect to the specification. A vision to close this gap involves automatically obtaining type checkers from declarative programming language specifications. This moves the burden of proving correctness from a case-by-case basis for concrete languages, to a single correctness proof for the specification language.

This vision is obstructed by an aspect common to all programming languages: name resolution. Naming and scoping are pervasive and complex aspects of the static semantics of programming languages. Implementations of type checkers for languages with name binding features such as modules, imports, classes, and inheritance interleave collection of binding information (i.e., declarations, scoping structure, and imports) and querying that information. This requires scheduling those two aspects in such a way that query answers are stable—i.e., they are computed only after all relevant binding structure has been collected. Type checkers for concrete languages accomplish stability using language-specific knowledge about the type system.

In this paper we give a language independent characterization of necessary and sufficient conditions to guarantee stability of name and type queries during type checking in terms of critical edges in an incomplete scope graph. We use critical edges to give a formal small-step operational semantics to a declarative specification language for type systems, delaying queries that may depend on missing information. This yields type checkers for the specified languages that are safe-by-construction—i.e., they safely schedule queries and only accept programs that are name- and type-correct according to the declarative language specification. We implement this approach, and evaluate it against specifications of a small module and record language, as well as subsets of Java and Scala.

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

08:20 - 09:00
Posters Session 1Posters at SPLASH-VII +12h
08:20
40m
Poster
Formulog: Datalog for SMT-based Static AnalysisOOPSLA
Posters
Aaron BembenekHarvard University, Michael GreenbergPomona College, Stephen ChongHarvard University
08:20
40m
Poster
Analogy-Making as a Core Primitive in the Software Engineering ToolboxOnward! Papers
Posters
Matthew SotoudehUniversity of California, Davis, Aditya V. ThakurUniversity of California, Davis
08:20
40m
Poster
Row and Bounded Polymorphism via Disjoint PolymorphismECOOP
Posters
Ningning XieThe University of Hong Kong, Bruno C. d. S. OliveiraUniversity of Hong Kong, Xuan BiThe University of Hong Kong, Tom SchrijversKU Leuven
08:20
40m
Poster
Gradual Verification of Recursive Heap Data StructuresOOPSLA
Posters
Jenna WiseCarnegie Mellon University, Johannes BaderJane Street, Cameron WongJane Street, Jonathan AldrichCarnegie Mellon University, Éric TanterUniversity of Chile, Joshua SunshineCarnegie Mellon University
08:20
40m
Poster
Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative SpecificationsOOPSLA
Posters
Arjen RouvoetDelft University of Technology, Hendrik van AntwerpenDelft University of Technology, Casper Bach PoulsenDelft University of Technology, Robbert KrebbersRadboud University Nijmegen, Eelco VisserDelft University of Technology
08:20
40m
Poster
Owicki-Gries Reasoning for C11 RARECOOP
Posters
Sadegh DalvandiUniversity of Surrey, Simon DohertyUniversity of Sheffield, Brijesh DongolUniversity of Surrey, Heike WehrheimPaderborn University
08:20
40m
Poster
Demystifying DependenceOnward! Papers
Posters
08:20
40m
Poster
Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in ObsidianOOPSLA
Posters
Michael CoblenzUniversity of Maryland at College Park, Jonathan AldrichCarnegie Mellon University, Brad A. MyersCarnegie Mellon University, Joshua SunshineCarnegie Mellon University
08:20
40m
Poster
Multiparty Session Programming with Global Protocol CombinatorsECOOP
Posters
Keigo ImaiGifu University, Rumyana NeykovaBrunel University London, Nobuko YoshidaImperial College London, Shoji YuenNagoya University
08:20
40m
Poster
Static Race Detection and Mutex Safety and Liveness for Go ProgramsECOOP
Posters
Julia GabetImperial College London, Nobuko YoshidaImperial College London
08:20
40m
Poster
CAMP: Cost-Aware Multiparty Session ProtocolsOOPSLA
Posters
David Castro-PerezImperial College London, Nobuko YoshidaImperial College London
08:20
40m
Poster
A Case Study in Language-Based Security: Building an I/O Library for WyvernOnward! Papers
Posters
Jennifer FishCarnegie Mellon University, Darya MelicherGoogle, Jonathan AldrichCarnegie Mellon University
08:20
40m
Poster
On the Unusual Effectiveness of Type-aware Operator Mutations for Testing SMT SolversOOPSLA
Posters
Dominik WintererETH Zurich, Chengyu ZhangEast China Normal University, Zhendong SuETH Zurich
08:20
40m
Poster
Reshape Your Layouts, Not Your Programs: A Safe Language Extension for Better Cache LocalityECOOP
Posters
Alexandros TasosImperial College London, Juliana Franco, Sophia DrossopoulouImperial College London, Tobias WrigstadUppsala University, Sweden, Susan EisenbachImperial College London
08:20
40m
Poster
A Type-Directed Operational Semantics for a Calculus with a Merge OperatorECOOP
Posters
Xuejing HuangThe University of Hong Kong, Bruno C. d. S. OliveiraUniversity of Hong Kong
08:20
40m
Poster
Geometry Types for Graphics ProgrammingOOPSLA
Posters
Dietrich GeislerCornell University, Irene YoonUniversity of Pennsylvania, Aditi KabraCarnegie Mellon University, Horace HeCornell University, Yinnon SandersCornell University, Adrian SampsonCornell University
20:20 - 21:00
Posters Session 1 MirrorPosters at SPLASH-VII
20:20
40m
Poster
Analogy-Making as a Core Primitive in the Software Engineering ToolboxOnward! Papers
Posters
Matthew SotoudehUniversity of California, Davis, Aditya V. ThakurUniversity of California, Davis
20:20
40m
Poster
Static Race Detection and Mutex Safety and Liveness for Go ProgramsECOOP
Posters
Julia GabetImperial College London, Nobuko YoshidaImperial College London
20:20
40m
Poster
On the Unusual Effectiveness of Type-aware Operator Mutations for Testing SMT SolversOOPSLA
Posters
Dominik WintererETH Zurich, Chengyu ZhangEast China Normal University, Zhendong SuETH Zurich
20:20
40m
Poster
A Type-Directed Operational Semantics for a Calculus with a Merge OperatorECOOP
Posters
Xuejing HuangThe University of Hong Kong, Bruno C. d. S. OliveiraUniversity of Hong Kong
20:20
40m
Poster
Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative SpecificationsOOPSLA
Posters
Arjen RouvoetDelft University of Technology, Hendrik van AntwerpenDelft University of Technology, Casper Bach PoulsenDelft University of Technology, Robbert KrebbersRadboud University Nijmegen, Eelco VisserDelft University of Technology
20:20
40m
Poster
A Case Study in Language-Based Security: Building an I/O Library for WyvernOnward! Papers
Posters
Jennifer FishCarnegie Mellon University, Darya MelicherGoogle, Jonathan AldrichCarnegie Mellon University
20:20
40m
Poster
CAMP: Cost-Aware Multiparty Session ProtocolsOOPSLA
Posters
David Castro-PerezImperial College London, Nobuko YoshidaImperial College London
20:20
40m
Poster
Owicki-Gries Reasoning for C11 RARECOOP
Posters
Sadegh DalvandiUniversity of Surrey, Simon DohertyUniversity of Sheffield, Brijesh DongolUniversity of Surrey, Heike WehrheimPaderborn University
20:20
40m
Poster
Formulog: Datalog for SMT-based Static AnalysisOOPSLA
Posters
Aaron BembenekHarvard University, Michael GreenbergPomona College, Stephen ChongHarvard University
20:20
40m
Poster
Demystifying DependenceOnward! Papers
Posters
20:20
40m
Poster
Row and Bounded Polymorphism via Disjoint PolymorphismECOOP
Posters
Ningning XieThe University of Hong Kong, Bruno C. d. S. OliveiraUniversity of Hong Kong, Xuan BiThe University of Hong Kong, Tom SchrijversKU Leuven
20:20
40m
Poster
Reshape Your Layouts, Not Your Programs: A Safe Language Extension for Better Cache LocalityECOOP
Posters
Alexandros TasosImperial College London, Juliana Franco, Sophia DrossopoulouImperial College London, Tobias WrigstadUppsala University, Sweden, Susan EisenbachImperial College London
20:20
40m
Poster
Gradual Verification of Recursive Heap Data StructuresOOPSLA
Posters
Jenna WiseCarnegie Mellon University, Johannes BaderJane Street, Cameron WongJane Street, Jonathan AldrichCarnegie Mellon University, Éric TanterUniversity of Chile, Joshua SunshineCarnegie Mellon University
20:20
40m
Poster
Multiparty Session Programming with Global Protocol CombinatorsECOOP
Posters
Keigo ImaiGifu University, Rumyana NeykovaBrunel University London, Nobuko YoshidaImperial College London, Shoji YuenNagoya University
20:20
40m
Poster
Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in ObsidianOOPSLA
Posters
Michael CoblenzUniversity of Maryland at College Park, Jonathan AldrichCarnegie Mellon University, Brad A. MyersCarnegie Mellon University, Joshua SunshineCarnegie Mellon University
20:20
40m
Poster
Geometry Types for Graphics ProgrammingOOPSLA
Posters
Dietrich GeislerCornell University, Irene YoonUniversity of Pennsylvania, Aditi KabraCarnegie Mellon University, Horace HeCornell University, Yinnon SandersCornell University, Adrian SampsonCornell University