Abstract is missing.
- Time Credits and Time Receipts in IrisGlen Mével, Jacques-Henri Jourdan, François Pottier. 3-29 [doi]
- Meta-F ^\star : Proof Automation with SMT, Tactics, and MetaprogramsGuido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy. 30-59 [doi]
- Semi-automated Reasoning About Non-determinism in C ExpressionsDan Frumin, Léon Gondelman, Robbert Krebbers. 60-87 [doi]
- Safe Deferred Memory Reclamation with TypesIsmail Kuru 0001, Colin S. Gordon. 88-116 [doi]
- Codata in ActionPaul Downen, Zachary Sullivan, Zena M. Ariola, Simon Peyton Jones. 119-146 [doi]
- Composing Bidirectional Programs MonadicallyLi-yao Xia, Dominic Orchard, Meng Wang. 147-175 [doi]
- Counters in Kappa: Semantics, Simulation, and Static AnalysisPierre Boutillier, Ioana Cristescu, Jérôme Feret. 176-204 [doi]
- One Step at a Time - A Functional Derivation of Small-Step Evaluators from Big-Step CounterpartsFerdinand Vesely, Kathleen Fisher. 205-231 [doi]
- Extended Call-by-Push-Value: Reasoning About Effectful Programs and Evaluation OrderDylan McDermott, Alan Mycroft. 235-262 [doi]
- Effectful Normal Form BisimulationUgo Dal Lago, Francesco Gavazzo. 263-292 [doi]
- On the Multi-Language ConstructionSamuele Buro, Isabella Mastroeni. 293-321 [doi]
- Probabilistic Programming Inference via Intensional SemanticsSimon Castellan, Hugo Paquet. 322-349 [doi]
- Handling Polymorphic Algebraic EffectsTaro Sekiyama, Atsushi Igarashi. 353-380 [doi]
- Distributive Disjoint Polymorphism for Compositional ProgrammingXuan Bi, Ningning Xie, Bruno C. D. S. Oliveira, Tom Schrijvers. 381-409 [doi]
- Types by NeedBeniamino Accattoli, Giulio Guerrieri, Maico Leberle. 410-439 [doi]
- Verifiable Certificates for Predicate SubtypingFrédéric Gilbert 0002. 440-466 [doi]
- Robustly Safe CompilationMarco Patrignani, Deepak Garg 0001. 469-498 [doi]
- Compiling Sandboxes: Formally Verified Software Fault IsolationFrédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas P. Jensen, Pierre Wilke. 499-524 [doi]
- Fixing Incremental Computation - Derivatives of Fixpoints, and the Recursive Semantics of DatalogMario Alvarez-Picallo, Alex Eyers-Taylor, Michael Peyton Jones, C.-H. Luke Ong. 525-552 [doi]
- Incremental \lambda -Calculus in Cache-Transfer Style - Static Memoization by Program TransformationPaolo G. Giarrusso, Yann Régis-Gianas, Philipp Schuster. 553-580 [doi]
- Asynchronous Timed Session Types - From Duality to Time-Sensitive ProcessesLaura Bocchi, Maurizio Murgia, Vasco Thudichum Vasconcelos, Nobuko Yoshida. 583-610 [doi]
- Manifest Deadlock-Freedom for Shared Session TypesStephanie Balzer, Bernardo Toninho, Frank Pfenning. 611-639 [doi]
- A Categorical Model of an \mathbf i/o -typed \pi -calculusKen Sakayori, Takeshi Tsukada. 640-667 [doi]
- A Process Algebra for Link Layer ProtocolsRob van Glabbeek, Peter Höfner, Michael Markl. 668-693 [doi]
- Data Races and Static Analysis for Interrupt-Driven KernelsNikita Chopra, Rekha Pai, Deepak D'Souza. 697-723 [doi]
- An Abstract Domain for Trees with Numeric RelationsMatthieu Journault, Antoine Miné, Abdelraouf Ouadjaout. 724-751 [doi]
- A Static Higher-Order Dependency Pair FrameworkCarsten Fuhs, Cynthia Kop. 752-782 [doi]
- Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn ClausesHenning Basold, Ekaterina Komendantskaya, Yue Li. 783-813 [doi]