POPL 2016
62 papers
- 'Cause I'm strong enough: reasoning about consistency choices in distributed systems
- A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
- A program logic for concurrent objects under fair scheduling
- A theory of effects and resources: adjunction models and polarised calculi
- Abstracting gradual typing
- Abstraction refinement guided by a learnt probabilistic model
- Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs
- Algorithms for algebraic path properties in concurrent systems of constant treewidth components
- Automatic patch generation by learning correct code
- Binding as sets of scopes
- Breaking through the normalization barrier: a self-interpreter for f-omega
- Casper: an efficient approach to call trace collection
- Chapar: certified causally consistent distributed key-value stores
- Combining static analysis with probabilistic models to enable market-scale Android inter-component analysis
- Confluences in programming languages research (keynote)
- Decidability of inferring inductive invariants
- Dependent types and multi-monadic effects in F
- Effects as sessions, sessions as effects
- Environmental bisimulations for probabilistic higher-order languages
- Estimating types in binaries using predictive modeling
- Example-directed synthesis: a type-theoretic interpretation
- Fabular: regression formulas as probabilistic programming
- From MinX to MinC: semantics-driven decompilation of recursive datatypes
- Fully-abstract compilation by approximate back-translation
- Is sound gradual typing dead?
- Kleenex: compiling nondeterministic transducers to deterministic streaming transducers
- Lattice-theoretic progress measures and coalgebraic model checking
- Learning invariants using decision trees and implication counterexamples
- Learning programs from noisy data
- Lightweight verification of separate compilation
- Maximal specification synthesis
- Memoryful geometry of interaction II: recursion and adequacy
- Model checking for symbolic-heap separation logic with inductive predicates
- Modelling the ARMv8 architecture, operationally: concurrency and ISA
- Monitors and blame assignment for higher-order session types
- Newtonian program analysis via tensor product
- Optimizing synthesis with metasketches
- Overhauling SC atomics in C11 and OpenCL
- PSync: a partially synchronous language for fault-tolerant distributed algorithms
- PolyCheck: dynamic verification of iteration space transformations on affine programs
- Principal type inference for GADTs
- Printing floating-point numbers: a faster, always correct method
- Programming the world of uncertain things (keynote)
- Pushdown control-flow analysis for free
- Query-guided maximum satisfiability
- Reducing crash recoverability to reachability
- SMO: an integrated approach to intra-array and inter-array storage optimization
- Scaling network verification using symmetry and surgery
- Sound type-dependent syntactic language extension
- String solving with word equations and transducers: towards a logic for analysing mutation XSS
- Symbolic abstract data type inference
- Symbolic computation of differential equivalences
- Synthesis of reactive controllers for hybrid systems (keynote)
- System f-omega with equirecursive types for datatype-generic programming
- Taming release-acquire consistency
- Temporal verification of higher-order functional programs
- The complexity of interaction
- The gradualizer: a methodology and algorithm for generating gradual type systems
- The hardness of data packing
- Transforming spreadsheet data types using examples
- Type theory in type theory using quotient inductive types
- Unboundedness and downward closures of higher-order pushdown automata