SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Events (97 results)

Miniaturize All States!

REBASE When: Wed 18 Nov 2020 07:00 - 07:40Wed 18 Nov 2020 19:00 - 19:40 People: Mathieu Boespflug

… Like science, software is in reproducibility crisis. All too often, “steps to reproduce” in bug reports don’t work or are too long and complicated. They shouldn’t be necessary to begin with. Fleets of servers suffer from constant …

Panel: Logic in Artificial Intelligence: Don’t Machine Learning and Neural Networks Do It All?

LPOP 2020 When: Sun 15 Nov 2020 13:45 - 14:15 People: Stuart Russell, Paul Tarau, Adnan Darwiche, David Warren

… …

In Pursuit of Easy(er) JITs

VMIL 2020 When: Tue 17 Nov 2020 13:00 - 14:20 People: Mark Stoodley

… challenges and features, all designed around the pursuit of “easy” JIT compiler …

Abstract Domains for Constraint Programming with Differential Equations

NSAD When: Tue 17 Nov 2020 03:00 - 03:20 People: Ghiles Ziat, Olivier Mullier, Julien Alexandre dit Sandretto, Christophe Garion, Alexandre Chapoutot, Xavier Thirioux

… to embrace all the components of CPSs. Physical part models of CPSs are usually …

Modular and Distributed IDE

SLE When: Sun 15 Nov 2020 23:20 - 23:40Sun 15 Nov 2020 11:20 - 11:40 People: Fabien Coulon, Alex Auvolat, Benoit Combemale, Yérom-David Bromberg, François Taïani, Olivier Barais, Noël Plouzeau

… that provides all language services (\emph{e.g.,} auto completion, compiler…) has … part that runs in the browser. However, all language services require different … within the IDE. The monolithic distribution of all language services prevents …

Sketchable Interaction - End-User Customization via Interactive Regions

LIVE 2020 When: Tue 17 Nov 2020 13:00 - 13:20 People: Jürgen Hahn, Raphael Wimmer

… . Within an SI context, all graphical objects, including canvas, icons … a sketch of a user interface. All interactive regions may contain effects which …, a “Delete” region will delete all documents that are dragged onto it. Additionally …

Data Dependence for Object-Oriented Programs

TAPAS When: Thu 19 Nov 2020 03:40 - 04:00 People: Carlos Galindo, Sergio Perez Rubio, Josep Silva

… subsumes previous approaches and that is able to represent all those situations. In this paper, we show that even the JSysDG does not produce complete slices in all

Program Slicing with Exception Handling

TAPAS When: Thu 19 Nov 2020 03:00 - 03:20 People: Carlos Galindo, Sergio Perez Rubio, Josep Silva

… instructions, which includes representation of all possible exception throwing …

Croquet: A Unique Collaboration Architecture (Keynote)

DLS 2020 When: Wed 18 - Thu 19 Nov 2020Wed 18 Nov 2020 11:40 - 12:20 People: Vanessa Freudenberg

… distributed to clients. Croquet moves all computation to the clients. A lightweight … that any external event is incorporated by all clients at exactly the same point in the computation, leading to synchronized, bit-identical state. All data …

Invited Talk: Abstract Domains in SMT Solving for Real Algebra

NSAD When: Tue 17 Nov 2020 01:00 - 02:20 People: Erika Abraham

… that all input polynomials are sign-invariant inside each of the cells. Therefore …

Test Case Generation from Context-Free Grammars using Generalized Traversal of LR-Automata

SLE When: Mon 16 Nov 2020 13:00 - 13:20Tue 17 Nov 2020 01:00 - 01:20 People: Christoff Rossouw, Bernd Fischer

… that generates positive test cases by covering all edges between pairs of directly … iterates over all edges stemming from shift/reduce and reduce/reduce conflicts, using …

Asterisk: Secure Programming Language for Smart Contracts (Student Talk)

Scala When: Wed 18 Nov 2020 11:40 - 12:00 People: Mohammadreza Ashouri

… by Asterisk are cross-platform in the sense that a compiled contract runs on all

