POPL 2017
Sun 15 - Sat 21 January 2017

This is the main track of POPL 2017, featuring research papers and invited talks. Please select a tab for more information.

News

The POPL 2017 program is available.

The full POPL 2017 proceedings are accessible.

Dates
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Wed 18 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 09:05
OpeningPOPL at Auditorium
Chair(s): Giuseppe Castagna Paris Diderot University & CNRS, Andrew D. Gordon Microsoft Research and University of Edinburgh
09:00
5m
Day opening
Opening
POPL

09:05 - 10:00
Invited speakerPOPL at Auditorium
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
09:05
55m
Talk
The Influence of Dependent Types
POPL
Stephanie Weirich University of Pennsylvania
10:30 - 12:10
Abstract InterpretationPOPL at Amphitheater 44
Chair(s): Isabella Mastroeni University of Verona, Italy
10:30
25m
Talk
Ogre and Pythia, An invariance proof method for weak consistency models
POPL
Jade Alglave University College London, Patrick Cousot New York University
10:55
25m
Talk
A Posteriori Environment Analysis with Pushdown Delta CFA
POPL
Kimball Germane University of Utah, Matthew Might University of Utah; Harvard Medical School; The White House
11:20
25m
Talk
Semantic-Directed Clumping of Disjunctive Abstract States
POPL
Huisong Li INRIA/CNRS/ENS/PSL*, François Bérenger INRIA/CNRS/ENS/PSL*, Bor-Yuh Evan Chang University of Colorado Boulder, Xavier Rival INRIA/CNRS/ENS Paris
11:45
25m
Talk
Fast Polyhedra Abstract Domain
POPL
Gagandeep Singh ETH Zurich, Switzerland, Markus Püschel ETH Zurich, Martin Vechev ETH Zurich
10:30 - 12:10
Type Systems 1POPL at Auditorium
Chair(s): Avik Chaudhuri Facebook
10:30
25m
Talk
Polymorphism, subtyping and type inference in MLsub
POPL
Stephen Dolan , Alan Mycroft University of Cambridge
10:55
25m
Talk
Java generics are Turing complete
POPL
Radu Grigore University of Kent
11:20
25m
Talk
Hazelnut: A Bidirectionally Typed Structure Editor Calculus
POPL
Cyrus Omar Carnegie Mellon University, Ian Voysey Carnegie Mellon University, Michael Hilton Oregon State University, USA, Jonathan Aldrich Carnegie Mellon University, Matthew Hammer University of Colorado, Boulder
11:45
25m
Talk
Modules, Abstraction, and Parametric Polymorphism
POPL
Karl Crary Carnegie Mellon University
14:20 - 16:00
Probabilistic ProgrammingPOPL at Amphitheater 44
Chair(s): Marco Gaboardi SUNY Buffalo, USA
14:20
25m
Talk
Beginner's Luck: A Language for Property-Based Generators
POPL
Leonidas Lampropoulos University of Pennsylvania, Diane Gallois-Wong Inria Paris, ENS Paris, Cătălin Hriţcu Inria Paris, John Hughes Chalmers University of Technology, Benjamin C. Pierce University of Pennsylvania, Li-yao Xia ENS Paris
Pre-print
14:45
25m
Talk
Exact Bayesian Inference by Symbolic Disintegration
POPL
Chung-chieh Shan Indiana University, USA, Norman Ramsey
Pre-print
15:10
25m
Talk
Stochastic Invariants for Probabilistic Termination
POPL
Krishnendu Chatterjee IST Austria, Petr Novotný IST Austria, Djordje Zikelic University of Cambridge
15:35
25m
Talk
Coupling proofs are probabilistic product programs
POPL
Gilles Barthe IMDEA, Benjamin Gregoire INRIA, Justin Hsu , Pierre-Yves Strub École Polytechnique
14:20 - 16:00
Concurrency 1POPL at Auditorium
Chair(s): Ilya Sergey University College London
14:20
25m
Talk
A Promising Semantics for Relaxed-Memory Concurrency
POPL
Jeehoon Kang Seoul National University, Chung-Kil Hur Seoul National University, Ori Lahav MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany, Derek Dreyer MPI-SWS
Link to publication Pre-print Media Attached
14:45
25m
Talk
Automatically Comparing Memory Consistency Models
POPL
John Wickerson Imperial College London, Mark Batty University of Kent, Tyler Sorensen Imperial College London, George A. Constantinides Imperial College London, UK
Pre-print Media Attached File Attached
15:10
25m
Talk
Interactive Proofs in Higher-Order Concurrent Separation Logic
POPL
Robbert Krebbers Delft University of Technology, Netherlands, Amin Timany imec - Distrinet, KU Leuven, Lars Birkedal Aarhus University
DOI Pre-print Media Attached
15:35
25m
Talk
A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic
POPL
Morten Krogh-Jespersen Aarhus University, Kasper Svendsen Aarhus University, Lars Birkedal Aarhus University
16:30 - 17:45
LogicPOPL at Amphitheater 44
Chair(s): Alexandra Silva University College London
16:30
25m
Talk
Monadic second-order logic on finite sequences
POPL
Loris D'Antoni University of Wisconsin–Madison, Margus Veanes Microsoft Research
16:55
25m
Talk
On the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic
POPL
Naoki Kobayashi University of Tokyo, Japan, Etienne Lozes ENS Cachan, Florian Bruse University of Kassel
17:20
25m
Talk
Coming to Terms with Quantified Reasoning
POPL
Simon Robillard Chalmers University of Technology, Andrei Voronkov University of Manchester, Laura Kovacs Chalmers University of Technology
16:30 - 17:45
Compiler OptimisationPOPL at Auditorium
Chair(s): Andrew C. Myers Cornell University
16:30
25m
Talk
A Program Optimization for Automatic Database Result Caching
POPL
Ziv Scully Carnegie Mellon University, Adam Chlipala MIT
16:55
25m
Talk
Stream Fusion, to Completeness
POPL
Oleg Kiselyov , Aggelos Biboudis University of Athens, Nick Palladinos Nessos Information Technologies, SA, Yannis Smaragdakis University of Athens
Pre-print Media Attached
17:20
25m
Talk
Rigorous Floating-point Mixed Precision Tuning
POPL
Wei-Fan Chiang School of Computing, University of Utah, Ganesh Gopalakrishnan University of Utah, Zvonimir Rakamaric University of Utah, Ian Briggs School of Computing, University of Utah, Marek S. Baranowski University of Utah, Alexey Solovyev School of Computing, University of Utah
Pre-print

