Neil D. Jones, Xavier Leroy
Proceedings of the 31st Symposium on Principles of Programming Languages
POPL, 2004.

@proceedings{POPL-2004,
	acmid         = "964001",
	address       = "Venice, Italy",
	editor        = "Neil D. Jones and Xavier Leroy",
	isbn          = "1-58113-729-X",
	publisher     = "{ACM}",
	title         = "{Proceedings of the 31st Symposium on Principles of Programming Languages}",
	year          = 2004,
}

Contents (29 items)

2 ×#abstract interpretation
2 ×#analysis
2 ×#proving
2 ×#recursion
2 ×#semantics
2 ×#source code
2 ×#using

POPL-2004-Rival #compilation

Symbolic transfer function-based approaches to certified compilation (XR), pp. 1–13.

POPL-2004-Benton #analysis #correctness #program transformation #proving #relational

Simple relational correctness proofs for static analyses and program transformations (NB), pp. 14–25.

POPL-2004-SittampalamML #execution #incremental #specification

Incremental execution of transformation specifications (GS, OdM, KFL), pp. 26–38.

POPL-2004-YuKS #dot-net #formal method #runtime

Formalization of generics for the .NET common language runtime (DY, AK, DS), pp. 39–51.

POPL-2004-VouillonM #fresh look #semantics

Semantic types: a fresh look at the ideal model for types (JV, PAM), pp. 52–63.

POPL-2004-BalatCF #normalisation #partial evaluation #λ-calculus

Extensional normalisation and type-directed partial evaluation for typed λ calculus with sums (VB, RDC, MPF), pp. 64–76.

POPL-2004-Fiore #morphism #polynomial #recursion

Isomorphisms of generic recursive polynomial types (MPF), pp. 77–88.

POPL-2004-PottierG #polymorphism

Polymorphic typed defunctionalization (FP, NG), pp. 89–98.

POPL-2004-JohannV #theorem

Free theorems in the presence of seq (PJ, JV), pp. 99–110.

POPL-2004-Ford #parsing expression grammar

Parsing expression grammars: a recognition-based syntactic foundation (BF), pp. 111–122.

POPL-2004-CaromelHS

Asynchronous and deterministic objects (DC, LH, BPS), pp. 123–134.

POPL-2004-Dal-ZilioLM #logic

A logic you can count on (SDZ, DL, CM), pp. 135–146.

POPL-2004-Yoshida #dependent type #higher-order #mobile #process

Channel dependent types for higher-order mobile processes (NY), pp. 147–160.

POPL-2004-SumiiP #bisimulation

A bisimulation for dynamic sealing (ES, BCP), pp. 161–172.

POPL-2004-CousotC #abstract interpretation #framework

An abstract interpretation-based framework for software watermarking (PC, RC), pp. 173–185.

POPL-2004-GiacobazziM #abstract interpretation

Abstract non-interference: parameterizing non-interference by abstract interpretation (RG, IM), pp. 186–197.

POPL-2004-BhargavanFG #authentication #semantics #web #web service

A semantics for web services authentication (KB, CF, ADG), pp. 198–209.

POPL-2004-Boehm #lazy evaluation

The space cost of lazy reference counting (HJB), pp. 210–219.

POPL-2004-BirkedalTR #garbage collection #reasoning

Local reasoning about a copying garbage collector (LB, NTS, JCR), pp. 220–231.

POPL-2004-HenzingerJMM #abstraction #proving

Abstractions from proofs (TAH, RJ, RM, KLM), pp. 232–244.

POPL-2004-QadeerRR #concurrent #source code

Summarizing procedures in concurrent programs (SQ, SKR, JR), pp. 245–255.

POPL-2004-FlanaganF #named #parallel #source code #thread

Atomizer: a dynamic atomicity checker for multithreaded programs (CF, SNF), pp. 256–267.

POPL-2004-OHearnYR #information management

Separation and information hiding (PWO, HY, JCR), pp. 268–280.

POPL-2004-DunfieldP #bidirectional

Tridirectional typechecking (JD, FP), pp. 281–292.

POPL-2004-Dreyer #recursion #type system

A type system for well-founded recursion (DD), pp. 293–305.

POPL-2004-AnconaZ #java

Principal typings for Java-like languages (DA, EZ), pp. 306–317.

POPL-2004-SankaranarayananSM #generative #invariant #using

Non-linear loop invariant generation using Gröbner bases (SS, HS, ZM), pp. 318–329.

POPL-2004-Muller-OlmS #algebra #analysis #interprocedural #linear #precise

Precise interprocedural analysis through linear algebra (MMO, HS), pp. 330–341.

POPL-2004-GulwaniN #random #using

Global value numbering using random interpretation (SG, GCN), pp. 342–352.