Hongseok Yang
Proceedings of the 24th European Symposium on Programming
ESOP, 2017.

@proceedings{ESOP-2017,
	doi           = "10.1007/978-3-662-54434-1",
	editor        = "Hongseok Yang",
	isbn          = "['978-3-662-54433-4', '978-3-662-54434-1']",
	publisher     = "{Springer}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 24th European Symposium on Programming}",
	volume        = 10201,
	year          = 2017,
}

Contents (36 items)

ESOP-2017-AlpuimOS #morphism #polymorphism

Disjoint Polymorphism (JA, BCdSO, ZS), pp. 1–28.

ESOP-2017-AnconaDZ #axiom

Generalizing Inference Systems by Coaxioms (DA, FD, EZ), pp. 29–55.

ESOP-2017-Atkey #communication #process #semantics

Observed Communication Semantics for Classical Processes (RA), pp. 56–82.

ESOP-2017-DArgenioBBFH #analysis #formal method #source code

Is Your Software on Dope? - Formal Analysis of Surreptitiously “enhanced” Programs (PRD, GB, SB, BF, HH), pp. 83–110.

ESOP-2017-BlanchetteBL0T #implementation #proving #recursion

Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants (JCB, AB, AL, AP0, DT), pp. 111–140.

ESOP-2017-BonchiGKSZ #confluence #graph grammar #interface

Confluence of Graph Rewriting with Interfaces (FB, FG, AK, PS, FZ), pp. 141–169.

ESOP-2017-BouajjaniEEOT #concurrent #robust #source code #verification

Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency (AB, ME, CE, BKO, ST), pp. 170–200.

ESOP-2017-BoutillierEK #graph grammar #incremental

Incremental Update for Graph Rewriting (PB, TE, JK), pp. 201–228.

ESOP-2017-CairesP #behaviour

Linearity, Control Effects, and Behavioral Types (LC, JAP), pp. 229–259.

ESOP-2017-ChargueraudP #logic

Temporary Read-Only Permissions for Separation Logic (AC, FP), pp. 260–286.

ESOP-2017-ChatterjeeKMP #algorithm #performance #recursion #state machine

Faster Algorithms for Weighted Recursive State Machines (KC, BK, SM, AP), pp. 287–313.

ESOP-2017-Cotton-BarrattM #branch #ml

ML and Extended Branching VASS (CCB, ASM, CHLO), pp. 314–340.

ESOP-2017-CrubilleL #metric #reasoning

Metric Reasoning About λ-Terms: The General Case (RC, UDL), pp. 341–367.

ESOP-2017-CulpepperC #equivalence #probability #random #source code

Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring (RC, AC), pp. 368–392.

ESOP-2017-LagoG #monad #probability #termination #type system

Probabilistic Termination by Monadic Affine Sized Typing (UDL, CG), pp. 393–419.

ESOP-2017-Dinsdale-YoungP #automation #concurrent #fine-grained #verification

Caper - Automatic Verification for Fine-Grained Concurrency (TDY, PdRP, KJA, LB), pp. 420–447.

ESOP-2017-DokoV #concurrent

Tackling Real-Life Relaxed Concurrency with FSL++ (MD, VV), pp. 448–475.

ESOP-2017-Dunfield

Extensible Datasort Refinements (JD), pp. 476–503.

ESOP-2017-0001P #source code #syntax #using

Programs Using Syntax with First-Class Binders (FF0, BP), pp. 504–529.

ESOP-2017-GeorgesMOP #framework #linear #logic #named

LINCX: A Linear Logical Framework with First-Class Contexts (ALG, AM, SO, BP), pp. 530–555.

ESOP-2017-Gibbons #programming

APLicative Programming with Naperian Functors (JG), pp. 556–583.

ESOP-2017-GueneauMKN

Verified Characteristic Formulae for CakeML (AG, MOM, RK, MN), pp. 584–610.

ESOP-2017-JansenKMNZ #logic #reasoning #robust

Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic (CJ, JK, CM, TN0, FZ), pp. 611–638.

ESOP-2017-KhyzhaDGP #partial order #proving #using

Proving Linearizability Using Partial Orders (AK, MD, AG, MJP), pp. 639–667.

ESOP-2017-KopS #complexity #higher-order #nondeterminism #power of #programming #using

The Power of Non-determinism in Higher-Order Implicit Complexity - Characterising Complexity Classes Using Non-deterministic Cons-Free Programming (CK, JGS), pp. 668–695.

ESOP-2017-Krebbers0BJDB #concurrent #higher-order #logic

The Essence of Higher-Order Concurrent Separation Logic (RK, RJ0, AB, JHJ, DD, LB), pp. 696–723.

ESOP-2017-Kuncar0 #consistency #higher-order

Comprehending Isabelle/HOL's Consistency (OK, AP0), pp. 724–749.

ESOP-2017-LeinbergerLS #functional #programming #semantics

The Essence of Functional Programming on Semantic Data (ML, RL, SS), pp. 750–776.

ESOP-2017-Miquey #calculus #dependent type

A Classical Sequent Calculus with Dependent Types (ÉM), pp. 777–803.

ESOP-2017-Padovani #type inference

Context-Free Session Type Inference (LP), pp. 804–830.

ESOP-2017-Sato0 #composition #functional #higher-order #source code #verification

Modular Verification of Higher-Order Functional Programs (RS, NK0), pp. 831–854.

ESOP-2017-Staton #commutative #probability #programming #semantics

Commutative Semantics for Probabilistic Programming (SS), pp. 855–879.

ESOP-2017-TangWXZW0 #analysis #library #performance #reachability #summary

Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization (HT, DW, YX, LZ, XW, LZ0), pp. 880–908.

ESOP-2017-TassarottiJ0 #concurrent #higher-order #logic #refinement

A Higher-Order Logic for Concurrent Termination-Preserving Refinement (JT, RJ0, RH0), pp. 909–936.

ESOP-2017-WoodDLE #composition #equivalence #memory management #verification

Modular Verification of Procedure Equivalence in the Presence of Memory Allocation (TW0, SD, SKL, SE), pp. 937–963.

ESOP-2017-XiongPNG #concurrent #specification

Abstract Specifications for Concurrent Maps (SX, PdRP, GN, PG), pp. 964–990.