| Tuesday, April 8th |
| 10h30 - 12h30 |
ESOP / Room: Mont Blanc
Type Systems (chair: Matthias Felleisen)
- Justin Slepak, Olin Shivers and Panagiotis Manolios. An Array-Oriented Language with Static Rank Polymorphism (nomination for best paper award)
- Peter Thiemann and Luminous Fennell. Gradual Typing for Annotated Type Systems
- Boris Düdder, Moritz Martens and Jakob Rehof. Staged Composition Synthesis
- Jesper Cockx, Frank Piessens and Dominique Devriese. Overlapping and Order-Independent Patterns
|
| 15h00 - 16h00 |
ESOP / Room: Mont Blanc
Verified Compilation (chair: Steve Zdancewic)
- Lennart Beringer, Gordon Stewart, Robert Dockins and Andrew W. Appel. Verified Compilation for Shared-Memory C
- James T. Perconti and Amal Ahmed. Verifying an Open Compiler Using Multi-Language Semantics
|
| 16h30 - 18h00 |
ESOP / Room: Mont Blanc
Program Verification I (chair: Xavier Leroy)
- Kasper Svendsen and Lars Birkedal. Impredicative Concurrent Abstract Predicates
- Philippa Gardner, Gian Ntzik and Adam Wright. Local Reasoning about File Systems
- Véronique Benzaken, Evelyne Contejean and Stefania Dumbrava. A Coq Formalization of the Relational Data Model
|
| Wednesday, April 9th |
| 10h30 - 12h30 |
ESOP / Room: Mont Blanc
Semantics (chair: Dan Ghica)
- Raphaelle Crubille and Ugo Dal Lago. On Probabilistic Applicative Bisimulation and Call-by-Value Lambda Calculi
- Joaquin Aguado, Michael Mendler, Reinhard von Hanxleden and Insa Fuhrmann. Grounding Synchronous Deterministic Concurrency in Sequential Programming
- Paul Downen and Zena Ariola. The Duality of Construction
- Casper Bach Poulsen and Peter D. Mosses. Deriving Pretty-Big-Step Semantics from Small-Step Semantics
|
| 14h00 - 15h00 |
Room: Amphitheater
ESOP Invited Speaker (chair: Zhong Shao)
Maurice Herlihy (Brown University, US)
Why Concurrent Data Structures are Still Hard |
| 15h00 - 16h00 |
ESOP / Room: Mont Blanc
Concurrency (chair: Paul-Andre Mellies)
- Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey and Germán Andrés Delbianco. Communicating State Transition Systems for Fine-Grained Concurrent Resources
- Oren Zomer, Guy Golan-Gueta, G. Ramalingam and Mooly Sagiv. Checking Linearizability of Encapsulated Extended Operations
|
| 16h30 - 18h00 |
ESOP / Room: Mont Blanc
Linear Types (chair: Tarmo Uustalu)
- Dan Ghica and Alex I. Smith. Bounded Linear Types with Generalised Resources
- Aloïs Brunel, Marco Gaboardi, Damiano Mazza and Steve Zdancewic. A Core Quantitative Coeffect Calculus
- Akira Yoshimizu, Ichiro Hasuo, Claudia Faggian and Ugo Dal Lago. Measurements in Proof Nets as Higher-Order Quantum Circuits
|
| Thursday, April 10th |
| 10h30 - 12h30 |
ESOP / Room: Mont Blanc
Program Verification II (chair: Lennart Beringer)
- Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno and Naoki Kobayashi. Automatic Termination Verification for Higher-Order Functional Programs
- Caterina Urban and Antoine Miné. An Abstract Domain to Infer Ordinal-Valued Ranking Functions
- Martin Brain, Cristina David, Daniel Kroening and Peter Schrammel. Model and Proof Generation for Heap-Manipulating Programs
- João Matos, João Garcia and Paolo Romano. REAP: Reporting Errors Using Alternative Path
|
| 15h00 - 16h00 |
ESOP / Room: Mont Blanc
Network and Process Calculi (chair: Zhong Shao)
- Tony Garnock-Jones, Sam Tobin-Hochstadt and Matthias Felleisen. The Network as a Language Construct
- Laura Bocchi, Hernan Melgratti and Emilio Tuosto. Resolving Non-determinism in Choreographies
|
| 16h30 - 18h00 |
ESOP / Room: Mont Blanc
Program Analysis (chair: Naoki Kobayashi)
- Ravi Mangal, Mayur Naik and Hongseok Yang. A Correspondence between Two Approaches to Interprocedural Analysis in the Presence of Join (nomination for best papers award)
- Zhoulai Fu. Targeted update -- Aggressive Memory Abstraction Beyond Common Sense and its Application on Static Numeric Analysis
- Aparna Kotha, Kapil Anand, Timothy Creech, Khaled Elwazeer, Matthew Smithson and Rajeev Barua. Affine Parallelization of Loops with Run-time Dependent Bounds from Binaries
|