Thu 19 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 09:15
ACM and SIGPLAN AwardsPOPL at Auditorium
Chair(s): Satnam Singh Facebook
09:00
5m
Awards
Turing Award Video
POPL

09:05
5m
Awards
Most Influential Paper Award
POPL

09:10
5m
Awards
Reynolds Doctoral Dissertation Award
POPL

09:15 - 10:00
Invited speakerPOPL at Auditorium
Chair(s): Roberto Giacobazzi University of Verona, Italy
09:15
45m
Talk
40 Years of Abstract Interpretation — An Interview with Patrick Cousot
POPL
Patrick Cousot New York University, Roberto Giacobazzi University of Verona, Italy
10:30 - 12:10
Program AnalysisPOPL at Amphitheater 44
Chair(s): Francesco Logozzo Facebook
10:30
25m
Talk
Relational Cost Analysis
POPL
Ezgi Çiçek MPI-SWS, Germany, Gilles Barthe IMDEA, Marco Gaboardi SUNY Buffalo, USA, Deepak Garg MPI-SWS, Germany, Jan Hoffmann Carnegie Mellon University
10:55
25m
Talk
Contract-based Resource Verification for Higher-order Functions with Memoization
POPL
Ravichandhran Madhavan EPFL, Sumith Kulal IIT Bombay, Viktor Kunčak EPFL, Switzerland
11:20
25m
Talk
Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability
POPL
Qirun Zhang University of California, Davis, Zhendong Su University of California, Davis
11:45
25m
Talk
Towards Automatic Resource Bound Analysis for OCaml
POPL
Jan Hoffmann Carnegie Mellon University, Ankush Das Carnegie Mellon University, Shu-chun Weng Yale University
10:30 - 12:10
Type Systems 2POPL at Auditorium
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
10:30
25m
Talk
Deciding equivalence with sums and the empty type
POPL
Gabriel Scherer Northeastern University
10:55
25m
Talk
The exp-log normal form of types: Decomposing extensional equality and representing terms compactly
POPL
Danko Ilik Trusted Labs
11:20
25m
Talk
Contextual isomorphisms
POPL
11:45
25m
Talk
Typed Self-Evaluation via Intensional Type Functions
POPL
Matt Brown UCLA, Jens Palsberg University of California, Los Angeles
14:20 - 16:00
Concurrency 2POPL at Amphitheater 44
Chair(s): Nobuko Yoshida Imperial College London, UK
14:20
25m
Talk
Mixed-size Concurrency: ARM, POWER, C/C++11, and SC
POPL
Shaked Flur University of Cambridge, Susmit Sarkar University of St. Andrews, UK, Christopher Pulte University of Cambridge, Kyndylan Nienhuis University of Cambridge, Luc Maranget INRIA Rocquencourt, Kathryn E. Gray University of Cambridge, Ali Sezgin University of Cambridge, Mark Batty University of Kent, Peter Sewell University of Cambridge
14:45
25m
Talk
Dynamic Race Detection For C++11
POPL
Christopher Lidbury Imperial College London, Alastair F. Donaldson Imperial College London
15:10
25m
Talk
Serializability for Eventual Consistency: Criterion, Analysis and Applications
POPL
Lucas Brutschy ETH Zurich, Dimitar Dimitrov ETH Zurich, Switzerland, Peter Müller ETH Zurich, Martin Vechev ETH Zurich
Pre-print
15:35
25m
Talk
Thread Modularity at Many Levels: a Pearl in Compositional Verification
POPL
Jochen Hoenicke Universität Freiburg, Rupak Majumdar MPI-SWS, Andreas Podelski University of Freiburg, Germany
14:20 - 16:00
Functional Programming with EffectsPOPL at Auditorium
Chair(s): Kathleen Fisher Tufts University
14:20
25m
Talk
Type Directed Compilation of Row-Typed Algebraic Effects
POPL
Daan Leijen Microsoft Research
14:45
25m
Talk
Do be do be do
POPL
Sam Lindley University of Edinburgh, Conor McBride , Craig McLaughlin The University of Edinburgh
15:10
25m
Talk
Dijkstra Monads for Free
POPL
Danel Ahman University of Edinburgh, Cătălin Hriţcu Inria Paris, Kenji Maillard Inria Paris, ENS Paris, and Microsoft Research, Guido Martínez CIFASIS-CONICET, Argentina, Gordon Plotkin , Jonathan Protzenko Microsoft Research, Aseem Rastogi Microsoft Research India, Nikhil Swamy Microsoft Research
Pre-print
15:35
25m
Talk
Stateful Manifest Contracts
POPL
Taro Sekiyama , Atsushi Igarashi Kyoto University
16:30 - 17:20
Semantic FoundationsPOPL at Amphitheater 44
Chair(s): Lars Birkedal Aarhus University
16:30
25m
Talk
A Semantic Account of Metric Preservation
POPL
Arthur Azevedo de Amorim University of Pennsylvania, USA, Ikram Cherigui ENS Paris, Marco Gaboardi SUNY Buffalo, USA, Justin Hsu , Shin-ya Katsumata Kyoto University
16:55
25m
Talk
Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
POPL
Steffen Smolka Cornell University, Praveen Kumar Cornell University, Nate Foster Cornell University, Dexter Kozen Cornell University, Alexandra Silva University College London
DOI File Attached
16:30 - 17:20
Logic and ProgrammingPOPL at Auditorium
Chair(s): Nada Amin EPFL
16:30
25m
Talk
Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks
POPL
Kausik Subramanian University of Wisconsin-Madison, Loris D'Antoni University of Wisconsin–Madison, Aditya Akella University of Wisconsin-Madison
16:55
25m
Talk
LOIS: syntax and semantics
POPL
17:20 - 18:20
Business meetingPOPL at Auditorium
Chair(s): Andrew D. Gordon Microsoft Research and University of Edinburgh
17:20
20m
Talk
PC Chair report
POPL
Andrew D. Gordon Microsoft Research and University of Edinburgh
17:40
10m
Talk
POPL 2018 presentation
POPL
Andrew C. Myers Cornell University, Ranjit Jhala University of California, San Diego
17:50
30m
Meeting
SIGPLAN business meeting
POPL
C: Andrew D. Gordon Microsoft Research and University of Edinburgh

