ACM Principles of Programming Languages, POPL 2014


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

Replicated data types: specification, verification, optimality

Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, Marek Zawirski

Replicated data types: specification, verification, optimality

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

30 years of research and development around Coq

Gérard P. Huet, Hugo Herbelin

30 years of research and development around Coq

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

Optimal dynamic partial order reduction

Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, Konstantinos F. Sagonas

Optimal dynamic partial order reduction

Details
Author Comments: A significantly extended version of this paper will appear in the Journal of the ACM under the title: "Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction". That article, which can be obtained from the authors, also has an associated artifact with the benchmarks.
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

CakeML: a verified implementation of ML

Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens

CakeML: a verified implementation of ML

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

Sound input filter generation for integer overflow errors

Fan Long, Stelios Sidiroglou-Douskos, Deokhwan Kim, Martin C. Rinard

Sound input filter generation for integer overflow errors

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

Combining proofs and programs in a dependently typed language

Chris Casinghino, Vilhelm Sjöberg, Stephanie Weirich

Combining proofs and programs in a dependently typed language

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

Probabilistic relational verification for cryptographic implementations

Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella Béguelin

Probabilistic relational verification for cryptographic implementations

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

Fair reactive programming

Andrew Cave, Francisco Ferreira, Prakash Panangaden, Brigitte Pientka

Fair reactive programming

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

A verified information-flow architecture

Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach

A verified information-flow architecture

Details
Author Comments: This POPL paper was later expanded into a journal version, available here: https://arxiv.org/abs/1509.06503v2
Discussion Comments: 0
Sharing: Research produced artifacts
Verification: Authors have verified information

A nonstandard standardization theorem

Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, Carlos Lombardi

A nonstandard standardization theorem

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

A type-directed abstraction refinement approach to higher-order model checking

Steven J. Ramsay, Robin P. Neatherway, C.-H. Luke Ong

A type-directed abstraction refinement approach to higher-order model checking

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

Tracing compilation by abstract interpretation

Stefano Dissegna, Francesco Logozzo, Francesco Ranzato

Tracing compilation by abstract interpretation

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

On coinductive equivalences for higher-order probabilistic functional programs

Ugo Dal Lago, Davide Sangiorgi, Michele Alberti

On coinductive equivalences for higher-order probabilistic functional programs

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

Gradual typing embedded securely in JavaScript

Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman

Gradual typing embedded securely in JavaScript

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

Abstract effects and proof-relevant logical relations

Nick Benton, Martin Hofmann, Vivek Nigam

Abstract effects and proof-relevant logical relations

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

Fissile type analysis: modular checking of almost everywhere invariants

Devin Coughlin, Bor-Yuh Evan Chang

Fissile type analysis: modular checking of almost everywhere invariants

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

Profiling for laziness

Stephen Chang, Matthias Felleisen

Profiling for laziness

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

Modular, higher-order cardinality analysis in theory and practice

Ilya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones

Modular, higher-order cardinality analysis in theory and practice

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

Applying quantitative semantics to higher-order quantum computing

Michele Pagani, Peter Selinger, Benoît Valiron

Applying quantitative semantics to higher-order quantum computing

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

Authenticated data structures, generically

Andrew Miller, Michael Hicks, Jonathan Katz, Elaine Shi

Authenticated data structures, generically

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

Proof search for propositional abstract separation logics via labelled sequents

Zhe Hou, Ranald Clouston, Rajeev Goré, Alwen Tiu

Proof search for propositional abstract separation logics via labelled sequents

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

Bias-variance tradeoffs in program analysis

Rahul Sharma, Aditya V. Nori, Alex Aiken

Bias-variance tradeoffs in program analysis

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

Battery transition systems

Udi Boker, Thomas A. Henzinger, Arjun Radhakrishna

Battery transition systems

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

A relationally parametric model of dependent type theory

Robert Atkey, Neil Ghani, Patricia Johann

A relationally parametric model of dependent type theory

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

Proofs that count

Azadeh Farzan, Zachary Kincaid, Andreas Podelski

Proofs that count

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

Toward general diagnosis of static errors

Danfeng Zhang, Andrew C. Myers

Toward general diagnosis of static errors

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

A trusted mechanised JavaSript specification

Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, Gareth Smith

A trusted mechanised JavaSript specification

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

Abstract acceleration of general linear loops

Bertrand Jeannet, Peter Schrammel, Sriram Sankaranarayanan

Abstract acceleration of general linear loops

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

A proof system for separation logic with magic wand

