| 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 |
|---|
|
Serializability for eventual consistency: criterion, analysis, and applications Lucas Brutschy, Dimitar Dimitrov, Peter Müller, Martin T. Vechev |
Serializability for eventual consistency: criterion, analysis, and applications 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
|
|
Deciding equivalence with sums and the empty type Gabriel Scherer |
Deciding equivalence with sums and the empty type Details |
|
Discussion Comments:
0
Verification:
Author has
not verified
information
|
|
A semantic account of metric preservation Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, Ikram Cherigui |
A semantic account of metric preservation Details |
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced no artifacts
Verification:
Authors have
verified
information
|
|
Exact Bayesian inference by symbolic disintegration Chung-chieh Shan, Norman Ramsey |
Exact Bayesian inference by symbolic disintegration Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
Intersection type calculi of bounded dimension Andrej Dudenhefner, Jakob Rehof |
Intersection type calculi of bounded dimension Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Towards automatic resource bound analysis for OCaml Jan Hoffmann, Ankush Das, Shu-Chun Weng |
Towards automatic resource bound analysis for OCaml 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:
This provides a type system for inferring resource bounds on programs written in OCaml. The type system also supports automatic type inference, hence these bounds are inferred automatically.
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
Type directed compilation of row-typed algebraic effects Daan Leijen |
Type directed compilation of row-typed algebraic effects Details |
Discussion Comments:
0
Verification:
Author has
not verified
information
|
|
|
The geometry of parallelism: classical, probabilistic, and quantum effects Ugo Dal Lago, Claudia Faggian, Benoît Valiron, Akira Yoshimizu |
The geometry of parallelism: classical, probabilistic, and quantum effects Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
The exp-log normal form of types: decomposing extensional equality and representing terms compactly Danko Ilik |
The exp-log normal form of types: decomposing extensional equality and representing terms compactly 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
|
|
Hypercollecting semantics and its application to static analysis of information flow Mounir Assaf, David A. Naumann, Julien Signoles, Eric Totel, Frédéric Tronel |
Hypercollecting semantics and its application to static analysis of information flow Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
Ananya Kumar, Guy E. Blelloch, Robert Harper |
Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Complexity verification using guided theorem enumeration Akhilesh Srikanth, Burak Sahin, William R. Harris |
Complexity verification using guided theorem enumeration Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Big types in little runtime: open-world soundness and collaborative blame for gradual type systems Michael M. Vitousek, Cameron Swords, Jeremy G. Siek |
Big types in little runtime: open-world soundness and collaborative blame for gradual type systems 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
|
|
Hazelnut: a bidirectionally typed structure editor calculus Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, Matthew A. Hammer |
Hazelnut: a bidirectionally typed structure editor calculus Details |
Author Comments:
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
Fast polyhedra abstract domain Gagandeep Singh, Markus Püschel, Martin T. Vechev |
Fast polyhedra abstract domain Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Paul Blain Levy |
Details |
|
Discussion Comments:
0
Verification:
Author has
not verified
information
|
|
Genesis: synthesizing forwarding tables in multi-tenant networks Kausik Subramanian, Loris D'Antoni, Aditya Akella |
Genesis: synthesizing forwarding tables in multi-tenant networks Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Stephen Chang, Alex Knauth, Ben Greenman |
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
|
|
Sums of uncertainty: refinements go gradual Khurram A. Jafery, Joshua Dunfield |
Sums of uncertainty: refinements go gradual Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Coming to terms with quantified reasoning Laura Kovács, Simon Robillard, Andrei Voronkov |
Coming to terms with quantified reasoning Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Fencing off go: liveness and safety for channel-based programming Julien Lange, Nicholas Ng, Bernardo Toninho, Nobuko Yoshida |
Fencing off go: liveness and safety for channel-based programming 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
|
|
Eryk Kopczynski, Szymon Torunczyk |
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
|
|
Igor V. Konnov, Marijana Lazic, Helmut Veith, Josef Widder |
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
|
|
Contract-based resource verification for higher-order functions with memoization Ravichandhran Madhavan, Sumith Kulal, Viktor Kuncak |
Contract-based resource verification for higher-order functions with memoization 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
|
|
Modules, abstraction, and parametric polymorphism Karl Crary |
Modules, abstraction, and parametric polymorphism 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
|
|
On the relationship between higher-order recursion schemes and higher-order fixpoint logic Naoki Kobayashi, Étienne Lozes, Florian Bruse |
On the relationship between higher-order recursion schemes and higher-order fixpoint logic Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Computational higher-dimensional type theory Carlo Angiuli, Robert Harper, Todd Wilson |
Computational higher-dimensional type theory Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann |
Details |
Author Comments:
Technical appendix is provided.
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
|
Mixed-size concurrency: ARM, POWER, C/C++11, and SC Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, Peter Sewell |
Mixed-size concurrency: ARM, POWER, C/C++11, and SC Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Taro Sekiyama, Atsushi Igarashi |
Details |
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced no artifacts
Verification:
Authors have
verified
information
|
|
Thread modularity at many levels: a pearl in compositional verification Jochen Hoenicke, Rupak Majumdar, Andreas Podelski |
Thread modularity at many levels: a pearl in compositional verification Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Automatically comparing memory consistency models John Wickerson, Mark Batty, Tyler Sorensen, George A. Constantinides |
Automatically comparing memory consistency models 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
|
|
Cantor meets scott: semantic foundations for probabilistic networks Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, Alexandra Silva |
Cantor meets scott: semantic foundations for probabilistic networks 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
|
|
Beginner's luck: a language for property-based generators Leonidas Lampropoulos, Diane Gallois-Wong, Catalin Hritcu, John Hughes, Benjamin C. Pierce, Li-yao Xia |
Beginner's luck: a language for property-based generators Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
A promising semantics for relaxed-memory concurrency Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer |
A promising semantics for relaxed-memory concurrency 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:
The alternative URL above is to the author-prepared version of the paper with the appendix.
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
LightDP: towards automating differential privacy proofs Danfeng Zhang, Daniel Kifer |
LightDP: towards automating differential privacy proofs Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Rigorous floating-point mixed-precision tuning Wei-Fan Chiang, Mark Baranowski, Ian Briggs, Alexey Solovyev, Ganesh Gopalakrishnan, Zvonimir Rakamaric |
Rigorous floating-point mixed-precision tuning 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
|
|
Sam Lindley, Conor McBride, Craig McLaughlin |
Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Analyzing divergence in bisimulation semantics Xinxin Liu, Tingting Yu, Wenhui Zhang |
Analyzing divergence in bisimulation semantics Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
A posteriori environment analysis with Pushdown Delta CFA Kimball Germane, Matthew Might |
A posteriori environment analysis with Pushdown Delta CFA Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Ogre and Pythia: an invariance proof method for weak consistency models Jade Alglave, Patrick Cousot |
Ogre and Pythia: an invariance proof method for weak consistency models Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
On verifying causal consistency Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, Jad Hamza |
On verifying causal consistency Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Invariants of quantum programs: characterisations and generation Mingsheng Ying, Shenggang Ying, Xiaodi Wu |
Invariants of quantum programs: characterisations and generation Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
A program optimization for automatic database result caching Ziv Scully, Adam Chlipala |
A program optimization for automatic database result caching 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
|
|
Dynamic race detection for C++11 Christopher Lidbury, Alastair F. Donaldson |
Dynamic race detection for C++11 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
|
|
Type soundness proofs with definitional interpreters Nada Amin, Tiark Rompf |
Type soundness proofs with definitional interpreters 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
|
|
Stochastic invariants for probabilistic termination Krishnendu Chatterjee, Petr Novotný, Dorde Zikelic |
Stochastic invariants for probabilistic termination Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Monadic second-order logic on finite sequences Loris D'Antoni, Margus Veanes |
Monadic second-order logic on finite sequences 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
|
|
Context-sensitive data-dependence analysis via linear conjunctive language reachability Qirun Zhang, Zhendong Su |
Context-sensitive data-dependence analysis via linear conjunctive language reachability Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Typed self-evaluation via intensional type functions Matt Brown, Jens Palsberg |
Typed self-evaluation via intensional type functions 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
|
|
Nico Lehmann, Éric Tanter |
Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Polymorphism, subtyping, and type inference in MLsub Stephen Dolan, Alan Mycroft |
Polymorphism, subtyping, and type inference in MLsub 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
|
|
Component-based synthesis for complex APIs Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, Thomas W. Reps |
Component-based synthesis for complex APIs Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Coupling proofs are probabilistic product programs Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub |
Coupling proofs are probabilistic product programs Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Java generics are turing complete Radu Grigore |
Java generics are turing complete Details |
Discussion Comments:
0
Verification:
Author has
not verified
information
|
|
|
The influence of dependent types (keynote) Stephanie Weirich |
The influence of dependent types (keynote) Details |
|
Discussion Comments:
0
Verification:
Author has
not verified
information
|
|
QWIRE: a core language for quantum circuits Jennifer Paykin, Robert Rand, Steve Zdancewic |
QWIRE: a core language for quantum circuits Details |
|
Author Comments:
Discussion Comments:
0
Sharing:
Research produced no artifacts
Verification:
Authors have
verified
information
|
|
Rust: from POPL to practice (keynote) Aaron Turon |
Rust: from POPL to practice (keynote) Details |
|
Discussion Comments:
0
Verification:
Author has
not verified
information
|
|
LMS-Verify: abstraction without regret for verified systems programming Nada Amin, Tiark Rompf |
LMS-Verify: abstraction without regret for verified systems programming Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Stream fusion, to completeness Oleg Kiselyov, Aggelos Biboudis, Nick Palladinos, Yannis Smaragdakis |
Stream fusion, to completeness 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:
The alternative (ArXiv) version of the paper includes the appendices (skipped in the version published in the POPL proceedings)
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
Joshua Moerman, Matteo Sammartino, Alexandra Silva, Bartek Klin, Michal Szynwelski |
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
|
|
Interactive proofs in higher-order concurrent separation logic Robbert Krebbers, Amin Timany, Lars Birkedal |
Interactive proofs in higher-order concurrent separation logic 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 relational model of types-and-effects in higher-order concurrent separation logic Morten Krogh-Jespersen, Kasper Svendsen, Lars Birkedal |
A relational model of types-and-effects in higher-order concurrent separation logic Details |
|
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
Semantic-directed clumping of disjunctive abstract states Huisong Li, Francois Berenger, Bor-Yuh Evan Chang, Xavier Rival |
Semantic-directed clumping of disjunctive abstract states 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:
Semantic-Directed Clumping of Disjunctive Abstract States, ACM Symposium on Principles of Programming Languages (POPL 2017), 2017 Huisong Li, Francois Berenger, Bor-Yuh Evan Chang and Xavier Rival. In Principles Of Programming Languages 2017 (POPL'17), Paris, Jan. 2017.
Discussion Comments:
0
Sharing:
Research produced artifacts
Verification:
Authors have
verified
information
|
|
Automatically generating the dynamic semantics of gradually typed languages Matteo Cimini, Jeremy G. Siek |
Automatically generating the dynamic semantics of gradually typed languages Details |
Discussion Comments:
0
Verification:
Authors have
not verified
information
|
|
|
Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy |
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
|