Fri 20 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:05 - 10:00
Invited speakerPOPL at Auditorium
Chair(s): Giuseppe Castagna Paris Diderot University & CNRS
09:05
55m
Talk
Rust: from POPL to practice
POPL
Aaron Turon MPI-SWS
10:30 - 12:10
Verification and SynthesisPOPL at Amphitheater 44
Chair(s): Benjamin Delaware Purdue University
10:30
25m
Talk
Component-Based Synthesis for Complex APIs
POPL
Yu Feng University of Texas at Austin, USA, Ruben Martins , Yuepeng Wang University of Texas at Austin, Isil Dillig UT Austin, Thomas Reps University of Wisconsin - Madison and Grammatech Inc.
10:55
25m
Talk
Learning nominal automata
POPL
Joshua Moerman Radboud University, Matteo Sammartino University College London, Alexandra Silva University College London, Bartek Klin University of Warsaw, Michał Szynwelski University of Warsaw
11:20
25m
Talk
On Verifying Causal Consistency
POPL
Ahmed Bouajjani IRIF, Université Paris Diderot, Constantin Enea LIAFA, Université Paris Diderot, Rachid Guerraoui , Jad Hamza LIAFA, Université Paris Diderot
11:45
25m
Talk
Complexity Verification Using Guided Theorem Enumeration
POPL
Akhilesh Srikanth Georgia Institute of Technology, Burak Sahin Georgia Institute of Technology, William Harris
10:30 - 12:10
Type Systems 3POPL at Auditorium
Chair(s): Derek Dreyer MPI-SWS
10:30
25m
Talk
Intersection Type Calculi of Bounded Dimension
POPL
Andrej Dudenhefner Technical University Dortmund, Jakob Rehof Technical University Dortmund
10:55
25m
Talk
Type Soundness Proofs with Definitional Interpreters
POPL
Nada Amin EPFL, Tiark Rompf Purdue University
11:20
25m
Talk
Computational Higher-Dimensional Type Theory
POPL
Carlo Angiuli Carnegie Mellon University, Robert Harper , Todd Wilson California State University Fresno
11:45
25m
Talk
Type Systems as Macros
POPL
Stephen Chang Northeastern University, Alex Knauth Northeastern University, Ben Greenman Northeastern University
14:20 - 16:00
Concurrency 3POPL at Amphitheater 44
Chair(s): Adam Chlipala MIT
14:20
25m
Talk
Parallel Functional Arrays
POPL
Ananya Kumar , Guy E. Blelloch Carnegie Mellon University, Robert Harper
14:45
25m
Talk
A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms
POPL
Igor Konnov TU Wien, Marijana Lazić TU Wien, Helmut Veith TU Wien, Josef Widder TU Wien
DOI Pre-print
15:10
25m
Talk
Analyzing divergence in bisimulation semantics
POPL
Xinxin Liu Institute of software, Chinese academy of sciences, Tingting Yu , Wenhui Zhang Institute of software, Chinese academy of sciences
15:35
25m
Talk
Fencing off Go: Liveness and Safety for Channel-Based Programming
POPL
Julien Lange Imperial College London, Nicholas Ng Imperial College London, Bernardo Toninho Imperial College London, Nobuko Yoshida Imperial College London, UK
Pre-print
14:20 - 16:00
Gradual Typing and ContractsPOPL at Auditorium
Chair(s): Ronald Garcia University of British Columbia
14:20
25m
Talk
Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System
POPL
Michael Vitousek , Cameron Swords Indiana University, Jeremy G. Siek Indiana University Bloomington
14:45
25m
Talk
Gradual Refinement Types
POPL
Nicolás Lehmann , Éric Tanter University of Chile, Chile
Link to publication DOI Pre-print
15:10
25m
Talk
Automatically Generating the Dynamic Semantics of Gradually Typed Languages
POPL
Matteo Cimini Indiana University, USA, Jeremy G. Siek Indiana University Bloomington
15:35
25m
Talk
Sums of Uncertainty: Refinements go gradual
POPL
Khurram A. Jafery University of British Columbia, Jana Dunfield University of British Columbia
16:30 - 17:45
QuantumPOPL at Amphitheater 44
Chair(s): Michele Pagani IRIF, Université Paris Diderot
16:30
25m
Talk
Invariants of Quantum Programs: Characterisations and Generation
POPL
Mingsheng Ying University of Technology Sydney, Australia, Shenggang Ying University of Technology Sydney, Australia, Xiaodi Wu University of Oregon, USA
16:55
25m
Talk
The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects
POPL
Ugo Dal Lago University of Bologna, France, Claudia Faggian , Benoit Valiron LRI, CentraleSupelec, Univ. Paris Saclay, Akira Yoshimizu Univ.Tokyo
17:20
25m
Talk
QWIRE: A Core Language for Quantum Circuits
POPL
Jennifer Paykin , Robert Rand University of Pennsylvania, Steve Zdancewic University of Pennsylvania
16:30 - 17:45
Security and PrivacyPOPL at Auditorium
Chair(s): Cătălin Hriţcu Inria Paris
16:30
25m
Talk
LMS-Verify: Abstraction Without Regret for Verified Systems Programming
POPL
Nada Amin EPFL, Tiark Rompf Purdue University
16:55
25m
Talk
Hypercollecting Semantics and its Application to Static Analysis of Information Flow
POPL
Mounir Assaf Stevens Institute of Technology, David Naumann Stevens Institute of Technology, Julien Signoles CEA LIST, Éric Totel CentraleSupélec, Frédéric Tronel CentraleSupélec
17:20
25m
Talk
LightDP: Towards Automating Differential Privacy Proofs
POPL
Danfeng Zhang Pennsylvania State University, Daniel Kifer Dept. of Computer Science and Engineering, Penn State University

