ACM Principles of Programming Languages, POPL 2015


Title/Authors Title Research Artifacts
[?] A research artifact is any by-product of a research project that is not directly included in the published research paper. In Computer Science research this is often source code and data sets, but it could also be media, documentation, inputs to proof assistants, shell-scripts to run experiments, etc.
Details

Quantitative Interprocedural Analysis

Krishnendu Chatterjee, Andreas Pavlogiannis, Yaron Velner

Quantitative Interprocedural Analysis

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Tractable Refinement Checking for Concurrent Objects

Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza

Tractable Refinement Checking for Concurrent Objects

Details
Discussion Comments: 0
Verification: Authors have not verified information

Sound Modular Verification of C Code Executing in an Unverified Context

Pieter Agten, Bart Jacobs, Frank Piessens

Sound Modular Verification of C Code Executing in an Unverified Context

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

A Calculus for Relaxed Memory

Karl Crary, Michael J. Sullivan

A Calculus for Relaxed Memory

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy

Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub

Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

A Coalgebraic Decision Procedure for NetKAT

Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva, Laure Thompson

A Coalgebraic Decision Procedure for NetKAT

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Coding by Everyone, Every Day

Peter Lee

Coding by Everyone, Every Day

Details
Discussion Comments: 0
Verification: Author has not verified information

Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction

Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Pietro Abate

Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments: Development version of CDuce. Branch cduce-next.
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Manifest Contracts for Datatypes

Taro Sekiyama, Yuki Nishida, Atsushi Igarashi

Manifest Contracts for Datatypes

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Abstract Symbolic Automata: Mixed syntactic/semantic similarity analysis of executables

Mila Dalla Preda, Roberto Giacobazzi, Arun Lakhotia, Isabella Mastroeni

Abstract Symbolic Automata: Mixed syntactic/semantic similarity analysis of executables

Details
Discussion Comments: 0
Verification: Authors have not verified information

Succinct Representation of Concurrent Trace Sets

Ashutosh Gupta, Thomas A. Henzinger, Arjun Radhakrishna, Roopsha Samanta, Thorsten Tarrach

Succinct Representation of Concurrent Trace Sets

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Compositional CompCert

Gordon Stewart, Lennart Beringer, Santiago Cuellar, Andrew W. Appel

Compositional CompCert

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Space-Efficient Manifest Contracts

Michael Greenberg

Space-Efficient Manifest Contracts

Details
Discussion Comments: 0
Verification: Author has not verified information

Algebraic Effects, Linearity, and Quantum Programming Languages

Sam Staton

Algebraic Effects, Linearity, and Quantum Programming Languages

Details
Discussion Comments: 0
Verification: Author has not verified information

A Formally-Verified C Static Analyzer

Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie

A Formally-Verified C Static Analyzer

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Higher Inductive Types as Homotopy-Initial Algebras

Kristina Sojakova

Higher Inductive Types as Homotopy-Initial Algebras

Details
Discussion Comments: 0
Verification: Author has not verified information

A Scalable, Correct Time-Stamped Stack

Mike Dodds, Andreas Haas, Christoph M. Kirsch

A Scalable, Correct Time-Stamped Stack

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant

Benjamin Delaware, Clément Pit-Claudel, Jason Gross, Adam Chlipala

Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks

Hao Tang, Xiaoyin Wang, Lingming Zhang, Bing Xie, Lu Zhang, Hong Mei

Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

DReX: A Declarative Language for Efficiently Evaluating Regular String Transformations

Rajeev Alur, Loris D'Antoni, Mukund Raghothaman

DReX: A Declarative Language for Efficiently Evaluating Regular String Transformations

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Proof Spaces for Unbounded Parallelism

Azadeh Farzan, Zachary Kincaid, Andreas Podelski

Proof Spaces for Unbounded Parallelism

Details
Discussion Comments: 0
Verification: Authors have not verified information

Conjugate Hylomorphisms - Or: The Mother of All Structured Recursion Schemes

Ralf Hinze, Nicolas Wu, Jeremy Gibbons

Conjugate Hylomorphisms - Or: The Mother of All Structured Recursion Schemes

Details
Discussion Comments: 0
Verification: Authors have not verified information

Integrating Linear and Dependent Types

Neelakantan R. Krishnaswami, Pierre Pradic, Nick Benton

Integrating Linear and Dependent Types

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Equations, Contractions, and Unique Solutions

Davide Sangiorgi

Equations, Contractions, and Unique Solutions

Details
Discussion Comments: 0
Verification: Author has not verified information

Differential Privacy: Now it's Getting Personal

Hamid Ebadi, David Sands, Gerardo Schneider

Differential Privacy: Now it's Getting Personal

Details
Discussion Comments: 0
Verification: Authors have not verified information

Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems

Fei He, Xiaowei Gao, Bow-Yaw Wang, Lijun Zhang

Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems

Details
Discussion Comments: 0
Verification: Authors have not verified information

Full Abstraction for Signal Flow Graphs

Filippo Bonchi, Pawel Sobocinski, Fabio Zanasi

Full Abstraction for Signal Flow Graphs

Details
Author Comments:
Discussion Comments: 0
Sharing: Research produced no artifacts
Verification: Authors have verified information

On Characterizing the Data Access Complexity of Programs

Venmugil Elango, Fabrice Rastello, Louis-Noël Pouchet, J. Ramanujam, P. Sadayappan

On Characterizing the Data Access Complexity of Programs

Details
Discussion Comments: 0
Verification: Authors have not verified information

