Abstract is missing.
- homotopy.io: A Proof Assistant for Finitely-Presented Globular n-CategoriesNathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru, Jamie Vicary. [doi]
- Automating Boundary Filling in Cubical AgdaMaximilian Doré, Evan Cavallo, Anders Mörtberg. [doi]
- Univalent Enriched Categories and the Enriched Rezk CompletionNiels van der Weide. [doi]
- On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting SystemsFranz Baader, Jürgen Giesl. [doi]
- A Categorical Approach to DIBI ModelsTao Gu, Jialu Bao, Justin Hsu, Alexandra Silva 0001, Fabio Zanasi. [doi]
- Optimizing a Non-Deterministic Abstract Machine with EnvironmentsMalgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Alan Schmitt. [doi]
- The Flower CalculusPablo Donato. [doi]
- Second-Order Generalised Algebraic Theories: Signatures and First-Order SemanticsAmbrus Kaposi, Szumi Xie. [doi]
- State Canonization and Early Pruning in Width-Based Automated Theorem ProvingMateus de Oliveira Oliveira, Farhad Vadiee. [doi]
- Abstraction-Based Decision Making for Statistical Properties (Invited Talk)Filip Cano, Thomas A. Henzinger, Bettina Könighofer, Konstantin Kueffner, Kaushik Mallik. [doi]
- On Iteration in Discrete Probabilistic ProgrammingMateo Torres-Ruiz, Robin Piedeleu, Alexandra Silva 0001, Fabio Zanasi. [doi]
- Commutation Groups and State-Independent ContextualitySamson Abramsky, Serban-Ion Cercelescu, Carmen-Maria Constantin. [doi]
- A Linear Type System for L^p-Metric Sensitivity AnalysisVictor Sannier, Patrick Baillot. [doi]
- A Verified Algorithm for Deciding Pattern CompletenessRené Thiemann, Akihisa Yamada 0002. [doi]
- Substitution for Non-Wellfounded Syntax with Binders Through Monoidal CategoriesRalph Matthes, Kobe Wullaert, Benedikt Ahrens. [doi]
- Two-Dimensional Kripke Semantics I: PresheavesGeorgios Alexandros Kavvos. [doi]
- Mechanized Subject Expansion in Uniform Intersection Types for Perpetual ReductionsAndrej Dudenhefner, Daniele Pautasso. [doi]
- Mirroring Call-By-Need, or Values Acting SillyBeniamino Accattoli, Adrienne Lancelot. [doi]
- Simulating Dependency Pairs by Semantic LabelingTeppei Saito, Nao Hirokawa. [doi]
- Meaningfulness and Genericity in a Subsuming Framework (Invited Talk)Delia Kesner, Victor Arrial, Giulio Guerrieri. [doi]
- Adjoint Natural DeductionJunyoung Jang 0001, Sophia Roshal, Frank Pfenning, Brigitte Pientka. [doi]
- IMELL Cut Elimination with Linear OverheadBeniamino Accattoli, Claudio Sacerdoti Coen. [doi]
- Lean: Past, Present, and Future (Invited Talk)Sebastian Ullrich 0002. [doi]
- Equational Theories and Validity for Logically Constrained Term RewritingTakahito Aoto 0001, Naoki Nishida 0001, Jonas Schöpf. [doi]
- Laplace Distributors and Laplace Transformations for Differential CategoriesMarie Kerjean, Jean-Simon Pacaud Lemay. [doi]
- Delooping Generated Groups in Homotopy Type TheoryCamil Champin, Samuel Mimram, Émile Oleon. [doi]
- Front Matter, Table of Contents, Preface, Conference Organization [doi]
- Böhm and Taylor for All!Aloÿs Dufour, Damiano Mazza. [doi]
- Semantics for a Turing-Complete Reversible Programming Language with Inductive TypesKostia Chardonnet, Louis Lemonnier, Benoît Valiron. [doi]
- Impredicativity, Cumulativity and Product Covariance in the Logical Framework DeduktiThiago Felicissimo, Théo Winterhalter. [doi]
- Representation of Peano Arithmetic in Separation LogicSohei Ito, Makoto Tatsuta. [doi]
- Termination of Generalized Term Rewriting SystemsSalvador Lucas. [doi]
- Machine-Checked Categorical Diagrammatic ReasoningBenoît Guillemet, Assia Mahboubi, Matthieu Piquerez. [doi]
- On the Logical Structure of Some Maximality and Well-Foundedness Principles Equivalent to Choice PrinciplesHugo Herbelin, Jad Koleilat. [doi]