PReGO: A Generative Methodology for Satisfying Real-Time Requirements on COTS-Based Systems: Definition and Experience Report

GPCE When: Sun 15 Nov 2020 15:40 - 16:00Mon 16 Nov 2020 03:40 - 04:00 People: Benjamin Rouxel, Ulrik Pagh Schultz, Benny Akesson, Jesper Holst, Ole Jørgensen, Clemens Grelck

… or operating systems with timing haz-ards and proprietary device drivers. All

Mito: Edit a spreadsheet. Generate production ready Python.

LIVE 2020 When: Tue 17 Nov 2020 11:20 - 11:40 People: Jacob Diamond-Reivich

… Mito is an editable spreadsheet inside a Jupyter notebook. With Mito, you can call your data frame as a spreadsheet, which you can edit in a point and click way, utilizing all the functions you have come to know in Excel. Every edit …

Managing Persistent Signals using Signal Classes

REBLS 2020 When: Mon 16 Nov 2020 09:40 - 10:20 People: Tetsuo Kamina, Tomoyuki Aotani, Hidehiko Masuhara

… is considered a ``small world,'' where all signals within it are synchronous. We further …

Hazel Tutor: Guiding Novices Through Type-Driven Development Strategies

HATRA When: Thu 19 Nov 2020 14:00 - 14:20 People: Hannah Potter, Cyrus Omar

… information at all times, including when there are \emph{holes} in the program. When …

Prusti – Deductive Verification for Rust

FTfJP People: Alexander J. Summers

… ; in particular, specifications and all interactions with our implemented tool …

Multi-stage Programming in the Large with Staged Classes

GPCE When: Sun 15 Nov 2020 13:00 - 13:20Mon 16 Nov 2020 01:00 - 01:20 People: Lionel Parreaux, Amir Shaikhha

… guarantee the removal of all
staging-time abstractions, resulting in the generation …

Grammar-Based Testing for Little Languages: An Experience Report with Student Compilers

SLE When: Mon 16 Nov 2020 13:20 - 13:40Tue 17 Nov 2020 01:20 - 01:40 People: Phillip van Heerden, Moeketsi Raselimo, Konstantinos (Kostis) Sagonas, Bernd Fischer

… that
(1) all test suites constructed systematically following different … the instructor's test suite in all aspects and
identifies errors or crashes in every … of triggered semantic errors and detected failures and crashes.
Moreover, all failing …

NBSafety: Fine-Grained Lineage for Safer Jupyter Notebooks

LIVE 2020 When: Tue 17 Nov 2020 11:00 - 11:20 People: Stephen Macke

… during unaided notebook interactions, all while preserving the flexibility …

Framework-Aware Debugging with Stack Tailoring

DLS 2020 When: Fri 20 Nov 2020 01:40 - 02:20Thu 19 Nov 2020 13:40 - 14:20 People: Matteo Marra, Guillermo Polito, Elisa Gonzalez Boix

… , or is available in another thread.
In such cases, manually gathering all

A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications

Research Papers When: Tue 17 Nov 2020 01:20 - 01:40Mon 16 Nov 2020 13:20 - 13:40 People: Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, Philippa Gardner

… async/await APIs, all underpinned by a simple Core Event Semantics that is sufficiently expressive to describe the event models underlying all these APIs. Our … official test-suites, passing all the applicable tests. Using the Core Events …

A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications

Artifacts People: Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, Philippa Gardner

… async/await APIs, all underpinned by a simple Core Event Semantics that is sufficiently expressive to describe the event models underlying all these APIs. Our … official test-suites, passing all the applicable tests. Using the Core Events …

Owicki-Gries Reasoning for C11 RAR

Artifacts People: Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, Heike Wehrheim

… the formalisation and proof of all case studies presented in the paper. All

Multiparty Session Programming with Global Protocol Combinators

Artifacts People: Keigo Imai, Rumyana Neykova, Nobuko Yoshida, Shoji Yuen

… . Local behaviours for all processes in a protocol are inferred at once from … of ocaml-mpst, with all the examples and benchmarks discussed in the paper …

Simple and Efficient Computation of Minimal Weak Control Closure

