Wed 19 Jul 2023 11:45 - 12:00 at Amazon Auditorium (Gates G20) - ECOOP 1: Semantics Chair(s): Sophia Drossopoulou

Modeling sequential and parallel composition of effectful computations has been investigated in a variety of languages for long. In particular, the popular do-notation provides a lightweight effect embedding for any instance of a monad. Idiom bracket notation, on the other hand, provides an embedding for applicatives. First, while monads force effects to be executed sequentially, ignoring potential for parallelism, applicatives do not support sequential effects. Composing both sequential with parallel effects remains an open problem. This is even more of an issue as real programs consist of a combination of both sequential and parallel segments. Second, common notations do not support invoking effects in direct-style, instead forcing a rigid structure upon the code.

In this paper, we propose a mixed applicative/monadic notation that retains parallelism where possible, but allows sequentiality where necessary. We leverage a direct-style notation where sequentiality or parallelism is derived from the structure of the code. We provide a mechanisation of our effectful language in Coq and prove that our compilation approach retains the parallelism of the source program.

Wed 19 Jul

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

10:30 - 12:00
ECOOP 1: SemanticsResearch Papers at Amazon Auditorium (Gates G20)
Chair(s): Sophia Drossopoulou Imperial College London
10:30
15m
Talk
Semantics for Noninterference with Interaction Trees
Research Papers
Lucas Silver University of Pennsylvania, Paul He University of Pennsylvania, Ethan Cecchetti University of Maryland, College Park, Andrew K. Hirsch University at Buffalo, Steve Zdancewic University of Pennsylvania
DOI
10:45
15m
Talk
Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations that Supports Auto-active Verification
Research Papers
Lucas Silver University of Pennsylvania, Edwin Westbrook Galois, Matthew Yacavone Galois, Inc., Ryan Scott Galois, Inc.
DOI
11:00
15m
Talk
Multi-Graded Featherweight Java
Research Papers
Riccardo Bianchini University of Genoa, Francesco Dagnino University of Genoa, Paola Giannini University of Eastern Piedmont, Elena Zucca University of Genoa
DOI
11:15
15m
Talk
Wiring circuits is easy as {0, 1, ω}, or is it…
Research Papers
Jan de Muijnck-Hughes University of Glasgow, Wim Vanderbauwhede University of Glasgow
DOI
11:30
15m
Talk
Automata Learning with an Incomplete Teacher
Research Papers
Mark Moeller Cornell University, Thomas Wiener Cornell University, Alaia Solko-Breslin University of Pennsylvania, Caleb Koch Stanford, Nate Foster Cornell University, Alexandra Silva Cornell University
DOI
11:45
15m
Talk
A Direct-Style Effect Notation for Sequential and Parallel Programs
Research Papers
David Richter Technical University of Darmstadt, Timon Böhler Technical University of Darmstadt, Pascal Weisenburger University of St. Gallen, Mira Mezini TU Darmstadt
DOI Pre-print Media Attached