Abstract is missing.
- Trace-Relating Compiler Correctness and Secure CompilationCarmine Abate, Roberto Blanco, Stefan Ciobaca, Adrien Durier, Deepak Garg 0001, Catalin Hritcu, Marco Patrignani, Éric Tanter, Jérémy Thibault. 1-28 [doi]
- Runners in ActionDanel Ahman, Andrej Bauer. 29-55 [doi]
- On the Versatility of Open Logical Relations - Continuity, Automatic Differentiation, and a Containment TheoremGilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo. 56-83 [doi]
- Constructive Game LogicBrandon Bohrer, André Platzer. 84-111 [doi]
- Optimal and Perfectly Parallel Algorithms for On-demand Data-Flow AnalysisKrishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis. 112-140 [doi]
- Concise Read-Only Specifications for Better Synthesis of Programs with PointersAndreea Costea, Amy Zhu, Nadia Polikarpova, Ilya Sergey. 141-168 [doi]
- Soundness Conditions for Big-Step SemanticsFrancesco Dagnino, Viviana Bono, Elena Zucca, Mariangiola Dezani-Ciancaglini. 169-196 [doi]
- Liberate Abstract Garbage Collection from the Stack by Decomposing the HeapKimball Germane, Michael D. Adams 0001. 197-223 [doi]
- SMT-Friendly Formalization of the Solidity Memory ModelÁkos Hajdu, Dejan Jovanovic. 224-250 [doi]
- Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session TypesSung-Shik Jongmans, Nobuko Yoshida. 251-279 [doi]
- Verifying Visibility-Based Weak ConsistencySiddharth Krishna, Michael Emmi, Constantin Enea, Dejan Jovanovic. 280-307 [doi]
- Local Reasoning for Global Graph PropertiesSiddharth Krishna, Alexander J. Summers, Thomas Wies. 308-335 [doi]
- Aneris: A Mechanised Logic for Modular Reasoning about Distributed SystemsMorten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, Lars Birkedal. 336-365 [doi]
- Continualization of Probabilistic Programs With CorrectionJacob Laurel, Sasa Misailovic. 366-393 [doi]
- Semantic Foundations for Deterministic Dataflow and Stream ProcessingKonstantinos Mamouras. 394-427 [doi]
- Connecting Higher-Order Separation Logic to a First-Order Outside WorldWilliam Mansky, Wolf Honoré, Andrew W. Appel. 428-455 [doi]
- Modular Inference of Linear Types for Multiplicity-Annotated ArrowsKazutaka Matsuda. 456-483 [doi]
- RustHorn: CHC-Based Verification for Rust ProgramsYusuke Matsushita 0002, Takeshi Tsukada, Naoki Kobayashi 0001. 484-514 [doi]
- A First-Order Logic with FramesAdithya Murali, Lucas Peña, Christof Löding, P. Madhusudan. 515-543 [doi]
- Proving the Safety of Highly-Available Distributed ObjectsSreeja S. Nair, Gustavo Petri, Marc Shapiro 0001. 544-571 [doi]
- Solving Program Sketches with Large Integer ValuesRong Pan, Qinheping Hu, Rishabh Singh, Loris D'Antoni. 572-598 [doi]
- Modular Relaxed Dependencies in Weak Memory ConcurrencyMarco Paviotti, Simon Cooksey, Anouk Paradis, Daniel Wright, Scott Owens, Mark Batty. 599-625 [doi]
- ARMv8-A System Semantics: Instruction Fetch in Relaxed ArchitecturesBen Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, Peter Sewell. 626-655 [doi]
- Higher-Ranked Annotation Polymorphic Dependency AnalysisFabian Thorand, Jurriaan Hage. 656-683 [doi]
- ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative ProgramsJohn Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, Naoki Kobayashi 0001. 684-714 [doi]
- Mixed SessionsVasco T. Vasconcelos, Filipe Casal, Bernardo Almeida, Andreia Mordido. 715-742 [doi]
- Higher-Order Spreadsheets with Spilled ArraysJack Williams, Nima Joharizadeh, Andrew D. Gordon, Advait Sarkar. 743-769 [doi]