SAS When: Thu 19 Nov 2020 03:40 - 04:00Wed 18 Nov 2020 15:40 - 16:00 People: Abu Naser Masud

… and sensitive control dependencies and subsume all previously defined control …

Monday Panel: OpenMP for High Integrity systems: Moving responsibility from users to vendors

HILT 2020 When: Mon 16 Nov 2020 12:00 - 13:00 People: Sara Royuela, Michael Klemm, Eduardo Quiñones, Tucker Taft, Dirk Ziegenbein

… . This requires all specifications, and compiler and runtime implementations, to include … and performance sides makes Eduardo an excellent facilitator for all the parties involved … programming models suit all parties. Additionally, his research activities provide …

XERIS/APEX: Hyperscaling with Ada

HILT 2020 When: Tue 17 Nov 2020 10:10 - 10:35 People: Richard Wai

… ” in the same shared memory region. Since all synchronization is via CAS queues …

Annotating Executable DSLs with Energy Estimation Formulas

SLE When: Mon 16 Nov 2020 20:00 - 20:20Mon 16 Nov 2020 08:00 - 08:20 People: Thibault Béziers la Fosse, Massimo Tisi, Jean-Marie Mottu, Gerson Sunyé

… by deployment and measurement on all runtime platforms, that is slow and expensive.

We …

Gradually Typing Strategies

SLE When: Sun 15 Nov 2020 22:00 - 22:20Sun 15 Nov 2020 10:00 - 10:20 People: Jeff Smits, Eelco Visser

… , where possible. To make sure that statically typed code cannot go wrong, all

A Layered Mapping of Ada 202X to OpenMP

HILT 2020 When: Mon 16 Nov 2020 10:15 - 10:45 People: Tucker Taft

… features, in particular parallel blocks and parallel loops. All versions of Ada …

Building a Culture of Safe and Performant Systems with the Rust Programming Language

HILT 2020 When: Tue 17 Nov 2020 11:35 - 12:00 People: James Munns

… for developers of all backgrounds, error messages that serve as a system of teaching …

The Duality of Subtyping (artifact)

Artifacts People: Bruno C. d. S. Oliveira, Shaobo Cui, Baber Rehman

… image with all the dependencies installed or it could be built from the scratch …

K-LLVM: A Relatively Complete Semantics of LLVM IR

Research Papers When: Mon 16 Nov 2020 01:00 - 01:20Sun 15 Nov 2020 13:00 - 13:20 People: Liyi Li, Elsa Gunter

… complete formal LLVM IR semantics to date, including all LLVM IR instructions … an abstract machine that executes all LLVM IR instructions. The machine allows … consistent memory model and does not include all LLVM concurrency memory behaviors …

Challenges and lessons learned introducing Fuse, an evolving open source technology, into an established legacy Ada and C++ program

HILT 2020 When: Tue 17 Nov 2020 10:35 - 11:00 People: Brian Kleinke

… Background: When the FAA (Federal Aviation Administration) launched the System Wide Information Management (SWIM) initiative, the FAA had the goal of using the same portable, open infrastructure across all systems in the NAS (National …

Featherweight Swift: A Core Calculus for Swift’s Type System

SLE When: Mon 16 Nov 2020 14:00 - 14:20Tue 17 Nov 2020 02:00 - 02:20 People: Dimitri Racordon, Didier Buchs

… stripped of all features not essential to describe its typing rules. Featherweight …

Meeting with Mentors

PLMW

… Mentors and mentees will gather to meet by audio, video and text chat in CLOWDR. CLOWDR will list all of the available mentors and the topics that they are ready to provide advice on, and the organizers will provide conversation starters. …

Tuesday Panel: Language support for parallel and distributed computing

HILT 2020 When: Tue 17 Nov 2020 12:00 - 13:00 People: Tucker Taft, Kyle Chard, James Munns, Richard Wai

… that today’s programmer is generally confronted with all of this complexity. In some …

Blame for Null

Research Papers When: Sun 15 Nov 2020 21:40 - 22:00Sun 15 Nov 2020 09:40 - 10:00 People: Abel Nieto, Marianna Rapoport, Gregor Richards, Ondřej Lhoták

… Multiple modern programming languages, including Kotlin, Scala, Swift, and C#, have type systems where nullability is explicitly specified in the types. All … can’t be blamed. All our results are formalized in the Coq proof assistant. …

Static Type Analysis by Abstract Interpretation of Python Programs

Artifacts People: Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné

… in the experimental evaluation of the paper (Fig. 13).

All analyzers have been compiled …

Perfect is the Enemy of Good: Best-Effort Program Synthesis

Research Papers When: Sun 15 Nov 2020 22:00 - 22:20Sun 15 Nov 2020 10:00 - 10:20 People: Hila Peleg, Nadia Polikarpova

… always satisfy the specification exactly. We conjecture that this all-or-nothing … then not, no result at all. In this paper we propose a new program synthesis paradigm we call … even when the specification is flawed or too hard: i) for all benchmarks …

