Matthias Felleisen, Philippa Gardner
Proceedings of the 22nd European Symposium on Programming
ESOP, 2013.

@proceedings{ESOP-2013,
	address       = "Rome, Italy",
	doi           = "10.1007/978-3-642-37036-6",
	editor        = "Matthias Felleisen and Philippa Gardner",
	isbn          = "978-3-642-37035-9",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 22nd European Symposium on Programming}",
	volume        = 7792,
	year          = 2013,
}

Contents (32 items)

5 ×#concurrent
5 ×#verification
4 ×#analysis
3 ×#composition
3 ×#memory management
3 ×#source code
2 ×#data type
2 ×#higher-order
2 ×#invariant
2 ×#logic

ESOP-2013-MillerCT #distributed #javascript

Distributed Electronic Rights in JavaScript (MSM, TVC, BT), pp. 1–20.

ESOP-2013-BudiuGP #compilation

The Compiler Forest (MB, JG, GDP), pp. 21–40.

ESOP-2013-Chargueraud #semantics

Pretty-Big-Step Semantics (AC), pp. 41–60.

ESOP-2013-JeanninKS

Language Constructs for Non-Well-Founded Computation (JBJ, DK, AS), pp. 61–80.

ESOP-2013-Chang #lazy evaluation

Laziness by Need (SC), pp. 81–100.

ESOP-2013-MatsudaW #named

FliPpr: A Prettier Invertible Printing System (KM, MW), pp. 101–120.

ESOP-2013-AlpuenteBFS #analysis #logic #specification

Slicing-Based Trace Analysis of Rewriting Logic Specifications with iJulienne (MA, DB, FF, JS), pp. 121–124.

ESOP-2013-FilliatreP #named #proving #source code #why

Why3 — Where Programs Meet Provers (JCF, AP), pp. 125–128.

ESOP-2013-EneaSS #composition #invariant

Compositional Invariant Checking for Overlaid and Nested Linked Lists (CE, VS, MS), pp. 129–148.

ESOP-2013-KassiosK #verification

A Discipline for Program Verification Based on Backpointers and Its Use in Observational Disjointness (ITK, EK), pp. 149–168.

ESOP-2013-SvendsenBP #composition #concurrent #data type #reasoning

Modular Reasoning about Separation of Concurrent Data Structures (KS, LB, MJP), pp. 169–188.

ESOP-2013-WickersonDP #logic #proving

Ribbon Proofs for Separation Logic (JW, MD, MJP), pp. 189–208.

ESOP-2013-VazouRJ #refinement

Abstract Refinement Types (NV, PMR, RJ), pp. 209–228.

ESOP-2013-TakikawaST #contract

Constraining Delimited Control with Contracts (AT, TSS, STH), pp. 229–248.

ESOP-2013-GotsmanRY #algorithm #concurrent #memory management #verification

Verifying Concurrent Memory Reclamation Algorithms with Grace (AG, NR, HY), pp. 249–269.

ESOP-2013-CollingbourneDKQ #analysis #gpu #kernel #semantics #verification

Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels (PC, AFD, JK, SQ), pp. 270–289.

ESOP-2013-BouajjaniEEH #concurrent #source code #specification #verification

Verifying Concurrent Programs against Sequential Specifications (AB, ME, CE, JH), pp. 290–309.

ESOP-2013-PetersNG #calculus #on the #process

On Distributability in Process Calculi (KP, UN, UG), pp. 310–329.

ESOP-2013-CairesPPT #behaviour #communication #morphism #parametricity #polymorphism

Behavioral Polymorphism and Parametricity in Session-Based Communication (LC, JAP, FP, BT), pp. 330–349.

ESOP-2013-ToninhoCP #higher-order #integration #monad #process

Higher-Order Processes, Functions, and Sessions: A Monadic Integration (BT, LC, FP), pp. 350–369.

ESOP-2013-LaneseLMSS #concurrent #flexibility

Concurrent Flexible Reversibility (IL, ML, CAM, AS, JBS), pp. 370–390.

ESOP-2013-LuPX #correlation

Structural Lock Correlation with Ownership Types (YL, JP, JX), pp. 391–410.

ESOP-2013-KatoenP #concurrent #implementation #modelling #probability

Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems (JPK, DP), pp. 411–430.

ESOP-2013-KobayashiI #higher-order #model checking #recursion #source code

Model-Checking Higher-Order Programs with Recursive Types (NK, AI), pp. 431–450.

ESOP-2013-SeghirK

Counterexample-Guided Precondition Inference (MNS, DK), pp. 451–471.

ESOP-2013-BeyerHTV #analysis #multi #reachability #reuse

Information Reuse for Multi-goal Reachability Analyses (DB, AH, MT, HV), pp. 472–491.

ESOP-2013-JagadeesanPPR #composition #memory management #modelling #reasoning

Quarantining Weakness — Compositional Reasoning under Relaxed Memory Models (RJ, GP, CP, JR), pp. 492–511.

ESOP-2013-AlglaveKNT #memory management #program transformation #verification

Software Verification for Weak Memory via Program Transformation (JA, DK, VN, MT), pp. 512–532.

ESOP-2013-BouajjaniDM #robust

Checking and Enforcing Robustness against TSO (AB, ED, RM), pp. 533–553.

ESOP-2013-SchererR #data type #type system

GADTs Meet Subtyping (GS, DR), pp. 554–573.

ESOP-2013-SharmaGHALN #algebra #approach #data-driven #invariant

A Data Driven Approach for Algebraic Loop Invariants (RS, SG, BH, AA, PL, AVN), pp. 574–592.

ESOP-2013-HofmannR #analysis #automation #type inference

Automatic Type Inference for Amortised Heap-Space Analysis (MH, DR), pp. 593–613.