POPL '14- Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Full Citation in the ACM Digital Library

SESSION: Milner award

Modular reasoning about concurrent higher-order imperative programs

SESSION: SIGPLAN achievement award

A galois connection calculus for abstract interpretation

SESSION: Type system design

Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation

Backpack: retrofitting Haskell with interfaces

Combining proofs and programs in a dependently typed language

SESSION: Program analysis 1

Tracing compilation by abstract interpretation

A type-directed abstraction refinement approach to higher-order model checking

Fissile type analysis: modular checking of almost everywhere invariants

SESSION: Semantics of systems

A trusted mechanised JavaScript specification

An operational and axiomatic semantics for non-determinism and sequence points in C

NetKAT: semantic foundations for networks

SESSION: Program analysis 2

Bias-variance tradeoffs in program analysis

Abstract satisfaction

Proofs that count

SESSION: Verified systems

A verified information-flow architecture

CakeML: a verified implementation of ML

Probabilistic relational verification for cryptographic implementations

SESSION: Synthesis

Bridging boolean and quantitative synthesis using smoothed proof search

A constraint-based approach to solving games on infinite graphs

Sound compilation of reals

SESSION: SIGPLAN software systems award

30 years of research and development around Coq

SESSION: In memory of John Reynolds

The essence of Reynolds

SESSION: Concurrent programming models

Freeze after writing: quasi-deterministic parallel programming with LVars

Replicated data types: specification, verification, optimality

Verifying eventual consistency of optimistic replication systems

SESSION: Probability

On coinductive equivalences for higher-order probabilistic functional programs

Probabilistic coherence spaces are fully abstract for probabilistic PCF

Tabular: a schema-driven probabilistic programming language

SESSION: Functional programming 1

Modular, higher-order cardinality analysis in theory and practice

Profiling for laziness

Fair reactive programming

SESSION: Reasoning

Optimal dynamic partial order reduction

Modular reasoning about heap paths via effectively propositional formulas

A sound and complete abstraction for reasoning about parallel prefix sums

SESSION: Security

Authenticated data structures, generically

Gradual typing embedded securely in JavaScript

Sound input filter generation for integer overflow errors

SESSION: Separation logic

Parametric completeness for separation theories

Proof search for propositional abstract separation logics via labelled sequents

A proof system for separation logic with magic wand

SESSION: Semantic models 1

From parametricity to conservation laws, via Noether's theorem

A relationally parametric model of dependent type theory

Game semantics for interface middleweight Java

SESSION: Program analysis 3

Abstract acceleration of general linear loops

Minimization of symbolic automata

Consistency analysis of decision-making programs

SESSION: Static errors

Toward general diagnosis of static errors

Counter-factual typing for debugging type errors

SESSION: Model checking and SMT

Battery transition systems

Symbolic optimization with SMT solvers

SESSION: Semantic models 2

Abstract effects and proof-relevant logical relations

Parametric effect monads and semantics of effect systems

Applying quantitative semantics to higher-order quantum computing

SESSION: Functional programming 2

A nonstandard standardization theorem

Closed type families with overlapping equations



Imprint / Data Protection