Perfect is the Enemy of Good: Best-Effort Program Synthesis

Artifacts People: Hila Peleg, Nadia Polikarpova

… always satisfy the specification exactly. We conjecture that this all-or-nothing … then not, no result at all. In this paper we propose a new program synthesis paradigm we call … when the specification is flawed or too hard: (i) for all benchmarks …

Scala with Explicit Nulls

Research Papers When: Mon 16 Nov 2020 06:00 - 06:20Sun 15 Nov 2020 18:00 - 18:20 People: Abel Nieto, Yaoyu Zhao, Ondřej Lhoták, Angela Chang, Justin Pu

… The Scala programming language makes all reference types implicitly nullable. This is a problem, because null references do not support most operations that do make sense on regular objects, leading to runtime errors. In this paper, we …

Owicki-Gries Reasoning for C11 RAR

Research Papers When: Mon 16 Nov 2020 03:40 - 04:00Sun 15 Nov 2020 15:40 - 16:00 People: Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, Heike Wehrheim

… with both relaxed and release-acquire accesses) that allows all Owicki-Gries …

Blame for Null

Artifacts People: Abel Nieto, Marianna Rapoport, Ondřej Lhoták, Gregor Richards

… . All of the above also need to interoperate with languages where types remain … \emph{explicitly nullable programs can’t be blamed}. All our results …

Scala with Explicit Nulls

Artifacts People: Abel Nieto, Ondřej Lhoták, Yaoyu Zhao, Angela Chang, Justin Pu

… The Scala programming language makes \emph{all} reference types \emph{implicitly nullable}. This is a problem, because null references do not support most operations that do make sense on regular objects, leading to runtime errors …

Row and Bounded Polymorphism via Disjoint Polymorphism

Research Papers When: Mon 16 Nov 2020 00:00 - 00:20Sun 15 Nov 2020 12:00 - 12:20 People: Ningning Xie, Bruno C. d. S. Oliveira, Xuan Bi, Tom Schrijvers

… intersection types* and disjoint polymorphism. With all these alternatives …

Multiparty Session Programming with Global Protocol Combinators

Research Papers When: Mon 16 Nov 2020 05:40 - 06:00Sun 15 Nov 2020 17:40 - 18:00 People: Keigo Imai, Rumyana Neykova, Nobuko Yoshida, Shoji Yuen

… and verifying multiparty protocols in OCaml. Local behaviours for all processes …

Static Type Analysis by Abstract Interpretation of Python Programs

Research Papers When: Mon 16 Nov 2020 02:00 - 02:20Sun 15 Nov 2020 14:00 - 14:20 People: Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné

… precisely track all exceptions (raised or caught). We designed a static analysis …

A Type-Directed Operational Semantics for a Calculus with a Merge Operator

Artifacts People: Xuejing Huang, Bruno C. d. S. Oliveira

… with respect to the $\lambda_{i}$ type system. All results have been fully …

A Type-Directed Operational Semantics for a Calculus with a Merge Operator

Research Papers When: Mon 16 Nov 2020 01:20 - 01:40Sun 15 Nov 2020 13:20 - 13:40 People: Xuejing Huang, Bruno C. d. S. Oliveira

