POPL 2017
66 papers
- A posteriori environment analysis with Pushdown Delta CFA
- A program optimization for automatic database result caching
- A promising semantics for relaxed-memory concurrency
- A relational model of types-and-effects in higher-order concurrent separation logic
- A semantic account of metric preservation
- A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
- Analyzing divergence in bisimulation semantics
- Automatically comparing memory consistency models
- Automatically generating the dynamic semantics of gradually typed languages
- Beginner's luck: a language for property-based generators
- Big types in little runtime: open-world soundness and collaborative blame for gradual type systems
- Cantor meets scott: semantic foundations for probabilistic networks
- Coming to terms with quantified reasoning
- Complexity verification using guided theorem enumeration
- Component-based synthesis for complex APIs
- Computational higher-dimensional type theory
- Context-sensitive data-dependence analysis via linear conjunctive language reachability
- Contextual isomorphisms
- Contract-based resource verification for higher-order functions with memoization
- Coupling proofs are probabilistic product programs
- Deciding equivalence with sums and the empty type
- Dijkstra monads for free
- Do be do be do
- Dynamic race detection for C++11
- Exact Bayesian inference by symbolic disintegration
- Fast polyhedra abstract domain
- Fencing off go: liveness and safety for channel-based programming
- Genesis: synthesizing forwarding tables in multi-tenant networks
- Gradual refinement types
- Hazelnut: a bidirectionally typed structure editor calculus
- Hypercollecting semantics and its application to static analysis of information flow
- Interactive proofs in higher-order concurrent separation logic
- Intersection type calculi of bounded dimension
- Invariants of quantum programs: characterisations and generation
- Java generics are turing complete
- LMS-Verify: abstraction without regret for verified systems programming
- LOIS: syntax and semantics
- Learning nominal automata
- LightDP: towards automating differential privacy proofs
- Mixed-size concurrency: ARM, POWER, C/C++11, and SC
- Modules, abstraction, and parametric polymorphism
- Monadic second-order logic on finite sequences
- Ogre and Pythia: an invariance proof method for weak consistency models
- On the relationship between higher-order recursion schemes and higher-order fixpoint logic
- On verifying causal consistency
- Parallel functional arrays
- Polymorphism, subtyping, and type inference in MLsub
- QWIRE: a core language for quantum circuits
- Relational cost analysis
- Rigorous floating-point mixed-precision tuning
- Rust: from POPL to practice (keynote)
- Semantic-directed clumping of disjunctive abstract states
- Serializability for eventual consistency: criterion, analysis, and applications
- Stateful manifest contracts
- Stochastic invariants for probabilistic termination
- Stream fusion, to completeness
- Sums of uncertainty: refinements go gradual
- The exp-log normal form of types: decomposing extensional equality and representing terms compactly
- The geometry of parallelism: classical, probabilistic, and quantum effects
- The influence of dependent types (keynote)
- Thread modularity at many levels: a pearl in compositional verification
- Towards automatic resource bound analysis for OCaml
- Type directed compilation of row-typed algebraic effects
- Type soundness proofs with definitional interpreters
- Type systems as macros
- Typed self-evaluation via intensional type functions