Wonyeol Lee, Sungwoo Park

A proof system for separation logic with magic wand

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

Probabilistic coherence spaces are fully abstract for probabilistic PCF

Thomas Ehrhard, Christine Tasson, Michele Pagani

Probabilistic coherence spaces are fully abstract for probabilistic PCF

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

Parametric effect monads and semantics of effect systems

Shin-ya Katsumata

Parametric effect monads and semantics of effect systems

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

The essence of Reynolds

Stephen Brookes, Peter W. O'Hearn, Uday S. Reddy

The essence of Reynolds

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

An operational and axiomatic semantics for non-determinism and sequence points in C

Robbert Krebbers

An operational and axiomatic semantics for non-determinism and sequence points in C

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

A Galois connection calculus for abstract interpretation

Patrick Cousot, Radhia Cousot

A Galois connection calculus for abstract interpretation

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

A constraint-based approach to solving games on infinite graphs

Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko

A constraint-based approach to solving games on infinite graphs

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

Verifying eventual consistency of optimistic replication systems

Ahmed Bouajjani, Constantin Enea, Jad Hamza

Verifying eventual consistency of optimistic replication systems

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

Tabular: a schema-driven probabilistic programming language

Andrew D. Gordon, Thore Graepel, Nicolas Rolland, Claudio V. Russo, Johannes Borgström, John Guiver

Tabular: a schema-driven probabilistic programming language

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

Minimization of symbolic automata

Loris D'Antoni, Margus Veanes

Minimization of symbolic automata

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

From parametricity to conservation laws, via Noether's theorem

Robert Atkey

From parametricity to conservation laws, via Noether's theorem

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

Bridging boolean and quantitative synthesis using smoothed proof search

Swarat Chaudhuri, Martin Clochard, Armando Solar-Lezama

Bridging boolean and quantitative synthesis using smoothed proof search

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

Symbolic optimization with SMT solvers

Yi Li, Aws Albarghouthi, Zachary Kincaid, Arie Gurfinkel, Marsha Chechik

Symbolic optimization with SMT solvers

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

Parametric completeness for separation theories

James Brotherston, Jules Villard

Parametric completeness for separation theories

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

Abstract satisfaction

Vijay D'Silva, Leopold Haller, Daniel Kroening

Abstract satisfaction

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

Freeze after writing: quasi-deterministic parallel programming with LVars

Lindsey Kuper, Aaron Turon, Neelakantan R. Krishnaswami, Ryan R. Newton

Freeze after writing: quasi-deterministic parallel programming with LVars

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

Consistency analysis of decision-making programs

Swarat Chaudhuri, Azadeh Farzan, Zachary Kincaid

Consistency analysis of decision-making programs

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

Counter-factual typing for debugging type errors

Sheng Chen, Martin Erwig

Counter-factual typing for debugging type errors

Details
Author Comments:
Discussion Comments: 0
Sharing: Not able to share produced artifacts
Verification: Authors have verified information

Closed type families with overlapping equations

Richard A. Eisenberg, Dimitrios Vytiniotis, Simon L. Peyton Jones, Stephanie Weirich

Closed type families with overlapping equations

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

A sound and complete abstraction for reasoning about parallel prefix sums

Nathan Chong, Alastair F. Donaldson, Jeroen Ketema

A sound and complete abstraction for reasoning about parallel prefix sums

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

NetkAT: semantic foundations for networks

Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, David Walker

NetkAT: semantic foundations for networks

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

Backpack: retrofitting Haskell with interfaces

Scott Kilpatrick, Derek Dreyer, Simon L. Peyton Jones, Simon Marlow

Backpack: retrofitting Haskell with interfaces

Details
Author Comments: The technical appendix of our paper, which contains paper-and-pencil proof sketches of the main results, is available at: http://plv.mpi-sws.org/backpack/. (This is not what is typically referred to as an "artifact".)
Discussion Comments: 0
Sharing: Research produced no artifacts
Verification: Authors have verified information

Sound compilation of reals

Eva Darulova, Viktor Kuncak

Sound compilation of reals

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

Modular reasoning about heap paths via effectively propositional formulas

Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv

Modular reasoning about heap paths via effectively propositional formulas

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

Modular reasoning about concurrent higher-order imperative programs

Lars Birkedal

Modular reasoning about concurrent higher-order imperative programs

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

Game semantics for interface middleweight Java

Andrzej S. Murawski, Nikos Tzevelekos

Game semantics for interface middleweight Java

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

Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation

Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet, Luca Padovani

Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation

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