… }^{:}$ is complete with respect to the $\lambda_{i}$ type system. All results have …

SqueakLive

Tutorials People: Marcel Taeumel, Patrick Rein, Tobias Pape, Tim Felgentreff, Robert Hirschfeld

… , tools, applications) with fast execution environments for all major platforms …

Polyglot Programming

Tutorials People: Fabio Niephaus, Tim Felgentreff, Mario Wolczko, Robert Hirschfeld

… an example notebook, and explain how it works under the hood. Together with all

Testing Differential Privacy with Dual Interpreters

OOPSLA When: Fri 20 Nov 2020 09:20 - 09:40Fri 20 Nov 2020 21:20 - 21:40 People: Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce, Aaron Roth

… annotations, handles all previously verified or
tested
algorithms … by implementing all benchmark
algorithms from prior work on mechanical verification …

A Type-and-Effect System for Object Initialization

OOPSLA When: Tue 17 Nov 2020 14:00 - 14:20Wed 18 Nov 2020 02:00 - 02:20 People: Fengyun Liu, Ondřej Lhoták, Aggelos Biboudis, Paolo G. Giarrusso, Martin Odersky

… Every newly created object goes through several initialization states:
starting from a state where all fields are uninitialized until all of
them are assigned. Any operation on the object during its initialization
process, which …

Non-local compiler transformations in the presence of dynamic dispatch

REBASE When: Mon 16 Nov 2020 15:00 - 15:40 People: Keno Fischer

… in Julia while retaining performance scalability all the way from completely …

Technology Today: A Paucity of Integrity and Imagination

REBASE When: Tue 17 Nov 2020 17:00 - 17:40Wed 18 Nov 2020 05:00 - 05:40Fri 20 Nov 2020 03:00 - 03:40 People: Robert Grimm

… of nativist nationalism across the western world, and contrast it all against …

A Ray of Hope: Array Programming for the 21st Century

REBASE When: Sun 15 Nov 2020 15:00 - 15:40Mon 16 Nov 2020 01:00 - 01:40 People: Gilad Bracha

… The ideas of APL and its successors, the array programming languages, were two generations ahead of their time.  These languages are based on the notion that everything is a tensor, and all operations are rank-polymorphic: they extend …

Pomsets with Preconditions: A Simple Model of Relaxed Memory

OOPSLA When: Fri 20 Nov 2020 07:20 - 07:40Fri 20 Nov 2020 19:20 - 19:40 People: Radha Jagadeesan, Alan Jeffrey, James Riely

… compositional reasoning for temporal safety properties, (2)
supports all

Speculation in Smart Contracts

REBASE When: Wed 18 Nov 2020 15:00 - 15:40Thu 19 Nov 2020 03:00 - 03:40 People: Maurice Herlihy

… for all transactions, especially simple payments and transfers that could …

Owicki-Gries Reasoning for C11 RAR

Posters When: Sun 15 Nov 2020 08:20 - 09:00Sun 15 Nov 2020 20:20 - 21:00 People: Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, Heike Wehrheim

… and release-acquire accesses) that allows all Owicki-Gries proof rules …

A Systematic Approach to Deriving Incremental Type Checkers

OOPSLA When: Tue 17 Nov 2020 13:20 - 13:40Wed 18 Nov 2020 01:20 - 01:40 People: André Pacak, Sebastian Erdweg, Tamás Szabó

… Static typing can guide programmers if feedback is immediate. Therefore, all major IDEs incrementalize type checking in some way. However, prior approaches to incremental type checking are often specialized and hard to transfer to new type …

Testing Consensus Implementations using Communication Closure

OOPSLA When: Fri 20 Nov 2020 15:40 - 16:00Sat 21 Nov 2020 03:40 - 04:00 People: Cezara Drăgoi, Constantin Enea, Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic

… on systematic or randomized exploration of all executions
of an implementation … in the same round or lost forever—such executions form a small subset of all

Revisiting Iso-Recursive Subtyping

