ETAPS 2014: 5-13 April 2014, Grenoble, France

ESOP 2014 programme

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