ACM Principles of Programming Languages, POPL 2017


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

Parallel functional arrays

Ananya Kumar, Guy E. Blelloch, Robert Harper

Parallel functional arrays

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

Contextual isomorphisms

Paul Blain Levy

Contextual isomorphisms

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

Type systems as macros

Stephen Chang, Alex Knauth, Ben Greenman

Type systems as macros

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

LOIS: syntax and semantics

Eryk Kopczynski, Szymon Torunczyk

LOIS: syntax and semantics

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 short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms

Igor V. Konnov, Marijana Lazic, Helmut Veith, Josef Widder

A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms

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

Relational cost analysis

Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann

Relational cost analysis

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

Stateful manifest contracts

Taro Sekiyama, Atsushi Igarashi

Stateful manifest contracts

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

Do be do be do

Sam Lindley, Conor McBride, Craig McLaughlin

Do be do be do

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

Gradual refinement types

Nico Lehmann, Éric Tanter

Gradual refinement types

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

Learning nominal automata

Joshua Moerman, Matteo Sammartino, Alexandra Silva, Bartek Klin, Michal Szynwelski

Learning nominal automata

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

Dijkstra monads for free

Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martinez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy

Dijkstra monads for free

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