Posters When: Mon 16 Nov 2020 10:20 - 11:00Mon 16 Nov 2020 22:20 - 23:00 People: Yaoda Zhou, Bruno C. d. S. Oliveira, Jinxu Zhao

… that two recursive types are subtypes \emph{if all their finite unfoldings …. All results are mechanically formalized in the Coq theorem prover. Furthermore …

Revisiting Iso-Recursive Subtyping

OOPSLA When: Wed 18 Nov 2020 08:00 - 08:20Wed 18 Nov 2020 20:00 - 20:20 People: Yaoda Zhou, Bruno C. d. S. Oliveira, Jinxu Zhao

… {if all their finite
unfoldings are subtypes}. The Amber rules are shown … and
metatheoretical studies involving recursive types. All results
are mechanically formalized …

Automatic and Efficient Variability-Aware Lifting of Functional Programs

OOPSLA When: Thu 19 Nov 2020 09:00 - 09:20Thu 19 Nov 2020 21:00 - 21:20 People: Ramy Shahin, Marsha Chechik

… variations individually, but not to the entire product line as a whole. Enumerating all … into a variability-aware version, exploring all combinations of its input arguments. Deep …

LiveDroid: Identifying and Preserving Mobile App State in Volatile Runtime Environments

OOPSLA When: Tue 17 Nov 2020 11:40 - 12:00Tue 17 - Wed 18 Nov 2020 People: Umar Farooq, Zhijia Zhao, Manu Sridharan, Iulian Neamtiu

… that includes all mutable program variables but ignores GUI properties … reveals a set of 46 issues due to incomplete state saving/restoring, all of which …

Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative Specifications

OOPSLA When: Tue 17 Nov 2020 15:20 - 15:40Wed 18 Nov 2020 03:20 - 03:40 People: Arjen Rouvoet, Hendrik van Antwerpen, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser

… for the specification language.
This vision is obstructed by an aspect common to all … are stable—i.e.,
they are computed only after all relevant binding structure has …

Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative Specifications

Posters When: Sun 15 Nov 2020 08:20 - 09:00Sun 15 Nov 2020 20:20 - 21:00 People: Arjen Rouvoet, Hendrik van Antwerpen, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser

… for the specification language.

This vision is obstructed by an aspect common to all …, they are computed only after all relevant binding structure has been collected …

Scaling Exact Inference for Discrete Probabilistic Programs

Posters When: Mon 16 Nov 2020 10:20 - 11:00Mon 16 Nov 2020 22:20 - 23:00 People: Steven Holtzen, Guy Van den Broeck, Todd Millstein

… . Inference is fundamentally hard, so there is no one-size-fits all solution …

Towards a Formal Foundation of Intermittent Computing

Posters When: Mon 16 Nov 2020 10:20 - 11:00Mon 16 Nov 2020 22:20 - 23:00 People: Milijana Surbatovich, Brandon Lucia, Limin Jia

… , such as I/O. Prior work has shown that all existing intermittent execution …

Enabling Accuracy-Aware Quantum Compilers using Symbolic Resource Estimation

OOPSLA When: Thu 19 Nov 2020 13:40 - 14:00Fri 20 Nov 2020 01:40 - 02:00 People: Giulia Meuli, Mathias Soeken, Martin Roetteler, Thomas Häner

… cost (e.g., total quantum gate count). All unspecified parameters of the quantum …

Towards a Formal Foundation of Intermittent Computing

OOPSLA When: Thu 19 Nov 2020 10:00 - 10:20Thu 19 Nov 2020 22:00 - 22:20 People: Milijana Surbatovich, Brandon Lucia, Limin Jia

… powered devices, such as I/O. Prior work
has shown that all existing …

Scaling Exact Inference for Discrete Probabilistic Programs

OOPSLA When: Fri 20 Nov 2020 13:40 - 14:00Sat 21 Nov 2020 01:40 - 02:00 People: Steven Holtzen, Guy Van den Broeck, Todd Millstein

… in practice. Inference is fundamentally hard, so there is no one-size-fits all

Row and Bounded Polymorphism via Disjoint Polymorphism

Posters When: Sun 15 Nov 2020 08:20 - 09:00Sun 15 Nov 2020 20:20 - 21:00 People: Ningning Xie, Bruno C. d. S. Oliveira, Xuan Bi, Tom Schrijvers

… and disjoint polymorphism. With all these alternatives it is natural to wonder how …

Designing Types for R, Empirically

OOPSLA When: Mon 16 Nov 2020 17:40 - 18:00Tue 17 Nov 2020 05:40 - 06:00 People: Alexi Turcotte, Aviral Goel, Filip Křikava, Jan Vitek

… no type annotations, and all
operations are dynamically checked at run-time …

Multiparty Session Programming with Global Protocol Combinators

Posters When: Sun 15 Nov 2020 08:20 - 09:00Sun 15 Nov 2020 20:20 - 21:00 People: Keigo Imai, Rumyana Neykova, Nobuko Yoshida, Shoji Yuen

… and verifying multiparty protocols in OCaml. Local behaviours for all processes …

Testing Deep Neural Networks

Keynotes When: Tue 17 Nov 2020 07:00 - 08:20Tue 17 Nov 2020 19:00 - 20:20 People: Mary Lou Soffa

… that all the three techniques generate significant number of invalid test inputs. We …

Dataflow-Based Pruning for Speeding up Superoptimization

OOPSLA When: Thu 19 Nov 2020 13:20 - 13:40Fri 20 Nov 2020 01:20 - 01:40 People: Manasij Mukherjee, Pranav Kant, Zhengyang Liu, John Regehr

… (14.54 hours vs 33.76
hours baseline, on a large multicore) at solving all 269,113 …

Effects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism

OOPSLA When: Fri 20 Nov 2020 15:00 - 15:20Sat 21 Nov 2020 03:00 - 03:20 People: Jonathan Immanuel Brachthäuser, Philipp Schuster, Klaus Ostermann

… , we
separate functions from values and treat <em>all</em …

Learning Graph-Based Heuristics for Pointer Analysis without Handcrafting Application-Specific Features

OOPSLA When: Fri 20 Nov 2020 07:20 - 07:40Fri 20 Nov 2020 19:20 - 19:40 People: Minseok Jeon, Myungho Lee, Hakjoo Oh

… , because applying context sensitivity to all methods in a real-world program …

Feedback-Driven Semi-supervised Synthesis of Program Transformations

OOPSLA When: Fri 20 Nov 2020 09:00 - 09:20Fri 20 Nov 2020 21:00 - 21:20 People: Xiang Gao, Shraddha Barke, Arjun Radhakrishna, Gustavo Soares, Sumit Gulwani, Alan Leung, Nachiappan Nagappan, Ashish Tiwari

… While editing code, it is common for developers to make multiple related
repeated edits that are all instances of a more general program transformation.
Since this process can be tedious and error-prone, we study the problem …

Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs

OOPSLA When: Thu 19 Nov 2020 09:20 - 09:40Thu 19 Nov 2020 21:20 - 21:40 People: Alejandro Gómez-Londoño, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus O. Myreen, Yong Kiam Tan


map directly to the space cost of the compiler-generated machine
code. All

A Large-Scale Longitudinal Study of Flaky Tests

OOPSLA When: Tue 17 Nov 2020 09:20 - 09:40Tue 17 Nov 2020 21:20 - 21:40 People: Wing Lam, Stefan Winter, Anjiang Wei, Tao Xie, Darko Marinov, Jonathan Bell

… are often impractical to be used on all tests for each project change. To combat … detectors are always applied to all tests. Our study is the first to empirically …

Lies we tell ourselves about developer infrastructure

REBASE When: Mon 16 Nov 2020 17:00 - 17:40Tue 17 Nov 2020 01:00 - 01:40 People: Joe Pamer

… , all while keeping a tight feedback loop with a potentially massive user base …

Direct Manipulation for Computational Making

SPLASH-E When: Fri 20 Nov 2020 15:00 - 15:10 People: Ian C. McCormack, Chris Johnson

… language. This language supports all shapes within the SVG standard as built …

Taming Type Annotations in Gradual Typing

OOPSLA When: Fri 20 Nov 2020 11:20 - 11:40Fri 20 Nov 2020 23:20 - 23:40 People: John Peter Campora, Sheng Chen

… considering all added annotations.

Recent studies provide evidence that type …

A Type-Directed Operational Semantics for a Calculus with a Merge Operator

Posters When: Sun 15 Nov 2020 08:20 - 09:00Sun 15 Nov 2020 20:20 - 21:00 People: Xuejing Huang, Bruno C. d. S. Oliveira

… }$ type system. All results have been fully formalized in the Coq theorem prover. …

