Proceedings of the 38th Symposium on Principles of Programming Languages
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter

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

PLT
DBLP
Scholar
Full names Links ISxN
@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)

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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.