Call for Papers

Scope

The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome, on topics ranging from formal frameworks to experience reports. Papers discussing new ideas and new areas are encouraged, as are papers (often called “pearls”) that elucidate existing concepts in ways that yield new insights. We are looking for any submission with the potential to make enduring contributions to the theory, design, implementation or application of programming languages.

The symposium is sponsored by ACM SIGPLAN, in cooperation with ACM SIGACT and ACM SIGLOG.

Evaluation

The Program Committee will evaluate the technical contribution of each submission as well as its accessibility to both experts and the general POPL audience. All papers will be judged on significance, originality, relevance, correctness, and clarity.

Explaining a known idea in a new way may make as strong a contribution as inventing a new idea. Hence, we encourage the submission of pearls: elegant essays that explain an old idea, but do so in a new way that clarifies the idea and yields new insights. There is no formal separation of categories; pearls will be held to the same standards as any other paper.

Each paper should explain its contributions in both general and technical terms, identifying what has been accomplished, explaining why it is significant, and comparing it with previous work. Authors should strive to make their papers understandable to a broad audience. Advice on writing technical papers can be found on the SIGPLAN author information page.

A document that details principles underlying organizational and reviewing policies can be found here.

A document containing frequently asked questions about the reviewing and submission process, especially as it pertains to double-blind reviewing, can be found here.

