Sriram K. Rajamani, David Walker
Proceedings of the 42nd Symposium on Principles of Programming Languages
POPL, 2015.

@proceedings{POPL-2015,
	acmid         = "2676726",
	address       = "Mumbai, India",
	editor        = "Sriram K. Rajamani and David Walker",
	isbn          = "978-1-4503-3300-9",
	publisher     = "{ACM}",
	title         = "{Proceedings of the 42nd Symposium on Principles of Programming Languages}",
	year          = 2015,
}

Contents (55 items)

5 ×#algebra
5 ×#composition
5 ×#named
4 ×#analysis
4 ×#concurrent
4 ×#source code
3 ×#programming
3 ×#refinement
2 ×#abstraction
2 ×#algorithm

POPL-2015-Gulwani #automation

Automating Repetitive Tasks for the Masses (SG), pp. 1–2.

POPL-2015-MelliesZ #refinement

Functors are Type Refinement Systems (PAM, NZ), pp. 3–16.

POPL-2015-KrishnaswamiPB #dependent type #linear

Integrating Linear and Dependent Types (NRK, PP, NB), pp. 17–30.

POPL-2015-Sojakova #algebra #induction

Higher Inductive Types as Homotopy-Initial Algebras (KS), pp. 31–42.

POPL-2015-NgoMMP #black box #policy #runtime #security #source code

Runtime Enforcement of Security Policies on Black Box Reactive Programs (MN, FM, DM, FP), pp. 43–54.

POPL-2015-BartheGAHRS #approximate #design #difference #higher-order #privacy #refinement #relational

Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy (GB, MG, EJGA, JH, AR, PYS), pp. 55–68.

POPL-2015-EbadiSS #difference #privacy

Differential Privacy: Now it’s Getting Personal (HE, DS, GS), pp. 69–81.

POPL-2015-TangWZXZM #analysis #data flow

Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks (HT, XW, LZ, BX, LZ, HM), pp. 83–95.

POPL-2015-ChatterjeeIPG #algebra #algorithm #constant #performance #recursion #state machine

Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth (KC, RIJ, AP, PG), pp. 97–109.

POPL-2015-RaychevVK #predict

Predicting Program Properties from “Big Code” (VR, MTV, AK), pp. 111–124.

POPL-2015-AlurDR #declarative #named #string

DReX: A Declarative Language for Efficiently Evaluating Regular String Transformations (RA, LD, MR), pp. 125–137.

POPL-2015-VeanesMML #source code #string

Data-Parallel String-Manipulating Programs (MV, TM, DM, BL), pp. 139–152.

POPL-2015-Chlipala #named #programming #web

Ur/Web: A Simple Model for Programming the Web (AC), pp. 153–165.

POPL-2015-RastogiSFBV #performance #type system #typescript

Safe & Efficient Gradual Typing for TypeScript (AR, NS, CF, GMB, PV), pp. 167–180.

POPL-2015-Greenberg #contract

Space-Efficient Manifest Contracts (MG), pp. 181–194.

POPL-2015-SekiyamaNI #contract #data type

Manifest Contracts for Datatypes (TS, YN, AI), pp. 195–207.

POPL-2015-VafeiadisBCMN #compilation #memory management #optimisation #what

Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it (VV, TB, SC, RM, FZN), pp. 209–220.

POPL-2015-LangeTY #communication #visual notation

From Communicating Machines to Graphical Choreographies (JL, ET, NY), pp. 221–232.

POPL-2015-DoddsHK #scalability #stack

A Scalable, Correct Time-Stamped Stack (MD, AH, CMK), pp. 233–246.

POPL-2015-JourdanLBLP #c

A Formally-Verified C Static Analyzer (JHJ, VL, SB, XL, DP), pp. 247–259.

POPL-2015-GiacobazziLR #analysis #metaprogramming

Analyzing Program Analyses (RG, FL, FR), pp. 261–273.

POPL-2015-StewartBCA #composition

Compositional CompCert (GS, LB, SC, AWA), pp. 275–287.

POPL-2015-Castagna0XA #polymorphism #re-engineering #type inference

Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction (GC, KN, ZX, PA), pp. 289–302.

POPL-2015-GarciaC #source code

Principal Type Schemes for Gradual Programs (RG, MC), pp. 303–315.

POPL-2015-LourencoC #data flow

Dependent Information Flow Types (LL, LC), pp. 317–328.

POPL-2015-PredaGLM #analysis #automaton #bytecode #semantics #similarity

