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)

4 ×#concurrent
4 ×#logic
4 ×#proving
4 ×#type system
3 ×#program transformation
2 ×#abstraction
2 ×#c
2 ×#c++
2 ×#compilation
2 ×#network

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.