POPL '15- Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Full Citation in the ACM Digital Library

SESSION: Keynote Address

Automating Repetitive Tasks for the Masses

SESSION: Session 1A: Types I

Functors are Type Refinement Systems

Integrating Linear and Dependent Types

Higher Inductive Types as Homotopy-Initial Algebras

SESSION: Session 1B: Security

Runtime Enforcement of Security Policies on Black Box Reactive Programs

Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy

Differential Privacy: Now it's Getting Personal

SESSION: Session 2A: Program Analysis I

Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks

Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth

Predicting Program Properties from "Big Code"

SESSION: Session 2B: Domain-specific Languages

DReX: A Declarative Language for Efficiently Evaluating Regular String Transformations

Data-Parallel String-Manipulating Programs

Ur/Web: A Simple Model for Programming the Web

SESSION: Session 3A: Dynamic Verification

Safe & Efficient Gradual Typing for TypeScript

Space-Efficient Manifest Contracts

Manifest Contracts for Datatypes

SESSION: Session 3B: Concurrency I

Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it

From Communicating Machines to Graphical Choreographies

A Scalable, Correct Time-Stamped Stack

SESSION: Session 4A: Compiler Correctness

A Formally-Verified C Static Analyzer

Analyzing Program Analyses

Compositional CompCert

SESSION: Session 4B: Types II

Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction

Principal Type Schemes for Gradual Programs

Dependent Information Flow Types

SESSION: Session 5A: Regular Languages and Automata

Abstract Symbolic Automata: Mixed syntactic/semantic similarity analysis of executables

A Coalgebraic Decision Procedure for NetKAT

Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests

SESSION: Session 5B: Programming Models I

Programming up to Congruence

A Meta Lambda Calculus with Cross-Level Computation

Algebraic Effects, Linearity, and Quantum Programming Languages

SESSION: Session 6A: Concurrency II

Proof Spaces for Unbounded Parallelism

Equations, Contractions, and Unique Solutions

Succinct Representation of Concurrent Trace Sets

SESSION: Session 6B: Semantics

K-Java: A Complete Semantics of Java

Towards the Essence of Hygiene

Self-Representation in Girard's System U

SESSION: Keynote Address

Coding by Everyone, Every Day

SESSION: Keynote Address

Databases and Programming: Two Subjects Divided by a Common Language?

SESSION: Session 7A: Probabilistic Programs

Probabilistic Termination: Soundness, Completeness, and Compositionality

Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems

SESSION: Session 7B: Programming Models II

Full Abstraction for Signal Flow Graphs

Conjugate Hylomorphisms -- Or: The Mother of All Structured Recursion Schemes

SESSION: Session 8A: Program Analysis II

Quantitative Interprocedural Analysis

Specification Inference Using Context-Free Language Reachability

On Characterizing the Data Access Complexity of Programs

SESSION: Session 8B: Verification

Sound Modular Verification of C Code Executing in an Unverified Context

Deep Specifications and Certified Abstraction Layers

From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification

SESSION: Session 9A: Concurrency III

A Calculus for Relaxed Memory

Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning

Tractable Refinement Checking for Concurrent Objects

SESSION: Session 9B: Synthesis

Decentralizing SDN Policies

Program Boosting: Program Synthesis via Crowd-Sourcing

Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant



Imprint / Data Protection