SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Tue 17 Nov 2020 15:20 - 15:40 at OOPSLA/ECOOP - T-5
Wed 18 Nov 2020 03:20 - 03:40 at OOPSLA/ECOOP - T-5

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.

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

15:00 - 16:20: T-5OOPSLA at OOPSLA/ECOOP +12h
15:00 - 15:20
Talk
OOPSLA
Mehdi BagherzadehOakland University, Nicholas FiremanOakland University, Anas ShaweshOakland University, Raffi KhatchadourianCity University of New York (CUNY) Hunter College
15:20 - 15:40
Talk
OOPSLA
Arjen RouvoetDelft University of Technology, Hendrik van AntwerpenTU Delft, Casper Bach PoulsenDelft University of Technology, Robbert KrebbersDelft University of Technology, Eelco VisserDelft University of Technology
Link to publication DOI Pre-print
15:40 - 16:00
Talk
OOPSLA
Quentin StiévenartVrije Universiteit Brussel, Belgium, Magnus MadsenAarhus University
16:00 - 16:20
Talk
OOPSLA
Lukáš HolíkBrno University of Technology, Czechia, Ondrej LengalBrno University of Technology , Olli SaarikiviMSR Redmond, Lenka TuronovaBrno University of Technology, Margus VeanesMicrosoft Research, Tomas VojnarBrno University of Technology

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

03:00 - 04:20: T-5OOPSLA at OOPSLA/ECOOP
03:00 - 03:20
Talk
OOPSLA
Mehdi BagherzadehOakland University, Nicholas FiremanOakland University, Anas ShaweshOakland University, Raffi KhatchadourianCity University of New York (CUNY) Hunter College
03:20 - 03:40
Talk
OOPSLA
Arjen RouvoetDelft University of Technology, Hendrik van AntwerpenTU Delft, Casper Bach PoulsenDelft University of Technology, Robbert KrebbersDelft University of Technology, Eelco VisserDelft University of Technology
Link to publication DOI Pre-print
03:40 - 04:00
Talk
OOPSLA
Quentin StiévenartVrije Universiteit Brussel, Belgium, Magnus MadsenAarhus University
04:00 - 04:20
Talk
OOPSLA
Lukáš HolíkBrno University of Technology, Czechia, Ondrej LengalBrno University of Technology , Olli SaarikiviMSR Redmond, Lenka TuronovaBrno University of Technology, Margus VeanesMicrosoft Research, Tomas VojnarBrno University of Technology