Abstract Symbolic Automata: Mixed syntactic/semantic similarity analysis of executables (MDP, RG, AL, IM), pp. 329–341.

POPL-2015-FosterKM0T #algebra

A Coalgebraic Decision Procedure for NetKAT (NF, DK, MM, AS, LT), pp. 343–355.

POPL-2015-Pous #algebra #algorithm #equivalence #testing

Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests (DP), pp. 357–368.

POPL-2015-SjobergW #congruence #programming

Programming up to Congruence (VS, SW), pp. 369–382.

POPL-2015-Tobisawa #λ-calculus

A Meta λ Calculus with Cross-Level Computation (KT), pp. 383–393.

POPL-2015-Staton #algebra #programming language #quantum

Algebraic Effects, Linearity, and Quantum Programming Languages (SS), pp. 395–406.

POPL-2015-FarzanKP #bound #parallel #proving

Proof Spaces for Unbounded Parallelism (AF, ZK, AP), pp. 407–420.

POPL-2015-Sangiorgi #equation

Equations, Contractions, and Unique Solutions (DS), pp. 421–432.

POPL-2015-GuptaHRST #concurrent #representation #set

Succinct Representation of Concurrent Trace Sets (AG, TAH, AR, RS, TT), pp. 433–444.

POPL-2015-BogdanasR #java #named #semantics

K-Java: A Complete Semantics of Java (DB, GR), pp. 445–456.

POPL-2015-Adams #towards

Towards the Essence of Hygiene (MDA), pp. 457–469.

POPL-2015-BrownP #self

Self-Representation in Girard’s System U (MB, JP), pp. 471–484.

POPL-2015-Lee

Coding by Everyone, Every Day (PL), p. 485.

POPL-2015-Buneman #database #programming #question

Databases and Programming: Two Subjects Divided by a Common Language? (PB), p. 487.

POPL-2015-FioritiH #composition #probability #termination

Probabilistic Termination: Soundness, Completeness, and Compositionality (LMFF, HH), pp. 489–501.

POPL-2015-HeGWZ #automaton #composition #concurrent #probability #reasoning

Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems (FH, XG, BYW, LZ), pp. 503–514.

POPL-2015-BonchiSZ #abstraction #graph

Full Abstraction for Signal Flow Graphs (FB, PS, FZ), pp. 515–526.

POPL-2015-HinzeWG #morphism #recursion

Conjugate Hylomorphisms — Or: The Mother of All Structured Recursion Schemes (RH, NW, JG), pp. 527–538.

POPL-2015-ChatterjeePV #analysis #interprocedural

Quantitative Interprocedural Analysis (KC, AP, YV), pp. 539–551.

POPL-2015-BastaniAA #context-free grammar #reachability #specification #using

Specification Inference Using Context-Free Language Reachability (OB, SA, AA), pp. 553–566.

POPL-2015-ElangoRPRS #complexity #data access #on the #source code

On Characterizing the Data Access Complexity of Programs (VE, FR, LNP, JR, PS), pp. 567–580.

POPL-2015-Agten0P #c #composition #verification

Sound Modular Verification of C Code Executing in an Unverified Context (PA, BJ, FP), pp. 581–594.

POPL-2015-GuKRSWWZG #abstraction #specification

Deep Specifications and Certified Abstraction Layers (RG, JK, TR, ZS, X(W, SCW, HZ, YG), pp. 595–608.

POPL-2015-Chlipala15a #case study #composition #interface #network #parallel #thread #verification #web

From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification (AC), pp. 609–622.

POPL-2015-CraryS #calculus #memory management

A Calculus for Relaxed Memory (KC, MJS), pp. 623–636.

POPL-2015-JungSSSTBD #concurrent #invariant #monad #named #orthogonal #reasoning

Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning (RJ, DS, FS, KS, AT, LB, DD), pp. 637–650.

POPL-2015-BouajjaniEEH #concurrent #refinement

Tractable Refinement Checking for Concurrent Objects (AB, ME, CE, JH), pp. 651–662.

POPL-2015-PadonIKLSS #policy

Decentralizing SDN Policies (OP, NI, AK, OL, MS, SS), pp. 663–676.

POPL-2015-CochranDLMV #synthesis

Program Boosting: Program Synthesis via Crowd-Sourcing (RAC, LD, BL, DM, MV), pp. 677–688.

POPL-2015-DelawarePGC #data type #deduction #named #proving #synthesis

Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant (BD, CPC, JG, AC), pp. 689–700.