Sciweavers

POPL
2015
ACM
8 years 9 days ago
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
We present Iris, a concurrent separation logic with a simple premise: monoids and invariants are all you need. Partial commutative monoids enable us to express—and invariants en...
Ralf Jung 0002, David Swasey, Filip Sieczkowski, K...
POPL
2015
ACM
8 years 9 days ago
On Characterizing the Data Access Complexity of Programs
Venmugil Elango, Fabrice Rastello, Louis-Noël...
POPL
2015
ACM
8 years 9 days ago
Succinct Representation of Concurrent Trace Sets
We present a method and a tool for generating succinct representations of sets of concurrent traces. We focus on trace sets that contain all correct or all incorrect permutations ...
Ashutosh Gupta, Thomas A. Henzinger, Arjun Radhakr...
POPL
2015
ACM
8 years 9 days ago
From Communicating Machines to Graphical Choreographies
Graphical choreographies, or global graphs, are general multiparty session specifications featuring expressive constructs such as forking, merging, and joining for representing a...
Julien Lange, Emilio Tuosto, Nobuko Yoshida
POPL
2015
ACM
8 years 9 days ago
A Coalgebraic Decision Procedure for NetKAT
Program equivalence is a fundamental problem that has practical applications across a variety of areas of computing including compilation, optimization, software synthesis, formal...
Nate Foster, Dexter Kozen, Matthew Milano, Alexand...
POPL
2015
ACM
8 years 9 days ago
Principal Type Schemes for Gradual Programs
Gradual typing is a discipline for integrating dynamic checking into
Ronald Garcia, Matteo Cimini
POPL
2015
ACM
8 years 9 days ago
Program Boosting: Program Synthesis via Crowd-Sourcing
a brief look at each paper and read its abstract. Each paper below includes a URL. Some papers are available for free, and others are available for free only to you as UMass studen...
Robert A. Cochran, Loris D'Antoni, Benjamin Livshi...
POPL
2015
ACM
8 years 9 days ago
Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it
We show that the weak memory model introduced by the 2011 C and C++ standards does not permit many common source-tosource program transformations (such as expression linearisation...
Viktor Vafeiadis, Thibaut Balabonski, Soham Chakra...