EVCS
Wed 5 Apr 2023 Delft, Netherlands
Wed 5 Apr 2023 16:50 - 17:00 at Theatre Hall - Session 4: Scopes & Types Chair(s): Yannis Smaragdakis

Clearly specified interfaces between software components are invaluable: development proceeds in parallel; implementation details are abstracted away; invariants are enforced; code is reused. But this abstraction comes with a cost: well chosen interfaces let related tasks be grouped together, but a running program interleaves tasks of all kinds. Reasoning about which values cross a given interface or which interfaces a value will cross is challenging.

It is particularly hard to know that interfaces apply runtime enforcement mechanisms correctly: as programs run, values cross abstraction boundaries in subtle ways. One particular case of such reasoning—proving that a contract system checks contracts correctly at runtime—uses a dynamic analysis to keep track of which interfaces are responsible for which values. The dynamic analysis works by giving an alternative semantics that `colors’ values to match the components responsible for them. No program is ever run in this alternative semantics—it’s a formal tool to verify that the contract system’s enforcement is correct.

In this short paper, we refine Dimoulas et al.’s dynamic analysis to more precisely track colors, phrasing our results graph theoretically: a value’s colors are a path in the interface graph of the original program. Our graph theoretic framing makes it easy to see that the dynamic analysis is related to Eelco Visser’s scope graphs.

Wed 5 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:30
Session 4: Scopes & TypesEelco Visser Commemorative Symposium at Theatre Hall
Chair(s): Yannis Smaragdakis University of Athens
16:00
10m
Talk
Scope Graphs: The Story so Far
Eelco Visser Commemorative Symposium
Aron Zwaan Delft University of Technology, Hendrik van Antwerpen GitHub
DOI Pre-print File Attached
16:10
10m
Talk
Dependently Typed Languages in Statix
Eelco Visser Commemorative Symposium
Jonathan Brouwer TU Delft, Jesper Cockx Delft University of Technology, Aron Zwaan Delft University of Technology
Link to publication DOI
16:20
10m
Talk
Stack graphs: Name Resolution at Scale
Eelco Visser Commemorative Symposium
DOI Pre-print
16:30
10m
Talk
Using Spoofax to Support Online Code Navigation
Eelco Visser Commemorative Symposium
Peter D. Mosses Delft University of Technology
DOI File Attached
16:40
10m
Talk
Renamingless Capture-Avoiding Substitution for Definitional Interpreters
Eelco Visser Commemorative Symposium
Casper Bach Poulsen Delft University of Technology
DOI Pre-print
16:50
10m
Talk
Reasoning About Paths in the Interface Graph
Eelco Visser Commemorative Symposium
Michael Greenberg Stevens Institute of Technology
Link to publication DOI
17:00
10m
Talk
Type Theory as a Language Workbench
Eelco Visser Commemorative Symposium
Jan de Muijnck-Hughes University of Glasgow, Guillaume Allais University of St Andrews, Edwin Brady University of St Andrews, UK
Pre-print
17:10
10m
Talk
A Simply Numbered Lambda Calculus
Eelco Visser Commemorative Symposium
Friedrich Steimann Fernuniversität in Hagen
Link to publication DOI
17:20
10m
Other
Session closing
Eelco Visser Commemorative Symposium