POPL '16- Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Full Citation in the ACM Digital Library

SESSION: Keynotes

Programming the world of uncertain things (keynote)

Synthesis of reactive controllers for hybrid systems (keynote)

Confluences in programming languages research (keynote)

SESSION: Types and Foundations

Breaking through the normalization barrier: a self-interpreter for f-omega

Type theory in type theory using quotient inductive types

System f-omega with equirecursive types for datatype-generic programming

A theory of effects and resources: adjunction models and polarised calculi

SESSION: Algorithmic Verification

Temporal verification of higher-order functional programs

Scaling network verification using symmetry and surgery

Model checking for symbolic-heap separation logic with inductive predicates

Reducing crash recoverability to reachability

SESSION: Decision Procedures

Query-guided maximum satisfiability

String solving with word equations and transducers: towards a logic for analysing mutation XSS

Symbolic computation of differential equivalences

Unboundedness and downward closures of higher-order pushdown automata

SESSION: Correct Compilation

Fully-abstract compilation by approximate back-translation

Lightweight verification of separate compilation

From MinX to MinC: semantics-driven decompilation of recursive datatypes

Sound type-dependent syntactic language extension

SESSION: Decidability and Complexity

Decidability of inferring inductive invariants

The hardness of data packing

The complexity of interaction

SESSION: Language Design

Dependent types and multi-monadic effects in F*

Fabular: regression formulas as probabilistic programming

Kleenex: compiling nondeterministic transducers to deterministic streaming transducers

SESSION: Probabilistic and Statistical Analysis

Automatic patch generation by learning correct code

Estimating types in binaries using predictive modeling

Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs

Transforming spreadsheet data types using examples

SESSION: Foundations of Distributed Systems

Chapar: certified causally consistent distributed key-value stores

'Cause I'm strong enough: Reasoning about consistency choices in distributed systems

A program logic for concurrent objects under fair scheduling

PSync: a partially synchronous language for fault-tolerant distributed algorithms

SESSION: Types, Generally or Gradually

Principal type inference for GADTs

Abstracting gradual typing

The gradualizer: a methodology and algorithm for generating gradual type systems

Is sound gradual typing dead?

SESSION: Learning and Verification

Combining static analysis with probabilistic models to enable market-scale Android inter-component analysis

Abstraction refinement guided by a learnt probabilistic model

Learning invariants using decision trees and implication counterexamples

Symbolic abstract data type inference

SESSION: Optimization

SMO: an integrated approach to intra-array and inter-array storage optimization

PolyCheck: dynamic verification of iteration space transformations on affine programs

Printing floating-point numbers: a faster, always correct method

SESSION: Sessions and Processes

Effects as sessions, sessions as effects

Monitors and blame assignment for higher-order session types

Environmental bisimulations for probabilistic higher-order languages

SESSION: Semantics and Memory Models

Modelling the ARMv8 architecture, operationally: concurrency and ISA

A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions

Overhauling SC atomics in C11 and OpenCL

Taming release-acquire consistency

SESSION: Program Design and Analysis

Newtonian program analysis via tensor product

Casper: an efficient approach to call trace collection

Pushdown control-flow analysis for free

Binding as sets of scopes

SESSION: Foundations of Model Checking

Lattice-theoretic progress measures and coalgebraic model checking

Algorithms for algebraic path properties in concurrent systems of constant treewidth components

Memoryful geometry of Interaction II: recursion and adequacy

SESSION: Synthesis

Learning programs from noisy data

Optimizing synthesis with metasketches

Maximal specification synthesis

Example-directed synthesis: a type-theoretic interpretation