Zhong Shao, Benjamin C. Pierce
Proceedings of the 36th Symposium on Principles of Programming Languages
POPL, 2009.

@proceedings{POPL-2009,
	acmid         = "1480881",
	address       = "Savannah, Georgia, USA",
	editor        = "Zhong Shao and Benjamin C. Pierce",
	isbn          = "978-1-60558-379-2",
	publisher     = "{ACM}",
	title         = "{Proceedings of the 36th Symposium on Principles of Programming Languages}",
	year          = 2009,
}

Contents (39 items)

4 ×#verification
3 ×#approach
3 ×#composition
3 ×#memory management
3 ×#semantics
2 ×#analysis
2 ×#automation
2 ×#higher-order
2 ×#linear
2 ×#logic

POPL-2009-Harris #memory management #transaction

Language constructs for transactional memory (TH), p. 1.

POPL-2009-ElmasQT #calculus

A calculus of atomic actions (TE, SQ, ST), pp. 2–15.

POPL-2009-GotsmanCPV #algorithm #proving

Proving that non-blocking algorithms don’t block (AG, BC, MJP, VV), pp. 16–28.

POPL-2009-AbadiP #thread

A model of cooperative threads (MA, GDP), pp. 29–40.

POPL-2009-XuJC #contract #haskell

Static contract checking for Haskell (DNX, SLPJ, KC), pp. 41–52.

POPL-2009-QiM

Masked types for sound object initialization (XQ, ACM), pp. 53–65.

POPL-2009-Leijen #flexibility #morphism #polymorphism #robust #type inference

Flexible types: robust type inference for first-class polymorphism (DL), pp. 66–77.

POPL-2009-LublinermanST #code generation #composition #diagrams

Modular code generation from synchronous block diagrams: modularity vs. code size (RL, CS, ST), pp. 78–89.

POPL-2009-BartheGB #certification #encryption #proving

Formal certification of code-based cryptographic proofs (GB, BG, SZB), pp. 90–101.

POPL-2009-GantyMR #liveness #source code #verification

Verifying liveness for asynchronous programs (PG, RM, AR), pp. 102–113.

POPL-2009-BrunelDHLM #logic #model checking #using

A foundation for flow-based program matching: using temporal logic and model checking (JB, DD, RRH, JLL, GM), pp. 114–126.

POPL-2009-GulwaniMC #complexity #estimation #named #performance #precise

SPEED: precise and efficient static estimation of program computational complexity (SG, KKM, TMC), pp. 127–139.

POPL-2009-Monniaux #abstraction #automation #composition #constraints #linear

Automatic modular abstractions for linear constraints (DM), pp. 140–151.

POPL-2009-Barker

Wild control operators (CB), p. 152.

POPL-2009-GarciaLS #evaluation #lazy evaluation

Lazy evaluation and delimited control (RG, AL, AS), pp. 153–164.

POPL-2009-Voigtlander #bidirectional #exclamation #for free

Bidirectionalization for free! (Pearl) (JV), pp. 165–176.

POPL-2009-MorihataMHT #divide and conquer #morphism #theorem

The third homomorphism theorem on trees: downward & upward lead to divide-and-conquer (AM, KM, ZH, MT), pp. 177–185.

POPL-2009-Ley-WildAF #self #semantics

A cost semantics for self-adjusting computation (RLW, UAA, MF), pp. 186–199.

POPL-2009-TozawaTOM #php

Copy-on-write in the PHP language (AT, MT, TO, YM), pp. 200–212.

POPL-2009-BronsonKO #optimisation

Feedback-directed barrier optimization in a strongly isolated STM (NGB, CK, KO), pp. 213–225.

POPL-2009-HardekopfL #analysis #pointer

Semi-sparse flow-sensitive pointer analysis (BH, CL), pp. 226–238.

POPL-2009-GulwaniLS #framework

A combination framework for tracking partition sizes (SG, TLA, MS), pp. 239–251.

POPL-2009-WangLKKM #concurrent #formal method

The theory of deadlock avoidance via discrete control (YW, SL, TK, MK, SAM), pp. 252–263.

POPL-2009-TateSTL #approach #optimisation #similarity

Equality saturation: a new approach to optimization (RT, MS, ZT, SL), pp. 264–276.

POPL-2009-JonssonN #call-by #higher-order #supercompilation

Positive supercompilation for a higher order call-by-value language (PAJ, JN), pp. 277–288.

POPL-2009-CalcagnoDOY #analysis #composition

Compositional shape analysis by means of bi-abduction (CC, DD, PWO, HY), pp. 289–300.

POPL-2009-Simpson #linear

Linear types for computational effects (AS), p. 301.

POPL-2009-ConditHLQ #low level #type checking

Unifying type checking and property checking for low-level code (JC, BH, SKL, SQ), pp. 302–314.

POPL-2009-Feng #reasoning

Local rely-guarantee reasoning (XF), pp. 315–327.

POPL-2009-BrotherstonC #logic #reasoning

Classical BI: a logic for reasoning about dualising resources (JB, CC), pp. 328–339.

POPL-2009-AhmedDR #independence #representation

State-dependent representation independence (AA, DD, AR), pp. 340–353.

POPL-2009-MontaguR #data type #modelling

Modeling abstract types in modules with open existential types (BM, DR), pp. 354–365.

POPL-2009-Krishnaswami #pattern matching

Focusing on pattern matching (NRK), pp. 366–378.

POPL-2009-SarkarSNORBMA #multi #semantics

The semantics of x86-CC multiprocessor machine code (SS, PS, FZN, SO, TR, TB, MOM, JA), pp. 379–391.

POPL-2009-BoudolP #approach #memory management #modelling

Relaxed memory models: an operational approach (GB, GP), pp. 392–403.

POPL-2009-GuerraouiK #memory management #semantics #transaction

The semantics of progress in lock-based transactional memory (RG, MK), pp. 404–415.

POPL-2009-Kobayashi #higher-order #recursion #source code #verification

Types and higher-order recursion schemes for verification of higher-order programs (NK), pp. 416–428.

POPL-2009-Ridge #approach #distributed #verification

Verifying distributed systems: the operational approach (TR), pp. 429–440.

POPL-2009-HawblitzelP #automation #garbage collection #verification

Automated verification of practical garbage collectors (CH, EP), pp. 441–453.