Researchers from Logic & Semantics and Programming Languages have had a remarkably high number of papers accepted at the top conferences OOPSLA’20 and POPL’21. At OOPSLA, which takes place this week, five papers have been accepted for publication. At POPL, they got six papers got accepted, which is almost 10% of all accepted papers.
Below you can find abstract and link for each of the accepted papers.
OOPSLA 2020 takes place online from November 15-21.
109 papers got accepted. Five from Aarhus University.
Detecting Locations in JavaScript Programs Affected by Breaking Library Changes
A. Møller, B. B. Nielsen, and M. T. Torp
JavaScript programmers often struggle with non-backwards compatible changes in software libraries. This paper presents a novel approach to automatically detect which parts of the programs need to be updated when upgrading to new versions of libraries.
https://cs.au.dk/~amoeller/papers/tapir/
Eliminating Abstraction Overhead of Java Stream Pipelines using Ahead-of-Time Program Optimization
A. Møller and O. H. Veileborg
Streams in Java make it easy for programmers to work with collections of data using high-level functional-style operations, however, this style of programming often has a significant run-time overhead. We present Streamliner, an ahead-of-time program optimizer that can make stream-based code run as fast as hand-written imperative-style code.
https://cs.au.dk/~amoeller/papers/streamliner/
Fixpoints for the Masses: Programming with First-Class Datalog Constraints
M. Madsen and O. Lhoták
We propose Datalog constraints as first-class values in a functional programming language. We present an extension of the lambda calculus with first-class Datalog constraints, including its semantics and a type system with row polymorphism based on Hindley-Milner. We prove soundness of the type system and implement it as an extension of the Flix programming language.
Fuzzing Channel-Based Concurrency Runtimes using Types and Effects
Q. Stievenart and M. Madsen
Modern programming languages support concurrent programming based on channels and processes. In this paper, we present an automatic program generation technique to test such programming language implementations. We define a type and effect system for programs that communicate over channels and where every execution is guaranteed to eventually terminate. We can generate and run such programs, and if a program fails to terminate, we have found a bug in the programming language implementation.
Polymorphic Types and Effects with Boolean Unification
M. Madsen and J. v. d. Pol
We provide a type and effect system that distinguishes pure expressions from expressions with effects. The type and effect inference algorithm uses Boolean unification, to calculate the most general polymorphic type and effect. We implemented the system in Flix and evaluate the efficiency of type and effect inference.
POPL 2021 takes place online from January 17-22.
61 papers (of 258 submitted) got accepted. Six from Aarhus University.
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
L. Gondelman, S.O. Gregersen, A. Nieto, A. Timany, and L. Birkedal
We present the first specification and verification of an implementation of a causally-consistent distributed database that supports modular verification of full functional correctness properties of clients and servers. We specify and reason about the causally-consistent distributed database in Aneris, a higher-order distributed separation logic for an ML-like programming language with network primitives for programming distributed systems. We demonstrate that our specifications are useful, by proving the correctness of small, but tricky, synthetic examples involving causal dependency and by verifying a session manager library implemented on top of the distributed database. We use Aneris’s facilities for modular specification and verification to obtain a highly modular development, where each component is verified in isolation, relying only on the specifications (not the implementations) of other components. We have used the Coq formalization of the Aneris logic to formalize all the results presented in the paper in the Coq proof assistant.
https://cs.au.dk/~birke/papers/2021-ccddb.pdf
Efficient and Provable Local Capability Revocation using Uninitialized Capabilities
A.L. Georges, A. Gueneau, T. van Strydonck, A. Timany, A. Trieu, S. Huyghebaert, D. Devriese, and L. Birkedal
Capability machines are a special form of CPUs that offer fine-grained privilege separation using a form of authority-carrying values known as capabilities. In this paper, we introduce a new form of capabilities that represent read/write authority to a block of memory without exposing the memory’s initial contents. We provide a mechanically verified program logic for reasoning about programs on a capability machine with the new feature and we formalize and prove capability safety in the form of a universal contract for untrusted code. We use uninitialized capabilities for making a previously proposed secure calling convention efficient and prove its security using the program logic.
https://cs.au.dk/~birke/papers/2021-iris-caps.pdf
Fully Abstract from Static to Gradual
K. Jacobs, A. Timany and D. Devriese
Gradually typed programming languages enable migration from existing untyped codebases to the static typing discipline. This paper investigates and argues for a new criterion where rather than preserving an arbitrarily chosen interpretation of static language types, all static language program equivalences are preserved.
https://cs.au.dk/~timany/publications/files/2021_POPL_gradual_full_abs.pdf
Mechanized Logical Relations for Termination-Insensitive Noninterference
S.O. Gregersen, J. Bay, A. Timany, and L. Birkedal
We present an expressive information-flow control type system for a higher-order programming language with higher-order state. We give a novel semantic model of this type system and show that well-typed programs satisfy termination-insensitive noninterference. Our semantic approach supports compositional integration of syntactically well-typed and syntactically ill-typed—but semantically sound—components, which we demonstrate through several interesting examples. We define our model using logical relations on top of the Iris program logic framework We formalize all of our theory and examples in the Coq proof assistant.
https://cs.au.dk/~birke/papers/2021-tiniris.pdf
Optimal Prediction of Synchronization-Preserving Races
U. Mathur, A. Pavlogiannis and M. Viswanathan
Data races are the most common errors in concurrent programs. The paper develops a new algorithm for predicting data races before they actually occur, by monitoring the program execution. The algorithm is much more effective than existing approaches, and almost as fast.
https://cs.au.dk/~pavlogiannis/publications/papers/popl21b.pdf
The Fine-Grained and Parallel Complexity of Andersen's Pointer Analysis
A. A. Mathiasen and A. Pavlogiannis
Andersen's Pointer Analysis (APA) is one of the most popular techniques to analyze a program's pattern of memory accesses. The paper resolves the algorithmic complexity of APA by presenting upper and lower complexity bounds, as well as new algorithms that are, in cases, optimal.
https://cs.au.dk/~pavlogiannis/publications/papers/popl21a.pdf