Example-Based Live Programming for Everyone: Building Language-agnostic Tools for Live Programming with LSP and GraalVM

Onward! Papers When: Tue 17 Nov 2020 21:00 - 21:20Tue 17 Nov 2020 09:00 - 09:20 People: Fabio Niephaus, Patrick Rein, Jakob Edding, Jonas Hering, Bastian König, Kolya Opahle, Nico Scordialo, Robert Hirschfeld

… ecosystems. Our system, on the other hand, brings ELP for all languages supported …

Proving Highly-Concurrent Traversals Correct

OOPSLA When: Wed 18 Nov 2020 13:40 - 14:00Thu 19 Nov 2020 01:40 - 02:00 People: Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham

… behaviors, necessitating intricate reasoning about all interleavings of reads …

A Sparse Iteration Space Transformation Framework for Sparse Tensor Algebra

Posters When: Mon 16 Nov 2020 10:20 - 11:00Mon 16 Nov 2020 22:20 - 23:00 People: Ryan Senanayake, Changwan Hong, Ziheng Wang, Amalee Wilson, Stephen Chou, Shoaib Kamil, Saman Amarasinghe, Fredrik Kjolstad

… implementations from the literature, while generalizing to all of the tensor algebra. …

A Sparse Iteration Space Transformation Framework for Sparse Tensor Algebra