Functors are Type Refinement Systems

Paul-André Melliès, Noam Zeilberger

Functors are Type Refinement Systems

Details
Discussion Comments: 0
Verification: Authors have not verified information

Automating Repetitive Tasks for the Masses

Sumit Gulwani

Automating Repetitive Tasks for the Masses

Details
Discussion Comments: 0
Verification: Author has not verified information

Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests

Damien Pous

Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Author has not verified information

Self-Representation in Girard's System U

Matt Brown, Jens Palsberg

Self-Representation in Girard's System U

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Ur/Web: A Simple Model for Programming the Web

Adam Chlipala

Ur/Web: A Simple Model for Programming the Web

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Author has not verified information

Programming up to Congruence

Vilhelm Sjöberg, Stephanie Weirich

Programming up to Congruence

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Deep Specifications and Certified Abstraction Layers

Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, Yu Guo

Deep Specifications and Certified Abstraction Layers

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Databases and Programming: Two Subjects Divided by a Common Language?

Peter Buneman

Databases and Programming: Two Subjects Divided by a Common Language?

Details
Discussion Comments: 0
Verification: Author has not verified information

Runtime Enforcement of Security Policies on Black Box Reactive Programs

Minh Ngo, Fabio Massacci, Dimiter Milushev, Frank Piessens

Runtime Enforcement of Security Policies on Black Box Reactive Programs

Details
Discussion Comments: 0
Verification: Authors have not verified information

Dependent Information Flow Types

Luísa Lourenço, Luís Caires

Dependent Information Flow Types

Details
Discussion Comments: 0
Verification: Authors have not verified information

Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning

Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer

Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments: Iris is an ongoing (open-source) project. The original Coq formalization that accompanied the POPL 2015 paper (Iris v1.0), and which received an Artifact Evaluation Badge, is available here: http://plv.mpi-sws.org/iris/distrib/. The Coq formalization of the latest version of Iris (v3.0) is available here: https://gitlab.mpi-sws.org/FP/iris-coq/. Both of the above are linked off the main Iris project page: http://iris-project.org/.
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

K-Java: A Complete Semantics of Java

Denis Bogdanas, Grigore Rosu

K-Java: A Complete Semantics of Java

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Probabilistic Termination: Soundness, Completeness, and Compositionality

Luis María Ferrer Fioriti, Holger Hermanns

Probabilistic Termination: Soundness, Completeness, and Compositionality

Details
Discussion Comments: 0
Verification: Authors have not verified information

Decentralizing SDN Policies

Oded Padon, Neil Immerman, Aleksandr Karbyshev, Ori Lahav, Mooly Sagiv, Sharon Shoham

Decentralizing SDN Policies

Details
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Analyzing Program Analyses

Roberto Giacobazzi, Francesco Logozzo, Francesco Ranzato

Analyzing Program Analyses

Details
Discussion Comments: 0
Verification: Authors have not verified information

From Communicating Machines to Graphical Choreographies

Julien Lange, Emilio Tuosto, Nobuko Yoshida

From Communicating Machines to Graphical Choreographies

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments:
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Predicting Program Properties from "Big Code"

Veselin Raychev, Martin T. Vechev, Andreas Krause

Predicting Program Properties from "Big Code"

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Author Comments: Accepted research data and artifact related to this paper: http://files.srl.inf.ethz.ch/jsniceartifact/ Website with the technology described in the paper: http://jsnice.org
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

Program Boosting: Program Synthesis via Crowd-Sourcing

Robert A. Cochran, Loris D'Antoni, Benjamin Livshits, David Molnar, Margus Veanes

Program Boosting: Program Synthesis via Crowd-Sourcing

Details
Discussion Comments: 0
Verification: Authors have not verified information

Principal Type Schemes for Gradual Programs

Ronald Garcia, Matteo Cimini

Principal Type Schemes for Gradual Programs

Details
Discussion Comments: 0
Verification: Authors have not verified information

Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it

Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli

Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth

Krishnendu Chatterjee, Rasmus Ibsen-Jensen, Andreas Pavlogiannis, Prateesh Goyal

Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth

Details
Discussion Comments: 0
Verification: Authors have not verified information

Safe & Efficient Gradual Typing for TypeScript

Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin M. Bierman, Panagiotis Vekris

Safe & Efficient Gradual Typing for TypeScript

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Authors have not verified information

Specification Inference Using Context-Free Language Reachability

Osbert Bastani, Saswat Anand, Alex Aiken

Specification Inference Using Context-Free Language Reachability

Details
Discussion Comments: 0
Verification: Authors have not verified information

Data-Parallel String-Manipulating Programs

Margus Veanes, Todd Mytkowicz, David Molnar, Benjamin Livshits

Data-Parallel String-Manipulating Programs

Details
Discussion Comments: 0
Verification: Authors have not verified information

Towards the Essence of Hygiene

Michael D. Adams

Towards the Essence of Hygiene

Details
Discussion Comments: 0
Verification: Author has not verified information

A Meta Lambda Calculus with Cross-Level Computation

Kazunori Tobisawa

A Meta Lambda Calculus with Cross-Level Computation

Details
Discussion Comments: 0
Verification: Author has not verified information

From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification

Adam Chlipala

From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification

Details
Artifacts for some papers are reviewed by an artifact evaluation, reproducibility, or similarly named committee. This is one such paper that passed review.
Artifact evaluation badge awarded
Discussion Comments: 0
Verification: Author has not verified information