ESOP 2021 programme

Probabilistic Programming and Verification (Chair: Sam Staton, sam.staton at cs.ox.ac.uk)

• 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]

• 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]

ESOP 

Category Theory and Type Theory (Chair: Tarmo Uustalu, tarmo at ru.is)

• 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]

• 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 -
18h20

ESOP

Invited Speaker: Isil Dillig 

(Chair: Peter Müller)

• 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)

• 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]