Programming Languages and Systems: 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings

Front Matter ....Pages i-xv
Front Matter ....Pages 1-1
 Time Credits and Time Receipts in Iris  (Glen Mével, Jacques-Henri Jourdan, François Pottier)....Pages 3-29
 Meta-F\(^\star \): Proof Automation with SMT, Tactics, and Metaprograms  (Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Cătălin Hriţcu et al.)....Pages 30-59
 Semi-automated Reasoning About Non-determinism in C Expressions  (Dan Frumin, Léon Gondelman, Robbert Krebbers)....Pages 60-87
 Safe Deferred Memory Reclamation with Types  (Ismail Kuru, Colin S. Gordon)....Pages 88-116
Front Matter ....Pages 117-117
 Codata in Action  (Paul Downen, Zachary Sullivan, Zena M. Ariola, Simon Peyton Jones)....Pages 119-146
 Composing Bidirectional Programs Monadically  (Li-yao Xia, Dominic Orchard, Meng Wang)....Pages 147-175
 Counters in Kappa: Semantics, Simulation, and Static Analysis  (Pierre Boutillier, Ioana Cristescu, Jérôme Feret)....Pages 176-204
 One Step at a Time  (Ferdinand Vesely, Kathleen Fisher)....Pages 205-231
Front Matter ....Pages 233-233
 Extended Call-by-Push-Value: Reasoning About Effectful Programs and Evaluation Order  (Dylan McDermott, Alan Mycroft)....Pages 235-262
 Effectful Normal Form Bisimulation  (Ugo Dal Lago, Francesco Gavazzo)....Pages 263-292
 On the Multi-Language Construction  (Samuele Buro, Isabella Mastroeni)....Pages 293-321
 Probabilistic Programming Inference via Intensional Semantics  (Simon Castellan, Hugo Paquet)....Pages 322-349
Front Matter ....Pages 351-351
 Handling Polymorphic Algebraic Effects  (Taro Sekiyama, Atsushi Igarashi)....Pages 353-380
 Distributive Disjoint Polymorphism for Compositional Programming  (Xuan Bi, Ningning Xie, Bruno C. d. S. Oliveira, Tom Schrijvers)....Pages 381-409
 Types by Need  (Beniamino Accattoli, Giulio Guerrieri, Maico Leberle)....Pages 410-439
 Verifiable Certificates for Predicate Subtyping  (Frederic Gilbert)....Pages 440-466
Front Matter ....Pages 467-467
 Robustly Safe Compilation  (Marco Patrignani, Deepak Garg)....Pages 469-498
 Compiling Sandboxes: Formally Verified Software Fault Isolation  (Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas Jensen, Pierre Wilke)....Pages 499-524
 Fixing Incremental Computation  (Mario Alvarez-Picallo, Alex Eyers-Taylor, Michael Peyton Jones, C.-H. Luke Ong)....Pages 525-552
 Incremental \(\lambda \)-Calculus in Cache-Transfer Style  (Paolo G. Giarrusso, Yann Régis-Gianas, Philipp Schuster)....Pages 553-580
Front Matter ....Pages 581-581
 Asynchronous Timed Session Types  (Laura Bocchi, Maurizio Murgia, Vasco Thudichum Vasconcelos, Nobuko Yoshida)....Pages 583-610
 Manifest Deadlock-Freedom for Shared Session Types  (Stephanie Balzer, Bernardo Toninho, Frank Pfenning)....Pages 611-639
 A Categorical Model of an \(\mathbf {i/o}\)-typed \(\pi \)-calculus  (Ken Sakayori, Takeshi Tsukada)....Pages 640-667
 A Process Algebra for Link Layer Protocols  (Rob van Glabbeek, Peter Höfner, Michael Markl)....Pages 668-693
Front Matter ....Pages 695-695
 Data Races and Static Analysis for Interrupt-Driven Kernels  (Nikita Chopra, Rekha Pai, Deepak D’Souza)....Pages 697-723
 An Abstract Domain for Trees with Numeric Relations  (Matthieu Journault, Antoine Miné, Abdelraouf Ouadjaout)....Pages 724-751
 A Static Higher-Order Dependency Pair Framework  (Carsten Fuhs, Cynthia Kop)....Pages 752-782
 Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses  (Henning Basold, Ekaterina Komendantskaya, Yue Li)....Pages 783-813
Back Matter ....Pages 815-816