Thomas Ball, Mooly Sagiv
Proceedings of the 38th Symposium on Principles of Programming Languages
POPL, 2011.

@proceedings{POPL-2011,
	acmid         = "1926385",
	address       = "Austin, Texas, USA",
	editor        = "Thomas Ball and Mooly Sagiv",
	isbn          = "978-1-4503-0490-0",
	publisher     = "{ACM}",
	title         = "{Proceedings of the 38th Symposium on Principles of Programming Languages}",
	year          = 2011,
}

Contents (52 items)

8 ×#source code
7 ×#concurrent
6 ×#verification
5 ×#abstraction
5 ×#analysis
5 ×#multi
5 ×#parallel
3 ×#automation
3 ×#compilation
3 ×#composition

POPL-2011-Leroy #question #tool support

Verified squared: does critical software deserve verified tools? (XL), pp. 1–2.

POPL-2011-LhotakC #analysis #performance #points-to

Points-to analysis with efficient strong updates (OL, KCAC), pp. 3–16.

POPL-2011-SmaragdakisBL #comprehension

Pick your contexts well: understanding object-sensitivity (YS, MB, OL), pp. 17–30.

POPL-2011-LiangTN #abstraction #learning

Learning minimal abstractions (PL, OT, MN), pp. 31–42.

POPL-2011-SevcikVNJS #compilation #concurrent

Relaxed-memory concurrency and verified compilation (JS, VV, FZN, SJ, PS), pp. 43–54.

POPL-2011-BattyOSSW #c++ #concurrent

Mathematizing C++ concurrency (MB, SO, SS, PS, TW), pp. 55–66.

POPL-2011-RamananandroRL #c++ #inheritance #layout #multi #verification

Formal verification of object layout for c++ multiple inheritance (TR, GDR, XL), pp. 67–80.

POPL-2011-ChoiAYT #multi #source code #static analysis

Static analysis of multi-staged programs via unstaging translation (WC, BA, KY, MT), pp. 81–92.

POPL-2011-SchwarzSVLM #protocol #source code #static analysis

Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol (MDS, HS, VV, PL, MMO), pp. 93–104.

POPL-2011-CousotCL #analysis #array #automation #parametricity #scalability #segmentation

A parametric segmentation functor for fully automatic and scalable array content analysis (PC, RC, FL), pp. 105–118.

POPL-2011-BirkedalRSSTY #modelling #recursion

Step-indexed kripke models over recursive worlds (LB, BR, JS, KS, JT, HY), pp. 119–132.

POPL-2011-HurD #assembly #logic #ml

A kripke logical relation between ML and assembly (CKH, DD), pp. 133–146.

POPL-2011-Pottier

A typed store-passing translation for general references (FP), pp. 147–158.

POPL-2011-PrountzosMPM #analysis #graph #optimisation #parallel #source code

A shape analysis for optimizing parallel graph programs (DP, RM, KP, KSM), pp. 159–172.

POPL-2011-RivalC #abstraction

Calling context abstraction with shapes (XR, BYEC), pp. 173–186.

POPL-2011-DilligDA #precise #reasoning #source code #using

Precise reasoning for programs using containers (ID, TD, AA), pp. 187–200.

POPL-2011-AhmedFSW

Blame for all (AA, RBF, JGS, PW), pp. 201–214.

POPL-2011-DimoulasFFF #contract

Correct blame for contracts: no more scapegoating (CD, RBF, CF, MF), pp. 215–226.

POPL-2011-WeirichVJZ #abstraction #generative

Generative type abstraction and type-level computation (SW, DV, SLPJ, SZ), pp. 227–240.

POPL-2011-MacLaurin #design #programming language #visual notation

The design of kodu: a tiny visual programming language for children on the Xbox 360 (MM), pp. 241–246.

POPL-2011-TuronW #concurrent #logic

A separation logic for refining concurrent objects (AJT, MW), pp. 247–258.

POPL-2011-DoddsJP #composition #parallel #reasoning

Modular reasoning for deterministic parallelism (MD, SJ, MJP), pp. 259–270.

POPL-2011-JacobsP #composition #concurrent #fine-grained #specification

Expressive modular fine-grained concurrency specification (BJ, FP), pp. 271–282.

POPL-2011-MadhusudanP

The tree width of auxiliary storage (PM, GP), pp. 283–294.

POPL-2011-Tzevelekos #automaton