The Program Committee, displayed to the right, meets face-to-face to make the final selection; the Program Committee is assisted by a larger External Review Committee, also displayed to the right. PC papers are reviewed and selected entirely by the ERC.

Submission guidelines

Prior to the registration deadline, the authors will register their paper by uploading information on the submission title, abstract (of at most 300 words), authors, topics, and conflicts to the conference web site. Papers that are not registered on time will be rejected.

Prior to the final paper submission deadline, the authors will upload their full paper in double blind format and formatted according to the ACM proceedings format. Each paper should have no more than 12 pages of text, excluding bibliography, in 9 pt format. Papers may be resubmitted multiple times up until the deadline. The last version submitted before the deadline will be the version that is reviewed. Papers that exceed the length requirement or deviate from the expected format or are submitted late will be rejected.

Deadlines expire at midnight anywhere on earth on the Important Dates displayed to the right.

Templates for ACM format are available for Microsoft Word and LaTeX at http://www.sigplan.org/Resources/Author (use the 9 pt preprint template). Submissions should be in PDF and printable on US Letter and A4 sized paper.

Submitted papers must adhere to the SIGPLAN Republication Policy and the ACM Policy on Plagiarism. Concurrent submissions to other conferences, workshops, journals, or similar forums of publication are not allowed.

