George C. Necula, Philip Wadler
Proceedings of the 35th Symposium on Principles of Programming Languages
POPL, 2008.

@proceedings{POPL-2008,
	acmid         = "1328438",
	address       = "San Francisco, California, USA",
	editor        = "George C. Necula and Philip Wadler",
	isbn          = "978-1-59593-689-9",
	publisher     = "{ACM}",
	title         = "{Proceedings of the 35th Symposium on Principles of Programming Languages}",
	year          = 2008,
}

Contents (38 items)

5 ×#logic
3 ×#analysis
3 ×#automation
3 ×#data type
3 ×#programming
3 ×#verification
2 ×#concurrent
2 ×#encryption
2 ×#formal method
2 ×#generative

POPL-2008-Fontana #biology #concurrent #modelling

Systems biology, models, and concurrency (WF), pp. 1–2.

POPL-2008-AydemirCPPW

Engineering formal metatheory (BEA, AC, BCP, RP, SW), pp. 3–15.

POPL-2008-TristanL #case study #optimisation #scheduling #validation #verification

Formal verification of translation validators: a case study on instruction scheduling optimizations (JBT, XL), pp. 17–27.

POPL-2008-Voigtlander #parallel

Much ado about two (pearl): a pearl on parallel prefix computation (JV), pp. 29–35.

POPL-2008-NeamtiuHFP #concurrent #programming

Contextual effects for version-consistent dynamic software updating and safe concurrent programming (IN, MH, JSF, PP), pp. 37–49.

POPL-2008-MooreG #semantics #transaction

High-level small-step operational semantics for transactions (KFM, DG), pp. 51–62.

POPL-2008-AbadiBHI #automation #memory management #semantics #transaction

Semantics of transactional memory and automatic mutual exclusion (MA, AB, TH, MI), pp. 63–74.

POPL-2008-ParkinsonB #abstraction #inheritance #logic

Separation logic, abstraction and inheritance (MJP, GMB), pp. 75–86.

POPL-2008-ChinDNQ #composition #logic #object-oriented #verification

Enhancing modular OO verification with separation logic (WNC, CD, HHN, SQ), pp. 87–99.

POPL-2008-BrotherstonBC #logic #proving #termination

Cyclic proofs of program termination in separation logic (JB, RB, CC), pp. 101–112.

POPL-2008-Asperti #theorem

The intensional content of Rice’s theorem (AA), pp. 113–119.

POPL-2008-GaboardiMR #logic

A logical account of pspace (MG, JYM, SRDR), pp. 121–131.

POPL-2008-Danielsson #analysis #complexity #data type #functional #lightweight

Lightweight semiformal time complexity analysis for purely functional data structures (NAD), pp. 133–144.

POPL-2008-McMillan #heuristic #program analysis

Relevance heuristics for program analysis (KLM), pp. 145–146.

POPL-2008-GuptaHMRX #proving

Proving non-termination (AG, TAH, RM, AR, RGX), pp. 147–158.

POPL-2008-Chaudhuri #algorithm #recursion #state machine

Subcubic algorithms for recursive state machines (SC), pp. 159–169.

POPL-2008-LahiriQ #precise #smt #using #verification

Back to the future: revisiting precise program verification using SMT solvers (SKL, SQ), pp. 171–182.

POPL-2008-UnkelL #automation #java

Automatic inference of stationary fields: a generalization of java’s final fields (CU, MSL), pp. 183–195.

POPL-2008-ZhengR #alias #analysis #c

Demand-driven alias analysis for C (XZ, RR), pp. 197–208.

POPL-2008-NitaGC #bytecode #formal method #low level #platform

A theory of platform-dependent low-level software (MN, DG, CC), pp. 209–220.

POPL-2008-YorshYC #generative #precise #summary

Generating precise and concise procedure summaries (GY, EY, SC), pp. 221–234.

POPL-2008-GulwaniMT #logic #quantifier

Lifting abstract interpreters to quantified logical domains (SG, BM, AT), pp. 235–246.

POPL-2008-ChangR #analysis #induction #relational

Relational inductive shape analysis (BYEC, XR), pp. 247–260.

POPL-2008-CastagnaGP #contract #formal method #web #web service

A theory of contracts for web services (GC, NG, LP), pp. 261–272.

POPL-2008-HondaYC #multi

Multiparty asynchronous session types (KH, NY, MC), pp. 273–284.

POPL-2008-Minsky #ml

Caml trading (YM), p. 285.

POPL-2008-McBride #data type

Clowns to the left of me, jokers to the right (pearl): dissecting data structures (CM), pp. 287–295.

POPL-2008-JohannG #data type #programming

Foundations for structured programming with GADTs (PJ, NG), pp. 297–308.

POPL-2008-AcarAB #imperative #self

Imperative self-adjusting computation (UAA, AA, MB), pp. 309–322.

POPL-2008-FournetR #data flow #encryption #implementation #security

Cryptographically sound implementations for typed information-flow security (CF, TR), pp. 323–335.

POPL-2008-Laud #encryption #on the

On the computational soundness of cryptographically masked flows (PL), pp. 337–348.

POPL-2008-AlaviGG #encoding

Extensible encoding of type hierarchies (HSA, SG, RG), pp. 349–358.

POPL-2008-Zeilberger #higher-order #syntax

Focusing and higher-order abstract syntax (NZ), pp. 359–369.

POPL-2008-Pientka #higher-order #programming #syntax

A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions (BP), pp. 371–382.

POPL-2008-HerbelinG #approach #call-by #continuation

An approach to call-by-name delimited continuations (HH, SG), pp. 383–394.

POPL-2008-Tobin-HochstadtF #design #implementation

The design and implementation of typed scheme (STH, MF), pp. 395–406.

POPL-2008-BohannonFPPS #lens #named #string

Boomerang: resourceful lenses for string data (AB, JNF, BCP, AP, AS), pp. 407–419.

POPL-2008-FisherWZW #ad hoc #automation #generative

From dirt to shovels: fully automatic tool generation from ad hoc data (KF, DW, KQZ, PW), pp. 421–434.