OOPSLA When: Fri 20 Nov 2020 09:00 - 09:20Fri 20 Nov 2020 21:00 - 21:20 People: Ryan Senanayake, Changwan Hong, Ziheng Wang, Amalee Wilson, Stephen Chou, Shoaib Kamil, Saman Amarasinghe, Fredrik Kjolstad

… implementations from the literature, while generalizing to all of the tensor algebra. …

Sound Garbage Collection for C using Pointer Provenance

OOPSLA When: Wed 18 Nov 2020 17:20 - 17:40Thu 19 Nov 2020 05:20 - 05:40 People: Subarno Banerjee, David Devecsery, Peter M. Chen, Satish Narayanasamy

… control-flow, our GC has sound and precise information to compute the set of all

CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files

Posters When: Mon 16 Nov 2020 10:20 - 11:00Mon 16 Nov 2020 22:20 - 23:00 People: Yuting Wang, Xiangzhe Xu, Pierre Wilke, Zhong Shao

… We present CompCertELF, the first extension to CompCert that supports verified compilation from C programs all the way to a standard binary file format, i.e., the ELF object format. Previous work on Stack-Aware CompCert provides a verified …

CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files

OOPSLA When: Wed 18 Nov 2020 18:00 - 18:20Thu 19 Nov 2020 06:00 - 06:20 People: Yuting Wang, Xiangzhe Xu, Pierre Wilke, Zhong Shao

… <p>
We present CompCertELF, the first extension to CompCert that
supports verified compilation from C programs all the way to a
standard binary file format, i.e., the ELF object format.
Previous work on Stack-Aware CompCert …

Paradigms Without Progress: Kuhnian Reflections on Programming Practice

REBASE When: Wed 18 Nov 2020 11:00 - 11:40 People: Jimmy Miller

… popular). Nor will we try to bridge the gap, finding some synthesis to make all

TacTok: Semantics-Aware Proof Synthesis

OOPSLA When: Fri 20 Nov 2020 07:40 - 08:00Fri 20 Nov 2020 19:40 - 20:00 People: Emily First, Yuriy Brun, Arjun Guha

… is
open-source and we make public all our data and a replication package of our …