## John Field, Michael Hicks

*Proceedings of the 39th Symposium on Principles of Programming Languages*

POPL, 2012.

@proceedings{POPL-2012, acmid = "2103656", address = "Philadelphia, Pennsylvania, USA", editor = "John Field and Michael Hicks", isbn = "978-1-4503-1083-3", publisher = "{ACM}", title = "{Proceedings of the 39th Symposium on Principles of Programming Languages}", year = 2012, }

### Contents (47 items)

- POPL-2012-BlackO #hoare #perspective
- Presentation of the SIGPLAN distinguished achievement award to Sir Charles Antony Richard Hoare, FRS, FREng, FBCS; and interview (APB, PWO), pp. 1–2.
- POPL-2012-StadenCM
- Freefinement (SvS, CC, BM), pp. 7–18.
- POPL-2012-JoshiLL #debugging
- Underspecified harnesses and interleaved bugs (SJ, SKL, AL), pp. 19–30.
- POPL-2012-GardnerMS #javascript #logic #towards
- Towards a program logic for JavaScript (PG, SM, GDS), pp. 31–44.
- POPL-2012-KrishnaswamiBH #bound #functional #higher-order #programming
- Higher-order functional reactive programming in bounded space (NRK, NB, JH), pp. 45–58.
- POPL-2012-HurDNV #bisimulation #logic
- The marriage of bisimulations and Kripke logical relations (CKH, DD, GN, VV), pp. 59–72.
- POPL-2012-JamesS
- Information effects (RPJ, AS), pp. 73–84.
- POPL-2012-YangYS #automation #policy #privacy
- A language for automatically enforcing privacy policies (JY, KY, ASL), pp. 85–96.
- POPL-2012-BartheKOB #difference #privacy #probability #reasoning #relational
- Probabilistic relational reasoning for differential privacy (GB, BK, FO, SZB), pp. 97–110.
- POPL-2012-HeideggerBT #contract #scripting language
- Access permission contracts for scripting languages (PH, AB, PT), pp. 111–122.
- POPL-2012-MadhusudanQS #induction #proving #recursion
- Recursive proofs for inductive tree data-structures (PM, XQ, AS), pp. 123–136.
- POPL-2012-VeanesHLMB #algorithm #finite #transducer
- Symbolic finite state transducers: algorithms and applications (MV, PH, BL, DM, NB), pp. 137–150.
- POPL-2012-KoksalKS #constraints
- Constraints as control (ASK, VK, PS), pp. 151–164.
- POPL-2012-AustinF #data flow #information management #multi
- Multiple facets for dynamic information flow (THA, CF), pp. 165–178.
- POPL-2012-RayL #injection
- Defining code-injection attacks (DR, JL), pp. 179–190.
- POPL-2012-BasuBO
- Deciding choreography realizability (SB, TB, MO), pp. 191–202.
- POPL-2012-BouajjaniE #analysis #parallel #recursion #source code
- Analysis of recursively parallel programs (AB, ME), pp. 203–214.
- POPL-2012-Rexford #network #programmable #programming language
- Programming languages for programmable networks (JR), pp. 215–216.
- POPL-2012-MonsantoFHW #compilation #network #programming language #runtime
- A compiler and run-time system for network programming languages (CM, NF, RH, DW), pp. 217–230.
- POPL-2012-ChughRJ #logic #type system
- Nested refinements: a logic for duck typing (RC, PMR, RJ), pp. 231–244.
- POPL-2012-CousotC #abstract interpretation #framework #termination
- An abstract interpretation framework for termination (PC, RC), pp. 245–258.
- POPL-2012-HoderKV #game studies #proving
- Playing in the grey area of proofs (KH, LK, AV), pp. 259–272.
- POPL-2012-StampoulisS #proving
- Static and user-extensible proof checking (AS, ZS), pp. 273–284.
- POPL-2012-KleinCDEFFMRTF #effectiveness #lightweight #research
- Run your research: on the effectiveness of lightweight mechanization (CK, JC, CD, CE, MF, MF, JAM, JR, STH, RBF), pp. 285–296.
- POPL-2012-FarzanK #composition #concurrent #reasoning #source code #verification
- Verification of parameterized concurrent programs by modular reasoning about data and control (AF, ZK), pp. 297–308.
- POPL-2012-BotincanDJ #abduction
- Resource-sensitive synchronization inference by abduction (MB, MD, SJ), pp. 309–322.
- POPL-2012-ReddyR #logic
- Syntactic control of interference for separation logic (USR, JCR), pp. 323–336.
- POPL-2012-LicataH #2d #type system
- Canonicity for 2-dimensional type theory (DRL, RH), pp. 337–348.
- POPL-2012-KammarP #algebra #optimisation
- Algebraic foundations for effect-dependent optimisations (OK, GDP), pp. 349–360.
- POPL-2012-CretinR #abstraction #on the #power of
- On the power of coercion abstraction (JC, DR), pp. 361–372.
- POPL-2012-NaikYCS #abstraction #testing
- Abstractions from tests (MN, HY, GC, MS), pp. 373–386.
- POPL-2012-SmaragdakisESYF #concurrent #detection #polynomial #predict
- Sound predictive race detection in polynomial time (YS, JE, CS, JY, CF), pp. 387–400.
- POPL-2012-BojanczykBKL #towards
- Towards nominal computation (MB, LB, BK, SL), pp. 401–412.
- POPL-2012-CaveP #data type #programming
- Programming with binders and indexed data-types (AC, BP), pp. 413–424.
- POPL-2012-Moore #proving #theorem proving
- Meta-level features in an industrial-strength theorem prover (JSM), pp. 425–426.
- POPL-2012-ZhaoNMZ #formal method #program transformation #representation
- Formalizing the LLVM intermediate representation for verified program transformations (JZ, SN, MMKM, SZ), pp. 427–440.
- POPL-2012-ZhuMKR #approximate #performance #program transformation #random
- Randomized accuracy-aware program transformations for efficient approximate computations (ZAZ, SM, JAK, MCR), pp. 441–454.
- POPL-2012-LiangFF #concurrent #program transformation #simulation #verification
- A rely-guarantee-based simulation for verifying concurrent program transformations (HL, XF, MF), pp. 455–468.
- POPL-2012-Balabonski #approach #lazy evaluation
- A unified approach to fully lazy sharing (TB), pp. 469–480.
- POPL-2012-RastogiCH #type inference
- The ins and outs of gradual type inference (AR, AC, BH), pp. 481–494.
- POPL-2012-HofmannPW #lens
- Edit lenses (MH, BCP, DW), pp. 495–508.
- POPL-2012-BattyMOSS #c #c++ #compilation #concurrent
- Clarifying and compiling C/C++ concurrency: from C++11 to POWER (MB, KM, SO, SS, PS), pp. 509–520.
- POPL-2012-RamananandroRL #c++ #resource management #semantics
- A mechanized semantics for C++ object construction and destruction, with applications to resource management (TR, GDR, XL), pp. 521–532.
- POPL-2012-EllisonR #c #execution #semantics
- An executable formal semantics of C with applications (CE, GR), pp. 533–544.
- POPL-2012-BhatAVG #probability #type system
- A type theory for probability density functions (SB, AA, RWV, AGG), pp. 545–556.
- POPL-2012-NadenBAB #type system
- A type system for borrowing permissions (KN, RB, JA, KB), pp. 557–570.
- POPL-2012-StrubSFC #coq #named #self
- Self-certification: bootstrapping certified typecheckers in F* with Coq (PYS, NS, CF, JC), pp. 571–584.

4 ×#concurrent

4 ×#logic

4 ×#proving

4 ×#type system

3 ×#program transformation

2 ×#abstraction

2 ×#c

2 ×#c++

2 ×#compilation

2 ×#network

4 ×#logic

4 ×#proving

4 ×#type system

3 ×#program transformation

2 ×#abstraction

2 ×#c

2 ×#c++

2 ×#compilation

2 ×#network