ETAPS 2021: 27 March-1 April 2021, Luxembourg, Luxembourg (online)

ESOP 2021 programme

All times are in CEST (GMT+2)

Tuesday, March 30
10h40 - 12h00 ESOP

Probabilistic Programming and Verification (Chair: Sam Staton, sam.staton at

  • Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen and Laura Kovács. Automated Termination Analysis of Polynomial Probabilistic Programs [doi]
  • Daniel Lundén, Johannes Borgström and David Broman. Correctness of Sequential Monte Carlo Inference for Probabilistic Programming Languages [doi]
  • Hugo Paquet. Bayesian strategies: probabilistic programs as generalised graphical models [doi]
  • Carol Mak, Luke Ong, Hugo Paquet and Dominik Wagner. Densities of almost-surely terminating probabilistic programs are differentiable almost everywhere [doi]
14h00 - 15h20 ESOP 
Session Types and Concurrency (Chair: Dominic Orchard, d.a.orchard at
  • Patrick Baillot and Alexis Ghyselen. Types for Complexity of Parallel Computation in Pi-Calculus [doi]
  • Alex Keizer, Henning Basold and Jorge A. Pérez. Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols [doi]
  • Ankush Das, Henry DeYoung, Andreia Mordido and Frank Pfenning. Nested Session Types [doi]
  • Sidi Mohamed Beillahi, Ahmed Bouajjani and Constantin Enea. Checking Robustness Between Weak Transactional Consistency Models [doi]
Wednesday, March 31
10h40 - 12h00


Category Theory and Type Theory (Chair: Tarmo Uustalu, tarmo at

  • Marco Gaboardi, Shin-Ya Katsumata, Dominic Orchard and Tetsuya Sato. Graded Hoare Logic and its Categorical Semantics [doi]
  • Benjamin Moon, Harley Eades III and Dominic Orchard. Graded Modal Dependent Type Theory [doi]
  • Guilhem Jaber and Andrzej Murawski. Complete trace models of state and control [doi]
  • Guilhem Jaber and Colin Riba. Temporal Refinements for Guarded Recursive Types [doi]
14h00 - 15h20 ESOP 
Programming Theories and Testing (Chair: Jorge A Perez, j.a.perez at
  • Matthijs Vákár. Reverse AD at Higher Types: Pure, Principled and Denotationally Correct [doi] (Nominated for EATCS best paper award)
  • Gian Pietro Farina, Stephen Chong and Marco Gaboardi. Coupled Relational Symbolic Execution for Differential Privacy [doi]
  • Shu-Hung You, Robert Bruce Findler and Christos Dimoulas. Sound and Complete Concolic Testing for Higher-Order Functions [doi]
  • Harrison Goldstein, John Hughes, Leonidas Lampropoulos and Benjamin C. Pierce. Do Judge a Test by its Cover: Combining Combinatorial and Property-Based Testing [doi]

17h20 -


Invited Speaker: Isil Dillig 

(Chair: Peter Müller)

Thursday, April 1
10h40 - 12h00 ESOP 
Concurrency and Verification (Chair: Hugo Paquet, hugo.paquet at
  • Snigdha Athaiya, Raghavan Komondoor and K Narayan Kumar. Data Flow Analysis of Asynchronous Systems using Infinite Abstract Domains [doi]
  • Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, Krishna S and Viktor Vafeiadis. The Decidability of Verification under PS 2.0 [doi]
  • Maximilian Paul Louis Haslbeck and Peter Lammich. For a Few Dollars More -- Verified Fine-Grained Algorithm Analysis Down to LLVM [doi] (Nominated for EASST best paper award)
  • Oren Ish Shalom, Shachar Itzhaky, Noam Rinetzky and Sharon Shoham. Run-time Complexity Bounds Using Squeezers [doi] (Nominated for EAPLS best paper award)
15h20 - 16h40 ESOP 
Verification and Programming Language Theory (Chair: Marco Gaboardi, gaboardi at
  • Lennart Beringer. Verified Software Units [doi]
  • Florian Zuleger and Jens Pagel. Strong-Separation Logic [doi]
  • Christophe Chareton, Sébastien Bardin, François Bobot, Valentin Perrelle and Benoit Valiron. An Automated Deductive Verication Framework for Circuit-building Quantum Programs [doi]
  • Wilmer Ricciotti and James Cheney. Query Lifting [doi]