Fresh-register automata (NT), pp. 295–306.

POPL-2011-Leroux #problem #proving #reachability #self

Vector addition system reachability problem: a short self-contained proof (JL), pp. 307–316.

POPL-2011-Gulwani #automation #spreadsheet #string #using

Automating string processing in spreadsheets using input-output examples (SG), pp. 317–330.

POPL-2011-GuptaPR #abstraction #concurrent #multi #refinement #source code #thread #verification

Predicate abstraction and refinement for verifying multi-threaded programs (AG, CP, AR), pp. 331–344.

POPL-2011-GhicaS #geometry #resource management #synthesis #type inference

Geometry of synthesis III: resource management through type inference (DRG, AS), pp. 345–356.

POPL-2011-HoffmannAH #analysis #multi

Multivariate amortized resource analysis (JH, KA, MH), pp. 357–370.

POPL-2011-HofmannPW #lens #symmetry

Symmetric lenses (MH, BCP, DW), pp. 371–384.

POPL-2011-HengleinN #axiom #induction #regular expression

Regular expression containment: coinductive axiomatization and computational interpretation (FH, LN), pp. 385–398.

POPL-2011-CookK

Making prophecies with decision predicates (BC, EK), pp. 399–410.

POPL-2011-EmmiQR #bound #scheduling

Delay-bounded scheduling (ME, SQ, ZR), pp. 411–422.

POPL-2011-SinhaW #abstraction #on the

On interference abstractions (NS, CW), pp. 423–434.

POPL-2011-DenielouY #multi

Dynamic multirole session types (PMD, NY), pp. 435–446.

POPL-2011-TovP

Practical affine types (JAT, RP), pp. 447–458.

POPL-2011-AnCFH #ruby #static typing

Dynamic inference of static types for ruby (Jh(A, AC, JSF, MH), pp. 459–472.

POPL-2011-GordonHHJS #concurrent #verification

Robin Milner 1934--2010: verification, languages, and concurrency (ADG, RH, JH, AJ, PS), pp. 473–474.

POPL-2011-BenderskyP #bound #memory management

Space overhead bounds for dynamic memory management with partial compaction (AB, EP), pp. 475–486.

POPL-2011-AttiyaGHKMV #algorithm #concurrent #order

Laws of order: expensive synchronization in concurrent algorithms cannot be eliminated (HA, RG, DH, PK, MMM, MTV), pp. 487–498.

POPL-2011-EsparzaG #complexity #parallel #source code #thread #verification

Complexity of pattern-based verification for multithreaded programs (JE, PG), pp. 499–510.

POPL-2011-PrabhuRMH #analysis #named

EigenCFA: accelerating flow analysis with GPUs (TP, SR, MM, MWH), pp. 511–522.

POPL-2011-FengDY #bisimulation #process #quantum

Bisimulation for quantum processes (YF, RD, MY), pp. 523–534.

POPL-2011-BocchinoHHAAWS #nondeterminism #parallel

Safe nondeterminism in a deterministic-by-default parallel language (RLBJ, SH, NH, SVA, VSA, AW, TS), pp. 535–548.

POPL-2011-PouchetBBCRSV #optimisation

Loop transformations: convexity, pruning and optimization (LNP, UB, CB, AC, JR, PS, NV), pp. 549–562.

POPL-2011-GuoP #compilation

The essence of compiling with traces (SyG, JP), pp. 563–574.

POPL-2011-RamseyD #composition #dependent type #independence #low level #type system #using

Resourceable, retargetable, modular instruction selection using a machine-independent, type-based tiling of low-level intermediate code (NR, JD), pp. 575–586.

POPL-2011-OngR #algebra #data type #functional #higher-order #pattern matching #source code #verification

Verifying higher-order functional programs with pattern-matching algebraic data types (CHLO, SJR), pp. 587–598.

POPL-2011-AlurC #algorithm #source code #streaming #transducer #verification

Streaming transducers for algorithmic verification of single-pass list-processing programs (RA, PC), pp. 599–610.

POPL-2011-MadhusudanPQ #decidability #logic

Decidable logics combining heap structures and data (PM, GP, XQ), pp. 611–622.

POPL-2011-JoishaSBBC #automation #compilation #effectiveness #optimisation #parallel #reuse #thread #using

A technique for the effective and automatic reuse of classical compiler optimizations on multithreaded code (PGJ, RSS, PB, HJB, DRC), pp. 623–636.