POPL 2017 will employ a lightweight double-blind reviewing process. To facilitate this, submitted papers must adhere to two rules:

  1. author names and institutions must be omitted, and
  2. references to authors’ own related work should be in the third person (e.g., not “We build on our previous work …” but rather “We build on the work of …”).

The purpose of this process is to help the PC and external reviewers come to an initial judgement about the paper without bias, not to make it impossible for them to discover the authors if they were to try. Nothing should be done in the name of anonymity that weakens the submission or makes the job of reviewing the paper more difficult (e.g., important background references should not be omitted or anonymized). In addition, authors should feel free to disseminate their ideas or draft versions of their paper as they normally would. For instance, authors may post drafts of their papers on the web or give talks on their research ideas. A document answering frequently asked questions should address many common concerns.

The submission itself is the object of review and so it should strive to convince the reader of at least the plausibility of reported results. Still, we encourage authors to provide any supplementary material that is required to support the claims made in the paper, such as detailed proofs, proof scripts, or experimental data. These materials should be uploaded at submission time, as a single pdf or a tarball, not via a URL. Two forms of supplementary material may be submitted.

  1. Anonymous supplementary material is available to the reviewers before they submit their first-draft reviews.
  2. Non-anonymous supplementary material is available to the reviewers after they have submitted their first-draft reviews and learnt the identity of the authors.

Use the anonymous form if possible. Reviewers are under no obligation to look at the supplementary material but may refer to it if they have questions about the material in the body of the paper.

Artifact Evaluation

Authors of accepted papers will be invited to formally submit supporting materials to the Artifact Evaluation process. Artifact Evaluation is run by a separate committee whose task is to assess how the artifacts support the work described in the papers. This submission is voluntary and will not influence the final decision regarding the papers. Papers that go through the Artifact Evaluation process successfully will receive a seal of approval printed on the papers themselves. Authors of accepted papers are encouraged to make these materials publicly available upon publication of the proceedings, by including them as “source materials” in the ACM Digital Library.

Publication

Final versions of accepted papers are allowed up to 12 pages excluding the bibliography. In addition, at most two additional pages may be purchased at $200 per page. This additional amount will be due at registration for the conference.

AUTHORS TAKE NOTE: The official publication date is the date the proceedings are made available in the ACM Digital Library. This date may be up to two weeks prior to the first day of your conference. The official publication date affects the deadline for any patent filings related to published work. (For those rare conferences whose proceedings are published in the ACM Digital Library after the conference is over, the official publication date remains the first day of the conference.)

Accepted Papers

