| 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 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 |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
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
|
|
Andrew Cave, Francisco Ferreira, Prakash Panangaden, Brigitte Pientka |
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
|
|
Stephen Chang, Matthias Felleisen |
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
|
|
Udi Boker, Thomas A. Henzinger, Arjun Radhakrishna |
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
|
|
Azadeh Farzan, Zachary Kincaid, Andreas Podelski |
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 JavaScript specification Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, Gareth Smith |
A trusted mechanised JavaScript 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
|
|
Stephen Brookes, Peter W. O'Hearn, Uday S. Reddy |
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
|
|
Vijay D'Silva, Leopold Haller, Daniel Kroening |
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
|
|
Eva Darulova, Viktor Kuncak |
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
|