POPL 2017- Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

Full Citation in the ACM Digital Library

SESSION: Keynotes

The influence of dependent types (keynote)

Rust: from POPL to practice (keynote)

SESSION: Abstract Interpretation

Ogre and Pythia: an invariance proof method for weak consistency models

A posteriori environment analysis with Pushdown Delta CFA

Semantic-directed clumping of disjunctive abstract states

Fast polyhedra abstract domain

SESSION: Type Systems 1

Polymorphism, subtyping, and type inference in MLsub

Java generics are turing complete

Hazelnut: a bidirectionally typed structure editor calculus

Modules, abstraction, and parametric polymorphism

SESSION: Probabilistic Programming

Beginner's luck: a language for property-based generators

Exact Bayesian inference by symbolic disintegration

Stochastic invariants for probabilistic termination

Coupling proofs are probabilistic product programs

SESSION: Concurrency 1

A promising semantics for relaxed-memory concurrency

Automatically comparing memory consistency models

Interactive proofs in higher-order concurrent separation logic

A relational model of types-and-effects in higher-order concurrent separation logic

SESSION: Logic

Monadic second-order logic on finite sequences

On the relationship between higher-order recursion schemes and higher-order fixpoint logic

Coming to terms with quantified reasoning

SESSION: Compiler Optimisation

A program optimization for automatic database result caching

Stream fusion, to completeness

Rigorous floating-point mixed-precision tuning

SESSION: Program Analysis

Relational cost analysis

Contract-based resource verification for higher-order functions with memoization

Context-sensitive data-dependence analysis via linear conjunctive language reachability

Towards automatic resource bound analysis for OCaml

SESSION: Type Systems 2

Deciding equivalence with sums and the empty type

The exp-log normal form of types: decomposing extensional equality and representing terms compactly

Contextual isomorphisms

Typed self-evaluation via intensional type functions

SESSION: Concurrency 2

Mixed-size concurrency: ARM, POWER, C/C++11, and SC

Dynamic race detection for C++11

Serializability for eventual consistency: criterion, analysis, and applications

Thread modularity at many levels: a pearl in compositional verification

SESSION: Functional Programming with Effects

Type directed compilation of row-typed algebraic effects

Do be do be do

Dijkstra monads for free

Stateful manifest contracts

SESSION: Semantic Foundations

A semantic account of metric preservation

Cantor meets scott: semantic foundations for probabilistic networks

SESSION: Logic and Programming

Genesis: synthesizing forwarding tables in multi-tenant networks

LOIS: syntax and semantics

SESSION: Verification and Synthesis

Component-based synthesis for complex APIs

Learning nominal automata

On verifying causal consistency

Complexity verification using guided theorem enumeration

SESSION: Type Systems 3

Intersection type calculi of bounded dimension

Type soundness proofs with definitional interpreters

Computational higher-dimensional type theory

Type systems as macros

SESSION: Concurrency 3

Parallel functional arrays

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

Analyzing divergence in bisimulation semantics

Fencing off go: liveness and safety for channel-based programming

SESSION: Gradual Typing and Contracts

Big types in little runtime: open-world soundness and collaborative blame for gradual type systems

Gradual refinement types

Automatically generating the dynamic semantics of gradually typed languages

Sums of uncertainty: refinements go gradual

SESSION: Quantum

Invariants of quantum programs: characterisations and generation

The geometry of parallelism: classical, probabilistic, and quantum effects

QWIRE: a core language for quantum circuits

SESSION: Security and Privacy

LMS-Verify: abstraction without regret for verified systems programming

Hypercollecting semantics and its application to static analysis of information flow

LightDP: towards automating differential privacy proofs