Title
A Posteriori Environment Analysis with Pushdown Delta CFA
POPL
A Program Optimization for Automatic Database Result Caching
POPL
A Promising Semantics for Relaxed-Memory Concurrency
POPL
Link to publication Pre-print Media Attached
A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic
POPL
A Semantic Account of Metric Preservation
POPL
A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms
POPL
DOI Pre-print
Analyzing divergence in bisimulation semantics
POPL
Automatically Comparing Memory Consistency Models
POPL
Pre-print Media Attached File Attached
Automatically Generating the Dynamic Semantics of Gradually Typed Languages
POPL
Beginner's Luck: A Language for Property-Based Generators
POPL
Pre-print
Big Types in Little Runtime: Open World Soundness and Collaborative Blame for Gradual Type System
POPL
Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
POPL
DOI File Attached
Coming to Terms with Quantified Reasoning
POPL
Complexity Verification Using Guided Theorem Enumeration
POPL
Component-Based Synthesis for Complex APIs
POPL
Computational Higher-Dimensional Type Theory
POPL
Context-sensitive data dependence analysis via Linear Conjunctive Language Reachability
POPL
Contextual isomorphisms
POPL
Contract-based Resource Verification for Higher-order Functions with Memoization
POPL
Coupling proofs are probabilistic product programs
POPL
Deciding equivalence with sums and the empty type
POPL
Dijkstra Monads for Free
POPL
Pre-print
Do be do be do
POPL
Dynamic Race Detection For C++11
POPL
Exact Bayesian Inference by Symbolic Disintegration
POPL
Pre-print
Fast Polyhedra Abstract Domain
POPL
Fencing off Go: Liveness and Safety for Channel-Based Programming
POPL
Pre-print
Genesis: Synthesizing Forwarding Tables in Multi-tenant Networks
POPL
Gradual Refinement Types
POPL
Link to publication DOI Pre-print
Hazelnut: A Bidirectionally Typed Structure Editor Calculus
POPL
Hypercollecting Semantics and its Application to Static Analysis of Information Flow
POPL
Interactive Proofs in Higher-Order Concurrent Separation Logic
POPL
DOI Pre-print Media Attached
Intersection Type Calculi of Bounded Dimension
POPL
Invariants of Quantum Programs: Characterisations and Generation
POPL
Java generics are Turing complete
POPL
LMS-Verify: Abstraction Without Regret for Verified Systems Programming
POPL
LOIS: syntax and semantics
POPL
Learning nominal automata
POPL
LightDP: Towards Automating Differential Privacy Proofs
POPL
Mixed-size Concurrency: ARM, POWER, C/C++11, and SC
POPL
Modules, Abstraction, and Parametric Polymorphism
POPL
Monadic second-order logic on finite sequences
POPL
Ogre and Pythia, An invariance proof method for weak consistency models
POPL
On Verifying Causal Consistency
POPL
On the Relationship Between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic
POPL
Opening
POPL

Parallel Functional Arrays
POPL
Polymorphism, subtyping and type inference in MLsub
POPL
QWIRE: A Core Language for Quantum Circuits
POPL
Relational Cost Analysis
POPL
Rigorous Floating-point Mixed Precision Tuning
POPL
Pre-print
Semantic-Directed Clumping of Disjunctive Abstract States
POPL
Serializability for Eventual Consistency: Criterion, Analysis and Applications
POPL
Pre-print
Stateful Manifest Contracts
POPL
Stochastic Invariants for Probabilistic Termination
POPL
Stream Fusion, to Completeness
POPL
Pre-print Media Attached
Sums of Uncertainty: Refinements go gradual
POPL
The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects
POPL
The exp-log normal form of types: Decomposing extensional equality and representing terms compactly
POPL
Thread Modularity at Many Levels: a Pearl in Compositional Verification
POPL
Towards Automatic Resource Bound Analysis for OCaml
POPL
Type Directed Compilation of Row-Typed Algebraic Effects
POPL
Type Soundness Proofs with Definitional Interpreters
POPL
Type Systems as Macros
POPL
Typed Self-Evaluation via Intensional Type Functions
POPL