References

• Graduality and Parametricity: Together Again for the First Time. Max S. New, Dustin Jamner, Amal Ahmed. 2019.
• The Simple Essence of Algebraic Subtyping: Principal Type Inference With Subtyping Made Easy (Functional Pearl). Lionel Parreaux. 2020.
• Staged Compilation With Two-Level Type Theory. András Kovács. 2022.
• An Elementary Illustrated Introduction to Simplicial Sets. Greg Friedman. 2021.
• Dendroidal Sets as Models for Homotopy Operads. Denis-Charles Cisinski, Ieke Moerdijk. 2014.
• Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi. Jose Espirito Santo, Ralph Matthes, Luis Pinto. 2009.
• Tannaka Duality for Comonoids in Cosmoi. Daniel Schäppi. 2009.
• Most Tensor Problems Are NP-Hard. Christopher Hillar, Lek-Heng Lim. 2013.
• A Unified Theory of Function Spaces and Hyperspaces: Local Properties. S. Dolecki, F. Mynard. 2010.
• Non-Deterministic Kleene Coalgebras. Alexandra Silva, Marcello Bonsangue, Jan Rutten. 2010.
• Resumptions, Weak Bisimilarity and Big-Step Semantics for While With Interactive I/O: An Exercise in Mixed Induction-Coinduction. Keiko Nakata, Tarmo Uustalu. 2010.
• Functorial Data Migration. David I. Spivak. 2013.
• A Categorical Outlook on Cellular Automata. Silvio Capobianco, Tarmo Uustalu. 2010.
• Logarithmic Tensor Category Theory for Generalized Modules for a Conformal Vertex Algebra, I: Introduction and Strongly Graded Algebras and Their Generalized Modules. Yi-Zhi Huang, James Lepowsky, Lin Zhang. 2013.
• From Coinductive Proofs to Exact Real Arithmetic: Theory and Applications. Ulrich Berger. 2012.
• Relating Sequent Calculi for Bi-Intuitionistic Propositional Logic. Luís Pinto, Tarmo Uustalu. 2011.
• Double Adjunctions and Free Monads. Thomas M. Fiore, Nicola Gambino, Joachim Kock. 2011.
• A Characterization of Entropy in Terms of Information Loss. John C. Baez, Tobias Fritz, Tom Leinster. 2011.
• Efficient and Correct Stencil Computation via Pattern Matching and Static Typing. Dominic Orchard, Alan Mycroft. 2011.
• Sequentiality vs. Concurrency in Games and Logic. Samson Abramsky. 2011.
• Inductive Types in Homotopy Type Theory. Steve Awodey, Nicola Gambino, Kristina Sojakova. 2012.
• A Dependent Nominal Type Theory. James Cheney. 2012.
• Irrelevance, Heterogeneous Equality, and Call-by-Value Dependent Type Systems. Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich. 2012.
• Structured General Corecursion and Coinductive Graphs [extended Abstract]. Tarmo Uustalu. 2012.
• Programming With Algebraic Effects and Handlers. Andrej Bauer, Matija Pretnar. 2012.
• The Axiom of Multiple Choice and Models for Constructive Set Theory. Benno van den Berg, Ieke Moerdijk. 2013.
• The Homotopy Theory of Coalgebras Over a Comonad. Kathryn Hess, Brooke Shipley. 2013.
• Extensional Models of Untyped Lambda-Mu Calculus. Koji Nakazawa, Shin-ya Katsumata. 2012.
• The Simplicial Model of Univalent Foundations (After Voevodsky). Chris Kapulkin, Peter LeFanu Lumsdaine. 2018.
• Relational Foundations for Functorial Data Migration. David I. Spivak, Ryan Wisnesky. 2015.
• Call-by-Value and Call-by-Name Dual Calculi With Inductive and Coinductive Types. Daisuke Kimura, Makoto Tatsuta. 2013.
• The Algebra of Directed Acyclic Graphs. Marcelo Fiore, Marco Devesas Campos. 2013.
• Automatic Equivalence Proofs for Non-Deterministic Coalgebras. Marcello Bonsangue, Georgiana Caltais, Eugen-Ioan Goriac, Dorel Lucanu, Jan Rutten, Alexandra Silva. 2013.
• Lambda Calculus Synopsis. Anton Salikhmetov. 2013.
• Enumeration of Generalized BCI Lambda-Terms. Olivier Bodini, Danièle Gardy, Bernhard Gittenberger, Alice Jacquot. 2013.
• Linear Logic Without Units. Robin Houston. 2013.
• Sets in Homotopy Type Theory. Egbert Rijke, Bas Spitters. 2014.
• Local Connection Forms Revisited. Efstathios Vassiliou. 2013.
• Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. Bruno Barras, Lourdes del Carmen González Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, Burkhart Wolff. 2013.
• Universal Induction With Varying Sets of Combinators. Alexey Potapov, Sergey Rodionov. 2013.
• Kolmogorov Complexity of Categories. Noson S. Yanofsky. 2013.
• An Effect System for Algebraic Effects and Handlers. Andrej Bauer, Matija Pretnar. 2014.
• Towards Synthetic Descriptive Set Theory: An Instantiation With Represented Spaces. Arno Pauly, Matthew de Brecht. 2014.
• Imperative Programs as Proofs via Game Semantics. Martin Churchill, Jim Laird, Guy McCusker. 2013.
• W-Types in Homotopy Type Theory. Benno van den Berg, Ieke Moerdijk. 2015.
• Indexed Induction and Coinduction, Fibrationally. Neil Ghani, Patricia Johann, Clement Fumex. 2013.
• The Univalence Axiom for Elegant Reedy Presheaves. Michael Shulman. 2015.
• Coalgebraic Characterizations of Context-Free Languages. Joost Winter, Jan J. M. Rutten, Marcello M. Bonsangue. 2013.
• A Coinductive Approach to Proof Search. José Espírito Santo, Ralph Matthes, Luís Pinto. 2013.
• Type Refinement and Monoidal Closed Bifibrations. Paul-André Melliès, Noam Zeilberger. 2013.
• Handling Algebraic Effects. Gordon D Plotkin, Matija Pretnar. 2013.
• Inferring Algebraic Effects. Matija Pretnar. 2014.
• Coinductive Big-Step Semantics for Concurrency. Tarmo Uustalu. 2013.
• Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory. Benedikt Ahrens, Régis Spadotti. 2014.
• Circular Proofs for Gödel-Löb Logic. Daniyar Shamkanov. 2014.
• The Semantic Marriage of Monads and Effects. Dominic Orchard, Tomas Petricek, Alan Mycroft. 2014.
• Higher Inductive Types as Homotopy-Initial Algebras. Kristina Sojakova. 2014.
• A Bayesian Characterization of Relative Entropy. John C. Baez, Tobias Fritz. 2014.
• Quantization via Linear Homotopy Types. Urs Schreiber. 2014.
• Note on the Tensor Product of Dendroidal Sets. Denis-Charles Cisinski, Ieke Moerdijk. 2014.
• The Galois Group of a Stable Homotopy Theory. Akhil Mathew. 2016.
• Towards a Good Notion of Categories of Logics. Caio de Andrade Mendes, Hugo Luiz Mariano. 2016.
• Representation Theory of Logics: A Categorial Approach. Darllan Conceição Pinto, Hugo Luiz Mariano. 2014.
• On Operads, Bimodules and Analytic Functors. Nicola Gambino, André Joyal. 2015.
• An Introduction to the Clocked Lambda Calculus. Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, Andrew Polonsky. 2014.
• Coherence for Skew-Monoidal Categories. Tarmo Uustalu. 2014.
• Natural Models of Homotopy Type Theory. Steve Awodey. 2017.
• On Sweedler's Cofree Cocommutative Coalgebra. Daniel Murfet. 2017.
• Categorical Probability Theory. Kirk Sturtz. 2015.
• Type Theoretical Databases. Henrik Forssell, Håkon Robbestad Gylterud, David I. Spivak. 2014.
• Logic and Linear Algebra: An Introduction. Daniel Murfet. 2017.
• Quantum Gauge Field Theory in Cohesive Homotopy Type Theory. Urs Schreiber, Michael Shulman. 2014.
• When Is a Container a Comonad?. Danel Ahman, James Chapman, Tarmo Uustalu. 2014.
• Kleene Algebras, Regular Languages and Substructural Logics. Christian Wurm. 2014.
• Kan Extensions and Cartesian Monoidal Categories. Ross Street. 2014.
• Pointwise Extensions and Sketches in Bicategories. Ross Street. 2014.
• Skew-Monoidal Reflection and Lifting Theorems. Stephen Lack, Ross Street. 2015.
• Algebraizable Logics and a Functorial Encoding of Its Morphisms. Darllan Conceição Pinto, Hugo Luiz Mariano. 2016.
• The General Universal Property of the Propositional Truncation. Nicolai Kraus. 2015.
• A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While. Keiko Nakata, Tarmo Uustalu. 2015.
• Operads as Polynomial 2-Monads. Mark Weber. 2015.
• Homotopy Techniques for Tensor Decomposition and Perfect Identifiability. Jonathan D. Hauenstein, Luke Oeding, Giorgio Ottaviani, Andrew J. Sommese. 2016.
• Relational Semantics of Linear Logic and Higher-Order Model-Checking. Charles Grellois, Paul-André Melliès. 2015.
• An Isbell Duality Theorem for Type Refinement Systems. Paul-André Melliès, Noam Zeilberger. 2015.
• Finitary Semantics of Linear Logic and Higher-Order Model-Checking. Charles Grellois, Paul-André Melliès. 2015.
• Positive Inductive-Recursive Definitions. Neil Ghani, Fredrik Nordvall Forsberg, Lorenzo Malatesta. 2015.
• Weighted Tensor Products of Joyal Species, Graphs, and Charades. Ross Street. 2016.
• Indexed Linear Logic and Higher-Order Model Checking. Charles Grellois, Paul-André Melliès. 2015.
• Non-Wellfounded Trees in Homotopy Type Theory. Benedikt Ahrens, Paolo Capriotti, Régis Spadotti. 2015.
• Homotopy-Initial Algebras in Type Theory. Steve Awodey, Nicola Gambino, Kristina Sojakova. 2015.
• Higher Galois Theory. Marc Hoyois. 2017.
• Functions Out of Higher Truncations. Paolo Capriotti, Nicolai Kraus, Andrea Vezzosi. 2015.
• Univalent Completion. Benno van den Berg, Ieke Moerdijk. 2015.
• A Compositional Framework for Markov Processes. John C. Baez, Brendan Fong, Blake S. Pollard. 2016.
• Minimal Fibrations of Dendroidal Sets. Ieke Moerdijk, Joost Nuiten. 2015.
• Brouwer's Fixed-Point Theorem in Real-Cohesive Homotopy Type Theory. Michael Shulman. 2017.
• The Frobenius Condition, Right Properness, and Uniform Fibrations. Nicola Gambino, Christian Sattler. 2017.
• The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory. Kristina Sojakova. 2015.
• Proof Equivalence in MLL Is PSPACE-Complete. Willem Heijltjes, Robin Houston. 2016.
• A Coinductive Approach to Computing With Compact Sets. Ulrich Berger, Dieter Spreen. 2016.
• Application of Covariant Analytic Mechanics With Differential Forms to Gravity With Dirac Field. Satoshi Nakajima. 2016.
• Counting and Generating Terms in the Binary Lambda Calculus (Extended Version). Katarzyna Grygiel, Pierre Lescanne. 2015.
• QINL: Query-Integrated Languages. Patrick Schultz, David I. Spivak, Ryan Wisnesky. 2015.
• Proof Relevant Corecursive Resolution. Peng Fu, Ekaterina Komendantskaya, Tom Schrijvers, Andrew Pond. 2015.
• Tensor Decomposition and Homotopy Continuation. Alessandra Bernardi, Noah S. Daleo, Jonathan D. Hauenstein, Bernard Mourrain. 2016.
• Guarded Dependent Type Theory With Coinductive Types. Aleš Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus E. Møgelberg, Lars Birkedal. 2016.
• Heterogeneous Substitution Systems Revisited. Benedikt Ahrens, Ralph Matthes. 2016.
• Semantics for Probabilistic Programming: Higher-Order Functions, Continuous Distributions, and Soft Constraints. Sam Staton, Hongseok Yang, Chris Heunen, Ohad Kammar, Frank Wood. 2016.
• Game-Theoretic Interpretation of Intuitionistic Type Theory. Norihiro Yamada. 2016.
• A Bifibrational Reconstruction of Lawvere's Presheaf Hyperdoctrine. Paul-André Melliès, Noam Zeilberger. 2016.
• Undecidability of the Lambek Calculus With a Relevant Modality. Max Kanovich, Stepan Kuznetsov, Andre Scedrov. 2016.
• From μ-Calculus to Alternating Tree Automata Using Parity Games. M. Fareed Arif. 2016.
• Left Fibrations and Homotopy Colimits II. Gijs Heuts, Ieke Moerdijk. 2016.
• Algebraic Databases. Patrick Schultz, David I. Spivak, Christina Vasilakopoulou, Ryan Wisnesky. 2016.
• Using Session Types as an Effect System. Dominic Orchard, Nobuko Yoshida. 2016.
• A Coinductive Approach to Proof Search Through Typed Lambda-Calculi. José Espírito Santo, Ralph Matthes, Luís Pinto. 2021.
• The Independence of Markov's Principle in Type Theory. Thierry Coquand, Bassel Mannaa. 2017.
• Exact Completion of Path Categories and Algebraic Set Theory -- Part I: Exact Completion of Path Categories. Benno van den Berg, Ieke Moerdijk. 2017.
• Variations on Noetherianness. Denis Firsov, Tarmo Uustalu, Niccolò Veltri. 2016.
• Directed Containers as Categories. Danel Ahman, Tarmo Uustalu. 2016.
• Inhabitation in Simply-Typed Lambda-Calculus Through a Lambda-Calculus for Proof Search. José Espírito Santo, Ralph Matthes, Luís Pinto. 2017.
• Extending Homotopy Type Theory With Strict Equality. Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus. 2016.
• Computational Higher Type Theory I: Abstract Cubical Realizability. Carlo Angiuli, Robert Harper, Todd Wilson. 2016.
• Commutative Algebra: Constructive Methods. Finite Projective Modules. Henri Lombardi, Claude Quitté. 2021.
• No Value Restriction Is Needed for Algebraic Effects and Handlers. Ohad Kammar, Matija Pretnar. 2016.
• An Introduction to Differential Linear Logic: Proof-Nets, Models and Antiderivatives. Thomas Ehrhard. 2016.
• Differential Bundles and Fibrations for Tangent Categories. J. R. B. Cockett, G. S. H. Cruttwell. 2017.
• The Guarded Lambda-Calculus: Programming and Reasoning With Guarded Recursion for Coinductive Types. Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl, Lars Birkedal. 2016.
• Computational Higher Type Theory II: Dependent Cubical Realizability. Carlo Angiuli, Robert Harper. 2017.
• Canonicity for Cubical Type Theory. Simon Huber. 2017.
• On the Likelihood of Normalisation in Combinatory Logic. Maciej Bendkowski, Katarzyna Grygiel, Marek Zaionc. 2016.
• Gödel Logic: From Natural Deduction to Parallel Computation. Federico Aschieri, Agata Ciabattoni, Francesco A. Genco. 2017.
• Reconciling Lambek's Restriction, Cut-Elimination, and Substitution in the Presence of Exponential Modalities. Max Kanovich, Stepan Kuznetsov, Andre Scedrov. 2019.
• Higher-Order Functions and Brouwer's Thesis. Jonathan Sterling. 2021.
• Undecidability of the Lambek Calculus With Subexponential and Bracket Modalities. Max Kanovich, Stepan Kuznetsov, Andre Scedrov. 2017.
• Five Basic Concepts of Axiomatic Rewriting Theory. Paul-André Melliès. 2016.
• New Methods for Old Spaces: Synthetic Differential Geometry. Anders Kock. 2017.
• Game Semantics for Martin-Löf Type Theory. Norihiro Yamada. 2021.
• Formalising Real Numbers in Homotopy Type Theory. Gaëtan Gilbert. 2016.
• Multisets in Type Theory. Håkon Robbestad Gylterud. 2016.
• On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control. Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar. 2017.
• Remarks on Propositional Logics and the Categorial Relationship Between Institutions and Π-Institutions. Darllan Conceição Pinto, Hugo Luiz Mariano. 2016.
• Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg. 2016.
• Quotient Inductive-Inductive Types. Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, Fredrik Nordvall Forsberg. 2017.
• Relative Pseudomonads, Kleisli Bicategories, and Substitution Monoidal Structures. Marcelo Fiore, Nicola Gambino, Martin Hyland, Glynn Winskel. 2017.
• From Multisets to Sets in Hotmotopy Type Theory. Håkon Robbestad Gylterud. 2016.
• A Convenient Category for Higher-Order Probability Theory. Chris Heunen, Ohad Kammar, Sam Staton, Hongseok Yang. 2020.
• Stack Semantics of Type Theory. Thierry Coquand, Bassel Mannaa, Fabian Ruch. 2017.
• A Sequent Calculus for the Tamari Order. Noam Zeilberger. 2017.
• Congruence Closure in Intensional Type Theory. Daniel Selsam, Leonardo de Moura. 2017.
• Dendroidal Spaces, Γ-Spaces and the Special Barratt-Priddy-Quillen Theorem. Pedro Boavida de Brito, Ieke Moerdijk. 2017.
• Quotients in Monadic Programming: Projective Algebras Are Equivalent to Coalgebras. Dusko Pavlovic, Peter-Michael Seidel. 2017.
• Homotopies for Free!. Taichi Uemura. 2017.
• Petri Automata. Paul Brunet, Damien Pous. 2017.
• Deformation Theory With Homotopy Algebra Structures on Tensor Products. Daniel Robert-Nicoud. 2017.
• Models of Type Theory With Strict Equality. Paolo Capriotti. 2017.
• Existentially Closed Brouwerian Semilattices. Luca Carai, Silvio Ghilardi. 2017.
• Homotopy Type Theory: The Logic of Space. Michael Shulman. 2017.
• The Equivalence Between the Categories of Giry-Algebras and Convex Spaces. Kirk Sturtz. 2017.
• The Dendroidal Category Is a Test Category. Dimitri Ara, Denis-Charles Cisinski, Ieke Moerdijk. 2018.
• A Categorical Characterization of Relative Entropy on Standard Borel Spaces. Nicolas Gagne, Prakash Panangaden. 2017.
• Generating Representative Executions [Extended Abstract]. Hendrik Maarand, Tarmo Uustalu. 2017.
• Categories With Dependence and Semantics of Dependent Types. Norihiro Yamada. 2019.
• Monoidal Computer III: A Coalgebraic View of Computability and Complexity. Dusko Pavlovic, Muzamil Yahia. 2018.
• The Complexity of Tree Partitioning. Zhao An, Qilong Feng, Iyad Kanj, Ge Xia. 2017.
• Dependent Session Types. Hanwen Wu, Hongwei Xi. 2017.
• An Expressive Completeness Theorem for Coalgebraic Modal Mu-Calculi. Sebastian Enqvist, Fatemeh Seifan, Yde Venema. 2017.
• A Polynomial Time Algorithm for the Lambek Calculus With Brackets of Bounded Order. Max Kanovich, Stepan Kuznetsov, Glyn Morrill, Andre Scedrov. 2017.
• Revisiting Parametricity: Inductives and Uniformity of Propositions. Abhishek Anand, Greg Morrisett. 2017.
• Two-Level Type Theory and Applications. Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Christian Sattler. 2019.
• Shuffles of Trees. Eric Hoffbeck, Ieke Moerdijk. 2017.
• Categorical Structures for Type Theory in Univalent Foundations. Benedikt Ahrens, Peter LeFanu Lumsdaine, Vladimir Voevodsky. 2018.
• Semantics of Higher Inductive Types. Peter LeFanu Lumsdaine, Mike Shulman. 2019.
• A Type Theory for Synthetic ∞-Categories. Emily Riehl, Michael Shulman. 2017.
• Knowledge Representation in Bicategories of Relations. Evan Patterson. 2017.
• Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic. Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, Alexandra Silva. 2018.
• Representing Nonterminating Rewriting With 𝐅_2^Μ. Peng Fu. 2017.
• Synthetic Homology in Homotopy Type Theory. Robert Graham. 2018.
• Modalities in Homotopy Type Theory. Egbert Rijke, Michael Shulman, Bas Spitters. 2020.
• Univalent Higher Categories via Complete Semi-Segal Types. Paolo Capriotti, Nicolai Kraus. 2017.
• Structure and Semantics. Tom Avery. 2017.
• Fishing in the Stream: Similarity Search Over Endless Data. Naama Kraus, David Carmel, Idit Keidar. 2017.
• Formalising Type-Logical Grammars in Agda. Wen Kokke. 2017.
• Subexponentials in Non-Commutative Linear Logic. Max Kanovich, Stepan Kuznetsov, Vivek Nigam, Andre Scedrov. 2017.
• On Bifibrations of Model Categories. Pierre Cagne, Paul-André Melliès. 2017.
• A Game Semantics of Concurrent Separation Logic. Paul-André Melliès, Léo Stefanesco. 2017.
• Fibred Computational Effects. Danel Ahman. 2017.
• Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC). Amin Timany, Matthieu Sozeau. 2020.
• Temporal Type Theory: A Topos-Theoretic Approach to Systems and Behavior. Patrick Schultz, David I. Spivak. 2017.
• The Univalence Axiom in Cubical Sets. Marc Bezem, Thierry Coquand, Simon Huber. 2017.
• A Type Checking Algorithm for Higher-Rank, Impredicative and Second-Order Types. Peng Fu. 2017.
• Eliminating the Unit Constant in the Lambek Calculus With Brackets. Stepan Kuznetsov. 2017.
• Functorial Semantics for Relational Theories. Filippo Bonchi, Dusko Pavlovic, Pawel Sobocinski. 2017.
• Computational Higher Type Theory III: Univalent Universes and Exact Equality. Carlo Angiuli, Kuen-Bang Hou, Robert Harper. 2017.
• Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs Under Arithmetic. Stefano Berardi, Makoto Tatsuta. 2017.
• Axioms for Modelling Cubical Type Theory in a Topos. Ian Orton, Andrew M. Pitts. 2018.
• Decomposing the Univalence Axiom. Ian Orton, Andrew M. Pitts. 2018.
• A Short Characterization of Relative Entropy. Tom Leinster. 2017.
• ∞-Operads as Analytic Monads. David Gepner, Rune Haugseng, Joachim Kock. 2020.
• Classical System of Martin-Lof's Inductive Definitions Is Not Equivalent to Cyclic Proofs. Stefano Berardi, Makoto Tatsuta. 2019.
• Computational Higher Type Theory IV: Inductive Types. Evan Cavallo, Robert Harper. 2018.
• Internal Universes in Models of Homotopy Type Theory. Daniel R. Licata, Ian Orton, Andrew M. Pitts, Bas Spitters. 2018.
• Disjunctive Axioms and Concurrent Λ-Calculi: A Curry-Howard Approach. F. Aschieri, A. Ciabattoni, F. A. Genco. 2018.
• Polynomial Pseudomonads and Dependent Type Theory. Steve Awodey, Clive Newstead. 2018.
• On Higher Inductive Types in Cubical Type Theory. Thierry Coquand, Simon Huber, Anders Mörtberg. 2018.
• Impredicative Encodings of (Higher) Inductive Types. Steve Awodey, Jonas Frey, Sam Speight. 2018.
• Models of Type Theory Based on Moore Paths. Ian Orton, Andrew M. Pitts. 2019.
• W-Types With Reductions and the Small Object Argument. Andrew Swan. 2018.
• Fixed-Point Elimination in the Intuitionistic Propositional Calculus (Extended Version). Silvio Ghilardi, Maria Joao Gouveia, Luigi Santocanale. 2018.
• On the Use of Computational Paths in Path Spaces of Homotopy Type Theory. Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira, Tiago Mendonça Lucena de Veras. 2018.
• Efficient Mendler-Style Lambda-Encodings in Cedille. Denis Firsov, Richard Blair, Aaron Stump. 2018.
• Seven Sketches in Compositionality: An Invitation to Applied Category Theory. Brendan Fong, David I Spivak. 2018.
• Univalent Polymorphism. Benno van den Berg. 2018.
• Every Metric Space Is Separable in Function Realizability. Andrej Bauer, Andrew Swan. 2019.
• On the Calculation of Fundamental Groups in Homotopy Type Theory by Means of Computational Paths. Tiago Mendonça Lucena de Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira. 2018.
• An Extension of Quillen's Theorem B. Ieke Moerdijk, Joost Nuiten. 2018.
• Symbolical Index Reduction and Completion Rules for Importing Tensor Index Notation Into Programming Languages. Satoshi Egi. 2021.
• Factorisation Systems for Logical Relations and Monadic Lifting in Type-and-Effect System Semantics. Ohad Kammar, Dylan McDermott. 2018.
• Completeness of Cyclic Proofs for Symbolic Heaps. Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura. 2018.
• Modal Dependent Type Theory and Dependent Right Adjoints. Lars Birkedal, Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, Bas Spitters. 2019.
• The Clocks They Are adjunctions:Denotational Semantics for Clocked Type Theory. Bassel Mannaa, Rasmus Ejlers Møgelberg. 2018.
• Graphical Conjunctive Queries. Filippo Bonchi, Jens Seeber, Pawel Sobocinski. 2018.
• Guarded Computational Type Theory. Jonathan Sterling, Robert Harper. 2018.
• A General Framework for Relational Parametricity. Kristina Sojakova, Patricia Johann. 2018.
• Denotational Semantics of Recursive Types in Synthetic Guarded Domain Theory. Rasmus E. Møgelberg, Marco Paviotti. 2018.
• Free Higher Groups in Homotopy Type Theory. Nicolai Kraus, Thorsten Altenkirch. 2020.
• Affine Logic for Constructive Mathematics. Michael Shulman. 2022.
• Encodings of Turing Machines in Linear Logic. James Clift, Daniel Murfet. 2018.
• Derivatives of Turing Machines in Linear Logic. James Clift, Daniel Murfet. 2019.
• Differential Categories Revisited. R. F. Blute, J. R. B. Cockett, J-S. Pacaud Lemay, R. A. G. Seely. 2019.
• Dependently Typed Folds for Nested Data Types. Peng Fu, Peter Selinger. 2018.
• Cartan Geometry in Modal Homotopy Type Theory. Felix Wellen. 2018.
• Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl. Mark Bickford. 2018.
• Indexed Type Theories. Valery Isaev. 2018.
• Hypergraph Categories. Brendan Fong, David I Spivak. 2019.
• Hopf Rings for Grading and Differentials. Branko Nikolić, Ross Street. 2018.
• A Game-Semantic Model of Computation, Revisited: An Automata-Theoretic Perspective. Norihiro Yamada. 2019.
• Universal Properties of Bicategories of Polynomials. Charles Walker. 2018.
• Rule Algebras for Adhesive Categories. Nicolas Behr, Pawel Sobocinski. 2020.
• Localization in Homotopy Type Theory. J. Daniel Christensen, Morgan Opie, Egbert Rijke, Luis Scoccola. 2020.
• What Is Algebraic About Algebraic Effects and Handlers?. Andrej Bauer. 2019.
• An Asynchronous Soundness Theorem for Concurrent Separation Logic. Paul-André Melliès, Léo Stefanesco. 2018.
• On the Logical Complexity of Cyclic Arithmetic. Anupam Das. 2020.
• Homotopical Inverse Diagrams in Categories With Attributes. Chris Kapulkin, Peter LeFanu Lumsdaine. 2020.
• Polymorphic Iterable Sequential Effect Systems. Colin S. Gordon. 2021.
• Convenient Antiderivatives for Differential Linear Categories. Jean-Simon Pacaud Lemay. 2020.
• On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory. Floris van Doorn. 2018.
• Comonadic Base Change for Enriched Categories. Branko Nikolić, Ross Street. 2021.
• Parameterized Games and Parameterized Automata. Arno Pauly. 2018.
• The Power of the Weak. Facundo Carreiro, Alessandro Facchini, Yde Venema, Fabio Zanasi. 2018.
• What Is Applied Category Theory?. Tai-Danae Bradley. 2018.
• Modalities, Cohesion, and Information Flow. G. A. Kavvos. 2018.
• Normalization by Gluing for Free λ-Theories. Jonathan Sterling, Bas Spitters. 2018.
• Quantitative Bisimulations Using Coreflections and Open Morphisms. Jérémy Dubut, Ichiro Hasuo, Shin-ya Katsumata, David Sprunger. 2018.
• Canonical Gauges in Higher Gauge Theory. Andreas Gastel. 2018.
• Codensity Lifting of Monads and Its Dual. Shin-ya Katsumata, Tetsuya Sato, Tarmo Uustalu. 2018.
• Fixpoint Games on Continuous Lattices. Paolo Baldan, Barbara König, Tommaso Padoan, Christina Mika-Michalski. 2021.
• Bisimulation as Path Type for Guarded Recursive Types. Rasmus Ejlers Møgelberg, Niccolò Veltri. 2018.
• A Domain Theory for Statistical Probabilistic Programming. Matthijs Vákár, Ohad Kammar, Sam Staton. 2021.
• Closed Dendroidal Sets and Unital Operads. Ieke Moerdijk. 2018.
• Sequential Effect Systems With Control Operators. Colin S. Gordon. 2020.
• Path Category for Free - Open Morphisms From Coalgebras With Non-Deterministic Branching. Thorsten Wißmann, Jérémy Dubut, Shin-ya Katsumata, Ichiro Hasuo. 2019.
• The Continuous Weak Order. Maria João Gouveia, Luigi Santocanale. 2018.
• Vector Product and Composition Algebras in Braided Monoidal Additive Categories. Ross Street. 2018.
• Towards the Average-Case Analysis of Substitution Resolution in Λ-Calculus. Maciej Bendkowski. 2018.
• Induction, Coinduction, and Fixed Points: A Concise Comparative Survey. Moez A. AbdelGawad. 2019.
• Free Heyting Algebra Endomorphisms: Ruitenburg\'s Theorem and Beyond. Silvio Ghilardi, Luigi Santocanale. 2019.
• A Homotopy Category for Graphs. Tien Chih, Laura Scull. 2020.
• Path Spaces of Higher Inductive Types in Homotopy Type Theory. Nicolai Kraus, Jakob von Raumer. 2019.
• Signatures and Induction Principles for Higher Inductive-Inductive Types. Ambrus Kaposi, András Kovács. 2020.
• Differentials and Distances in Probabilistic Coherence Spaces. Thomas Ehrhard. 2021.
• Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus. Andreas Abel, Christian Sattler. 2019.
• Canonicity and Homotopy Canonicity for Cubical Type Theory. Thierry Coquand, Simon Huber, Christian Sattler. 2022.
• Composing Bidirectional Programs Monadically (With Appendices). Li-yao Xia, Dominic Orchard, Meng Wang. 2019.
• From Cubes to Twisted Cubes via Graph Morphisms in Type Theory. Gun Pinyo, Nicolai Kraus. 2020.
• Bicategories in Univalent Foundations. Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, Niels van der Weide. 2022.
• Nilpotent Types and Fracture Squares in Homotopy Type Theory. Luis Scoccola. 2022.
• Polynomials as Spans. Ross Street. 2020.
• Induction, Coinduction, and Fixed Points: Intuitions and Tutorial. Moez A. AbdelGawad. 2019.
• Mutual Coinduction. Moez A. AbdelGawad. 2019.
• Entropy Modulo a Prime. Tom Leinster. 2020.
• Elaborating Inductive Definitions and Course-of-Values Induction in Cedille. Christopher Jenkins, Colin McDonald, Aaron Stump. 2019.
• Categorical Data Integration for Computational Science. Kristopher Brown, David I. Spivak, Ryan Wisnesky. 2019.
• A General Framework for the Semantics of Type Theory. Taichi Uemura. 2019.
• A HoTT Quantum Equational Theory (Extended Version). Jennifer Paykin, Steve Zdancewic. 2019.
• Taking Linear Logic Apart. Wen Kokke, Fabrizio Montesi, Marco Peressotti. 2019.
• All (∞,1)-Toposes Have Strict Univalent Universes. Michael Shulman. 2019.
• Cubical Syntax for Reflection-Free Extensional Equality. Jonathan Sterling, Carlo Angiuli, Daniel Gratzer. 2019.
• A Comonadic View of Simulation and Quantum Resources. Samson Abramsky, Rui Soares Barbosa, Martti Karvonen, Shane Mansfield. 2019.
• Natural Deduction and Normalization Proofs for the Intersection Type Discipline. Federico Aschieri. 2019.
• On Church's Thesis in Cubical Assemblies. Andrew Swan, Taichi Uemura. 2019.
• Stability Conditions on Morphisms in a Category. Kotaro Kawatani. 2020.
• A (Co)algebraic Theory of Succinct Automata. Gerco van Heerdt, Joshua Moerman, Matteo Sammartino, Alexandra Silva. 2019.
• Enriched Lawvere Theories for Operational Semantics. John C. Baez, Christian Williams. 2020.
• A Non-Wellfounded, Labelled Proof System for Propositional Dynamic Logic. Simon Docherty, Reuben N. S. Rowe. 2019.
• Towards a Constructive Simplicial Model of Univalent Foundations. Nicola Gambino, Simon Henry. 2021.
• Models of Martin-Löf Type Theory From Algebraic Weak Factorisation Systems. Nicola Gambino, Marco Federico Larrea. 2021.
• Bialgebraic Semantics for String Diagrams. Filippo Bonchi, Robin Piedeleu, Pawel Sobocinski, Fabio Zanasi. 2019.
• Foundations of Constructive Probability Theory. Yuen-Kwok Chan. 2019.
• Classifying Types. Egbert Rijke. 2019.
• Functorial Approach to Graph and Hypergraph Theory. Martin Schmidt. 2019.
• An Introduction to Higher Categorical Algebra. David Gepner. 2019.
• ⅋ Means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs. Federico Aschieri, Francesco A. Genco. 2019.
• A Duality Theoretic View on Limits of Finite Structures. Mai Gehrke, Tomáš Jakl, Luca Reggio. 2020.
• The Constructive Kan-Quillen Model Structure: Two New Proofs. Nicola Gambino, Christian Sattler, Karol Szumiło. 2021.
• Codensity Games for Bisimilarity. Yuichi Komorida, Shin-ya Katsumata, Nick Hu, Bartek Klin, Ichiro Hasuo. 2019.
• Reordering Derivatives of Trace Closures of Regular Languages (Full Version). Hendrik Maarand, Tarmo Uustalu. 2019.
• Methods of Constructive Category Theory. Sebastian Posur. 2019.
• On the Elementary Affine Lambda-Calculus With and Without Fixed Points. Lê Thành Dũng Nguyen. 2019.
• A Synthetic Approach to Markov Kernels, Conditional Independence and Theorems on Sufficient Statistics. Tobias Fritz. 2020.
• Good Fibrations Through the Modal Prism. David Jaz Myers. 2022.
• First-Order Homotopical Logic. Joseph Helfer. 2022.
• Information Geometry, Trade-Off Relations, and Generalized Glansdorff-Prigogine Criterion for Stability. Sosuke Ito. 2021.
• A Type-Based HFL Model Checking Algorithm. Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada. 2019.
• Tensor Products of Finitely Presented Functors. Martin Bies, Sebastian Posur. 2019.
• The Marriage of Univalence and Parametricity. Nicolas Tabareau, Éric Tanter, Matthieu Sozeau. 2020.
• Towards Races in Linear Logic. Wen Kokke, J. Garrett Morris, Philip Wadler. 2020.
• Backpropagation in the Simply Typed Lambda-Calculus With Linear Negation. Alois Brunel, Damiano Mazza, Michele Pagani. 2019.
• On Well-Founded and Recursive Coalgebras. Jiří Adámek, Stefan Milius, Lawrence S. Moss. 2020.
• Quantum Programming With Inductive Datatypes: Causality and Affine Type Theory. Romain Péchoux, Simon Perdrix, Mathys Rennela, Vladimir Zamdzhiev. 2019.
• Runners in Action. Danel Ahman, Andrej Bauer. 2020.
• Symbolic Controller Synthesis for Büchi Specifications on Stochastic Systems. Rupak Majumdar, Kaushik Mallik, Sadegh Soudjani. 2020.
• Automata Learning: An Algebraic Approach. Henning Urbat, Lutz Schröder. 2020.
• A Simple Differentiable Programming Language. Martin Abadi, Gordon D. Plotkin. 2020.
• Naive Cubical Type Theory. Bruno Bentzen. 2021.
• Constructing Infinitary Quotient-Inductive Types. Marcelo Fiore, Andrew M. Pitts, S. C. Steenkamp. 2020.
• Failure of Normalization in Impredicative Type Theory With Proof-Irrelevant Propositional Equality. Andreas Abel, Thierry Coquand. 2020.
• Simplicial Sets Inside Cubical Sets. Thomas Streicher, Jonathan Weinberger. 2021.
• Isomorphism Revisited. David McAllester. 2020.
• Synthetic Topology in Homotopy Type Theory for Probabilistic Programming. Martin E. Bidlingmaier, Florian Faissole, Bas Spitters. 2021.
• On the Unity of Logic: A Sequential, Unpolarized Approach. Norihiro Yamada. 2019.
• Constructive Sheaf Models of Type Theory. Thierry Coquand, Fabian Ruch, Christian Sattler. 2020.
• Formalizing the Curry-Howard Correspondence. Juan Ferrer Meleiro, Hugo Luiz Mariano. 2019.
• Action Logic Is Undecidable. Stepan Kuznetsov. 2019.
• Polynomial-Time Exact MAP Inference on Discrete Models With Global Dependencies. Alexander Bauer, Shinichi Nakajima. 2022.
• Interaction Laws of Monads and Comonads. Shin-ya Katsumata, Exequiel Rivas, Tarmo Uustalu. 2019.
• Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing. Mathieu Huot, Sam Staton, Matthijs Vákár. 2020.
• Monotone Recursive Types and Recursive Data Representations in Cedille. Christopher Jenkins, Aaron Stump. 2021.
• Canonical Extensions of Lattices Are More Than Perfect. Andrew P. K. Craig, Maria J. Gouveia, Miroslav Haviar. 2020.
• Non-Wellfounded Sets in Homotopy Type Theory. Håkon Robbestad Gylterud, Elisabeth Bonnevier. 2020.
• Infinitary Action Logic With Exponentiation. Stepan L. Kuznetsov, Stanislav O. Speranski. 2021.
• Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory. Nicolai Kraus, Jakob von Raumer. 2020.
• Star Games and Hydras. Jörg Endrullis, Jan Willem Klop, Roy Overbeek. 2021.
• Unifying Graded and Parameterised Monads. Dominic Orchard, Philip Wadler, Harley Eades III. 2020.
• Intuitionistic Fixed Point Logic. Ulrich Berger, Hideki Tsuiki. 2020.
• Cohomology Fractals. David Bachman, Saul Schleimer, Henry Segerman. 2020.
• Connecting Abstract Logics and Adjunctions in the Theory of (Π-)institutions: Some Theoretical Remarks and Applications. Gabriel Bittencourt Rios, Daniel de Almeida Souza, Darllan Conceição Pinto, Hugo Luiz Mariano. 2020.
• Cartesian Difference Categories: Extended Report. Mario Alvarez-Picallo, Jean-Simon Pacaud Lemay. 2020.
• NP Reasoning in the Monotone Μ-Calculus. Daniel Hausmann, Lutz Schröder. 2020.
• The Cantor-Schröder-Bernstein Theorem for ∞-Groupoids. Martín Hötzel Escardó. 2020.
• Constructing Higher Inductive Types as Groupoid Quotients. Niccolò Veltri, Niels van der Weide. 2021.
• Decomposing Probabilistic Lambda-Calculi. Ugo Dal Lago, Giulio Guerrieri, Willem Heijltjes. 2020.
• A Cubical Language for Bishop Sets. Jonathan Sterling, Carlo Angiuli, Daniel Gratzer. 2022.
• Asynchronous Effects. Danel Ahman, Matija Pretnar. 2020.
• The Sequent Calculus of Skew Monoidal Categories. Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger. 2020.
• Patch Graph Rewriting (Extended Version). Roy Overbeek, Jörg Endrullis. 2020.
• Cartesian Bicategories With Choice. Filippo Bonchi, Jens Seeber, Pawel Sobocinski. 2020.
• Ticking Clocks as Dependent Right Adjoints: Denotational Semantics for Clocked Type Theory. Bassel Mannaa, Rasmus Ejlers Møgelberg, Niccolò Veltri. 2020.
• Noncommutative Poisson Bialgebras. Jiefeng Liu, Chengming Bai, Yunhe Sheng. 2020.
• At the Interface of Algebra and Statistics. Tai-Danae Bradley. 2020.
• A Higher Structure Identity Principle. Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis. 2020.
• An Introduction to Regular Categories. Marino Gran. 2020.
• Freely Adjoining Monoidal Duals. Kevin Coulembier, Ross Street, Michel van den Bergh. 2020.
• A Complete Proof System for 1-Free Regular Expressions Modulo Bisimilarity. Clemens Grabmayer, Wan Fokkink. 2020.
• Linear Dependent Type Theory for Quantum Programming Languages. Peng Fu, Kohei Kishida, Peter Selinger. 2022.
• Models of Homotopy Type Theory With an Interval Type. Valery Isaev. 2020.
• Multi-Dimensional Arrays With Levels. Artjoms {Š}inkarovs. 2020.
• Efficient Lambda Encodings for Mendler-Style Coinductive Types in Cedille. Christopher Jenkins, Aaron Stump, Larry Diehl. 2020.
• Partial Univalence in N-Truncated Type Theory. Christian Sattler, Andrea Vezzosi. 2020.
• Complexity of the Infinitary Lambek Calculus With Kleene Star. Stepan Kuznetsov. 2020.
• Poly: An Abundant Categorical Setting for Mode-Dependent Dynamics. David I. Spivak. 2020.
• A Linear Algebra Approach to Linear Metatheory. James Wood, Robert Atkey. 2021.
• Concurrent Separation Logic Meets Template Games. Paul-André Melliès, Léo Stefanesco. 2020.
• Cubical Models of (∞, 1)-Categories. Brandon Doherty, Chris Kapulkin, Zachery Lindsey, Christian Sattler. 2022.
• A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper. Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger. 2020.
• Comprehension and Quotient Structures in the Language of 2-Categories. Paul-André Melliès, Nicolas Rolland. 2020.
• Internal Parametricity for Cubical Type Theory. Evan Cavallo, Robert Harper. 2021.
• Designing With Static Capabilities and Effects: Use, Mention, and Invariants. Colin S. Gordon. 2020.
• Minimisation in Logical Form. Nick Bezhanishvili, Marcello Bonsangue, Helle Hvid Hansen, Dexter Kozen, Clemens Kupke, Prakash Panangaden, Alexandra Silva. 2020.
• Local Algebraic Effect Theories. Žiga Lukšič, Matija Pretnar. 2020.
• Explicit Effect Subtyping. Georgios Karachalias, Matija Pretnar, Amr Hany Saleh, Stien Vanderhallen, Tom Schrijvers. 2020.
• A Class of Higher Inductive Types in Zermelo-Fraenkel Set Theory. Andrew Swan. 2021.
• Foundations of Regular Coinduction. Francesco Dagnino. 2021.
• A Complete Equational Axiomatisation of Partial Differentiation. Gordon D. Plotkin. 2020.
• Grading Adjoint Logic. Harley Eades III, Dominic Orchard. 2020.
• Large and Infinitary Quotient Inductive-Inductive Types. András Kovács, Ambrus Kaposi. 2020.
• Frege's Theory of Types. Bruno Bentzen. 2020.
• Algebraic Models of Simple Type Theories: A Polynomial Approach. Nathanael Arkor, Marcelo Fiore. 2020.
• The Integers as a Higher Inductive Type. Thorsten Altenkirch, Luis Scoccola. 2020.
• The Hurewicz Theorem in Homotopy Type Theory. J. Daniel Christensen, Luis Scoccola. 2020.
• Game Semantics of Martin-Löf Type Theory, Part III: Its Consistency With Church's Thesis. Norihiro Yamada. 2020.
• Retracing Some Paths in Categorical Semantics: From Process-Propositions-as-Types to Categorified Reals and Computers. Dusko Pavlovic. 2020.
• Graded Hoare Logic and Its Categorical Semantics. Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Tetsuya Sato. 2021.
• Coinductive Proof Search for Polarized Logic With Applications to Full Intuitionistic Propositional Logic. José Espírito Santo, Ralph Matthes, Luís Pinto. 2021.
• Language Models for Some Extensions of the Lambek Calculus. Max Kanovich, Stepan Kuznetsov, Andre Scedrov. 2020.
• The Multiplicative-Additive Lambek Calculus With Subexponential and Bracket Modalities. Max Kanovich, Stepan Kuznetsov, Andre Scedrov. 2020.
• Partial Orders, Residuation, and First-Order Linear Logic. Richard Moot. 2020.
• Logic-Induced Bisimulations. Jim de Groot, Helle Hvid Hansen, Alexander Kurz. 2020.
• Gentzen-Mints-Zucker Duality. Daniel Murfet, William Troiani. 2020.
• Coinductive Invertibility in Higher Categories. Alex Rice. 2020.
• On Sheaf Cohomology and Natural Expansions. Ana Luiza Tenorio, Hugo Luiz Mariano. 2021.
• Comonadic Semantics for Guarded Fragments. Samson Abramsky, Dan Marsden. 2021.
• 2-Adjoint Equivalences in Homotopy Type Theory. Daniel Carranza, Jonathan Chang, Chris Kapulkin, Ryan Sandford. 2021.
• Internal ∞-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT. Nicolai Kraus. 2021.
• Filter Pairs and Natural Extensions of Logics. Peter Arndt, Hugo Luiz Mariano, Darllan Conceição Pinto. 2022.
• A General Definition of Dependent Type Theories. Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine. 2020.
• Internalizing Representation Independence With Univalence. Carlo Angiuli, Evan Cavallo, Anders Mörtberg, Max Zeuner. 2020.
• A Functorial Characterization of Von Neumann Entropy. Arthur J. Parzygnat. 2021.
• Simplicial Model Structures on Pro-Categories. Thomas Blom, Ieke Moerdijk. 2022.
• Logical Foundations for Hybrid Type-Logical Grammars. Richard Moot, Symon Stevens-Guille. 2020.
• On the Nielsen-Schreier Theorem in Homotopy Type Theory. Andrew W Swan. 2022.
• Filtered Cocategories. Volodymyr Lyubashenko. 2020.
• Collapsible Pushdown Parity Games. Christopher H. Broadbent, Arnaud Carayol, Matthew Hague, Andrzej S. Murawski, C. -H. Luke Ong, Olivier Serre. 2020.
• An SMT Solver for Regular Expressions and Linear Arithmetic Over String Length. Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel D. Day, Dirk Nowotka, Vijay Ganesh. 2021.
• Representable Markov Categories and Comparison of Statistical Experiments in Categorical Probability. Tobias Fritz, Tomáš Gonda, Paolo Perrone, Eigil Fjeldgren Rischel. 2020.
• Monoidal Centres and Groupoid-Graded Categories. Branko Nikolić, Ross Street. 2022.
• Graded Modal Dependent Type Theory. Benjamin Moon, Harley Eades III, Dominic Orchard. 2021.
• Whither Semantics?. Samson Abramsky. 2020.
• Coherence of Strict Equalities in Dependent Type Theories. Rafaël Bocquet. 2020.
• Partial Functions and Recursion in Univalent Type Theory. Cory Knapp. 2020.
• The Categorical Origins of Lebesgue Integration. Tom Leinster. 2022.
• A Smart Backtracking Algorithm for Computing Set Partitions With Parts of Certain Sizes. Samer Nofal. 2021.
• Contextuality: At the Borders of Paradox. Samson Abramsky. 2020.
• Functorial Semantics for Partial Theories. Ivan Di Liberti, Fosco Loregian, Chad Nester, Paweł Sobociński. 2020.
• Universal Semantics for the Stochastic Lambda-Calculus. Pedro Amorim, Dexter Kozen, Radu Mardare, Prakash Panangaden, Michael Roberts. 2021.
• A Probabilistic Higher-Order Fixpoint Logic. Yo Mitani, Naoki Kobayashi, Takeshi Tsukada. 2021.
• Multimodal Dependent Type Theory. Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal. 2021.
• String Diagram Rewrite Theory I: Rewriting With Frobenius Structure. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, Fabio Zanasi. 2022.
• Entropy and Diversity: The Axiomatic Approach. Tom Leinster. 2021.
• Cauchy Completeness for DG-Categories. Branko Nikolić, Ross Street, Giacomo Tendas. 2021.
• A Unified Implementation of Automata and Expression Structures, and of the Associated Algorithms Using Enriched Categories. Ludovic Mignot. 2020.
• Syntactic Categories for Dependent Type Theory: Sketching and Adequacy. Daniel Gratzer, Jonathan Sterling. 2021.
• Bidimensional Linear Recursive Sequences and Universality of Unambiguous Register Automata. Corentin Barloy, Lorenzo Clemente. 2021.
• Deductive Systems and Coherence for Skew Prounital Closed Categories. Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger. 2021.
• Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory. Bruno Barras, Valentin Maestracci. 2021.
• Parametricity for Nested Types and GADTs. Patricia Johann, Enrico Ghiorzi. 2021.
• Complete Trace Models of State and Control. Guilhem Jaber, Andrzej S. Murawski. 2021.
• Leafy Automata for Higher-Order Concurrency. Alex Dixon, Ranko Lazić, Andrzej S. Murawski, Igor Walukiewicz. 2021.
• Relational Type Theory (All Proofs). Aaron Stump, Benjamin Delaware, Christopher Jenkins. 2021.
• Proof Theory of Partially Normal Skew Monoidal Categories. Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger. 2021.
• Normalization for Cubical Type Theory. Jonathan Sterling, Carlo Angiuli. 2021.
• K-Theory and Polynomial Functors. Clark Barwick, Saul Glasman, Akhil Mathew, Thomas Nikolaus. 2022.
• Greatest HITs: Higher Inductive Types in Coinductive Definitions via Induction Under Clocks. Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, Andrea Vezzosi. 2022.
• Synthetic Spectra via a Monadic and Comonadic Modality. Mitchell Riley, Eric Finster, Daniel R. Licata. 2021.
• The Effective Model Structure and ∞-Groupoid Objects. Nicola Gambino, Simon Henry, Christian Sattler, Karol Szumiło. 2021.
• Optimal Spectral-Norm Approximate Minimization of Weighted Finite Automata. Borja Balle, Clara Lacroce, Prakash Panangaden, Doina Precup, Guillaume Rabusseau. 2021.
• Commutative Action Logic. Stepan L. Kuznetsov. 2021.
• Relative Induction Principles for Type Theories. Rafaël Bocquet, Ambrus Kaposi, Christian Sattler. 2021.
• The Agda Universal Algebra Library, Part 1: Foundation. William DeMeo. 2021.
• An Extensible Equality Checking Algorithm for Dependent Type Theories. Andrej Bauer, Anja Petković Komel. 2022.
• Univalence in Higher Category Theory. Nima Rasekh. 2021.
• Prioritise the Best Variation. Wen Kokke, Ornela Dardha. 2022.
• Deadlock-Free Session Types in Linear Haskell. Wen Kokke, Ornela Dardha. 2021.
• Connecting Constructive Notions of Ordinals in Homotopy Type Theory. Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. 2021.
• Synthetic Fibered (∞, 1)-Category Theory. Ulrik Buchholtz, Jonathan Weinberger. 2022.
• De Finetti's Theorem in Categorical Probability. Tobias Fritz, Tomáš Gonda, Paolo Perrone. 2021.
• GADTs, Functoriality, Parametricity: Pick Two. Patricia Johann, Enrico Ghiorzi, Daniel Jeffries. 2022.
• Towards a Functorial Description of Quantum Relative Entropy. Arthur J. Parzygnat. 2021.
• (Deep) Induction Rules for GADTs. Patricia Johann, Enrico Ghiorzi. 2021.
• The Topological Mu-Calculus: Completeness and Decidability. Alexandru Baltag, Nick Bezhanishvili, David Fernández-Duque. 2021.
• Parametricity and Semi-Cubical Types. Hugo Moeneclaey. 2022.
• Separating Sessions Smoothly. Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, J. Garrett Morris. 2022.
• Diagrammatic Polyhedral Algebra. Filippo Bonchi, Alessandro Di Giorgio, Pawel Sobocinski. 2021.
• Universal Cohomology Theories. L. Barbieri-Viale. 2021.
• Normalization for Multimodal Type Theory. Daniel Gratzer. 2021.
• An Equational Logical Framework for Type Theories. Robert Harper. 2021.
• String Diagrammatic Electrical Circuit Theory. Guillaume Boisseau, Paweł Sobociński. 2021.
• An Enriched Category Theory of Language: From Syntax to Semantics. Tai-Danae Bradley, John Terilla, Yiannis Vlassopoulos. 2021.
• On Doctrines and Cartesian Bicategories. Filippo Bonchi, Alessio Santamaria, Jens Seeber, Paweł Sobociński. 2021.
• Asymptotic Distribution of Parameters in Trivalent Maps and Linear Lambda Terms. Olivier Bodini, Alexandros Singh, Noam Zeilberger. 2021.
• ∞-Operads as Symmetric Monoidal ∞-Categories. Rune Haugseng, Joachim Kock. 2022.
• From Linear Term Rewriting to Graph Rewriting With Preservation of Termination. Roy Overbeek, Jörg Endrullis. 2021.
• Automatic Differentiation With Higher Infinitesimals, or Computational Smooth Infinitesimal Analysis in Weil Algebra. Hiromi Ishii. 2021.
• Generalized Cohomology Theories for Algebraic Stacks. Adeel A. Khan, Charanya Ravi. 2022.
• Fixed-Points for Quantitative Equational Logics. Radu Mardare, Prakash Panangaden, Gordon Plotkin. 2021.
• A Rewriting Coherence Theorem With Applications in Homotopy Type Theory. Nicolai Kraus, Jakob von Raumer. 2021.
• The Elementary Infinity-Topos of Truncated Coherent Spaces. Mathieu Anel. 2021.
• Dirichlet Polynomials and Entropy. David I. Spivak, Timothy Hosgood. 2021.
• Coherent Differentiation. Thomas Ehrhard. 2021.
• Entropy as a Topological Operad Derivation. Tai-Danae Bradley. 2021.
• Profinite ∞-Operads. Thomas Blom, Ieke Moerdijk. 2021.
• Dynamic Cantor Derivative Logic. David Fernández-Duque, Yoàv Montacute. 2022.
• Type Theories in Category Theory. Tesla Zhang. 2022.
• Bottom-Up Derivatives of Tree Expressions. Samira Attou, Ludovic Mignot, Djelloul Ziadi. 2021.
• Syllepsis in Homotopy Type Theory. Kristina Sojakova. 2021.
• Yoneda Lemma for 𝒟-Simplicial Spaces. Nima Rasekh. 2021.
• The Cumulative Hierarchy in Homotopy Type Theory. Ioannis Eleftheriadis. 2021.
• Some Notions of (Open) Dynamical System on Polynomial Interfaces. Toby St. Clere Smithe. 2021.
• Constructing Coproducts in Locally Cartesian Closed ∞-Categories. Jonas Frey, Nima Rasekh. 2022.
• Termination Analysis for the Π-Calculus by Reduction to Sequential Program Termination. Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada. 2021.
• Congruence Filter Pairs, Adjoints and Leibniz Hierarchy. Peter Arndt, Hugo Luiz Mariano, Darllan Conceição Pinto. 2021.
• Reducing Higher-Order Recursion Scheme Equivalence to Coinductive Higher-Order Constrained Horn Clauses. Jerome Jochems. 2021.
• String Diagram Rewrite Theory III: Confluence With and Without Frobenius. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Paweł Sobociński, Fabio Zanasi. 2022.
• Coalgebra Symmetry for Discrete Systems. G. Gubbiotti, D. Latini, B. K. Tapley. 2022.
• Substructural Fixed-Point Theorems and the Diagonal Argument: Theme and Variations. David Michael Roberts. 2021.
• From Dependent Type Theory to Higher Algebraic Structures. Chaitanya Leena Subramaniam. 2021.
• Free Commutative Monoids in Homotopy Type Theory. Vikraman Choudhury, Marcelo Fiore. 2021.
• First-Order Modal Ξ-Calculus: On the Aspects of Application and Bisimulation. Xinyu Wang. 2023.
• Comonadic Semantics for Hybrid Logic and Bounded Fragments. Samson Abramsky, Dan Marsden. 2021.
• Kripke-Joyal Forcing for Type Theory and Uniform Fibrations. S. Awodey, N. Gambino, S. Hazratpour. 2021.
• Cyclic Shift in the Lambek Calculus. Tikhon Pshenitsyn. 2021.
• Efficient Multi-Partition Topology Optimization. Stijn Koppen, Matthijs Langelaar, Fred van Keulen. 2021.
• Should Type Theory Replace Set Theory as the Foundation of Mathematics. Thorsten Altenkirch. 2022.
• The Finite Dual Coalgebra as a Quantization of the Maximal Spectrum. Manuel L. Reyes. 2021.
• Compositional Thermostatics. John C. Baez, Owen Lynch, Joe Moeller. 2021.
• Strictification of Weakly Stable Type-Theoretic Structures Using Generic Contexts. Rafaël Bocquet. 2021.
• Functorial Aggregation. David I. Spivak. 2022.
• Some Examples of Nonassociative Coalgebras and Supercoalgebras. Daniyar Kozybaev, Ualbai Umirbaev, Viktor Zhelyabin. 2021.
• Monoidal Weak Omega-Categories as Models of a Type Theory. Thibaut Benjamin. 2021.
• Formalization of Dependent Type Theory: The Example of CaTT. Thibaut Benjamin. 2021.
• SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs. Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martínez. 2021.
• Finitary Type Theories With and Without Contexts. Philipp G. Haselwarter, Andrej Bauer. 2021.
• On Representation Categories of A_∞-Algebras and A_∞-Coalgebras. Abhishek Banerjee, Anita Naolekar. 2022.
• Interpreting Lambda Calculus in Domain-Valued Random Variables. Robert Furber, Radu Mardare, Prakash Panangaden, Dana Scott. 2021.
• On Planarity of Graphs in Homotopy Type Theory. Jonathan Prieto-Cubides, Håkon Robbestad Gylterud. 2021.
• Homotopy Limits and Fixed Point Stacks. R. Virk. 2021.
• Implementing a Category-Theoretic Framework for Typed Abstract Syntax. Benedikt Ahrens, Ralph Matthes, Anders Mörtberg. 2021.
• Partition Complexes and Trees. Gijs Heuts, Ieke Moerdijk. 2021.
• Parametric Church's Thesis: Synthetic Computability Without Choice. Yannick Forster. 2021.
• A Cartesian Bicategory of Polynomial Functors in Homotopy Type Theory. Eric Finster, Samuel Mimram, Maxime Lucas, Thomas Seiller. 2021.
• Two Guarded Recursive Powerdomains for Applicative Simulation. Rasmus Ejlers Møgelberg, Andrea Vezzosi. 2021.
• Inductive and Coinductive Predicate Liftings for Effectful Programs. Niccolò Veltri, Niels F. W. Voorneveld. 2021.
• A Braided Lambda Calculus. Masahito Hasegawa. 2021.
• Deriving Distributive Laws for Graded Linear Types. Jack Hughes, Michael Vollmer, Dominic Orchard. 2021.
• Categorical Models for Path Spaces. Emilio Minichiello, Manuel Rivera, Mahmoud Zeinalian. 2022.
• First-Order Game Logic and Modal Mu-Calculus. Noah Abou El Wafa, André Platzer. 2022.
• Structured Handling of Scoped Effects: Extended Version. Zhixuan Yang, Marco Paviotti, Nicolas Wu, Birthe van den Berg, Tom Schrijvers. 2022.
• Polynomial Functors and Shannon Entropy. David I. Spivak. 2022.
• A Reference for Categorical Structures on 𝐏𝐨𝐥𝐲. David I. Spivak. 2022.
• Univalent Foundations and the Equivalence Principle. Benedikt Ahrens, Paige Randall North. 2022.
• Minimality Notions via Factorization Systems and Examples. Thorsten Wißmann. 2022.
• Coalgebraic Semantics for Nominal Automata. Florian Frank, Stefan Milius, Henning Urbat. 2022.
• Galois Connecting Call-by-Value and Call-by-Name. Dylan McDermott, Alan Mycroft. 2023.
• Bilimits in Categories of Partial Maps. Jonathan Sterling. 2022.
• Strict Universes for Grothendieck Topoi. Daniel Gratzer, Michael Shulman, Jonathan Sterling. 2022.
• Limits and Colimits of Synthetic ∞-Categories. César Bardomiano Martínez. 2022.
• A Synthetic Perspective on (∞,1)-Category Theory: Fibrational and Semantic Aspects. Jonathan Weinberger. 2022.
• Fantastic Morphisms and Where to Find Them: A Guide to Recursion Schemes. Zhixuan Yang, Nicolas Wu. 2022.
• Graph Rewriting and Relabeling With PBPO+: A Unifying Theory for Quasitoposes. Roy Overbeek, Jörg Endrullis, Aloïs Rosset. 2022.
• On the Structure of Abelian Hopf Algebras. Tilman Bauer. 2022.
• A Theory of Composing Protocols. Laura Bocchi, Dominic Orchard, A. Laura Voinea. 2022.
• Strict Stability of Extension Types. Jonathan Weinberger. 2022.
• A Coinductive Reformulation of Milner's Proof System for Regular Expressions Modulo Bisimilarity. Clemens Grabmayer. 2022.
• Limits, Colimits, and Spectra of Modelled Spaces. Hisashi Aratake. 2022.
• The Lie Coalgebra of Multiple Polylogarithms. Zachary Greenberg, Dani Kaufman, Haoran Li, Christian K. Zickert. 2022.
• Towards Constructivising the Freyd-Mitchell Embedding Theorem. Anna Giulia Montaruli. 2022.
• Replicate, Reuse, Repeat: Capturing Non-Linear Communication via Session Types and Graded Modal Types. Daniel Marshall, Dominic Orchard. 2022.
• Unifying Cubical and Multimodal Type Theory. Frederik Lerbjerg Aagaard, Magnus Baunsgaard Kristensen, Daniel Gratzer, Lars Birkedal. 2022.
• Game Semantics of Universes. Norihiro Yamada. 2022.
• How Functorial Are (Deep) GADTs?. Patricia Johann, Pierre Cagne. 2022.
• Free Gs-Monoidal Categories and Free Markov Categories. Tobias Fritz, Wendong Liang. 2022.
• Mockingbird Lattices. Samuele Giraudo. 2022.
• Homotopy Equivalence of Topological Categories. David Michael Roberts. 2022.
• Embeddings Between Partial Combinatory Algebras. Anton Golov, Sebastiaan A. Terwijn. 2022.
• The Combinator 𝐌 and the Mockingbird Lattice. Samuele Giraudo. 2022.
• A Unified Treatment of Structural Definitions on Syntax for Capture-Avoiding Substitution, Context Application, Named Substitution, Partial Differentiation, and So On. Tom Hirschowitz, Ambroise Lafont. 2022.
• Normalization by Evaluation for the Lambek Calculus. Niccolò Veltri. 2022.
• Proof Theory of Skew Non-Commutative MILL. Tarmo Uustalu, Niccolò Veltri, Cheng-Syuan Wan. 2022.
• Introducing Sheaves Over Commutative Semicartesian Quantales. Ana Luiza Tenório, Caio de Andrade Mendes, Hugo Luiz Mariano. 2022.
• Untangled: A Complete Dynamic Topological Logic. David Fernández-Duque, Yoàv Montacute. 2022.
• Sheaf Semantics of Termination-Insensitive Noninterference. Jonathan Sterling, Robert Harper. 2022.
• Linear-Algebraic Models of Linear Logic as Categories of Modules Over Sigma-Semirings. Takeshi Tsukada, Kazuyuki Asada. 2022.
• Unboundedness for Recursion Schemes: A Simpler Type System. David Barozzini, Paweł Parys, Jan Wróblewski. 2022.
• Coalgebraic Partition Refinement For All Functors. Jules Jacobs, Thorsten Wißmann. 2022.
• On Quantitative Algebraic Higher-Order Theories. Ugo Dal Lago, Furio Honsell, Marina Lenisa, Paolo Pistone. 2022.
• Internal Sums for Synthetic Fibered (∞,1)-Categories. Jonathan Weinberger. 2022.
• Uniform Interpolation in Coalgebraic Modal Logic. Fatemeh Seifan, Lutz Schröder, Dirk Pattinson. 2022.
• Time and Gödel: Fuzzy Temporal Reasoning in PSPACE. Juan Pablo Aguilera, Martín Diéguez, David Fernández-Duque, Brett McLean. 2022.
• ∞-Type Theories. Hoang Kim Nguyen, Taichi Uemura. 2022.
• A Gödel Calculus for Linear Temporal Logic. Juan Pablo Aguilera, Martín Diéguez, David Fernández-Duque, Brett McLean. 2022.
• Algebraic Presentation of Semifree Monads. Aloïs Rosset, Helle Hvid Hansen, Jörg Endrullis. 2022.
• On the Lambek Embedding and the Category of Product-Preserving Presheaves. Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger. 2022.
• Discrete Density Comonads and Graph Parameters. Samson Abramsky, Tomáš Jakl, Thomas Paine. 2022.
• Univalent Typoids. Iosif Petrakis. 2022.
• Higher Geometric Sheaf Theories. Raffael Stenzel. 2022.
• On Hofmann-Streicher Universes. Steve Awodey. 2022.
• Virtual Concepts in the Theory of Accessible Categories. Stephen Lack, Giacomo Tendas. 2022.
• HyperTree Proof Search for Neural Theorem Proving. Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, Timothée Lacroix. 2022.
• On the Additivity of the Little Cubes Operads. Miguel Barata, Ieke Moerdijk. 2022.
• coCartesian Fibrations and Homotopy Colimits. Amit Sharma. 2022.
• Orbifolds as Microlinear Types in Synthetic Differential Cohesive Homotopy Type Theory. David Jaz Myers. 2022.
• Open Dynamical Systems as Coalgebras for Polynomial Functors, With Application to Predictive Processing. Toby St Clere Smithe. 2022.
• Divergences on Monads for Relational Program Logics. Tetsuya Sato, Shin-ya Katsumata. 2022.
• Monoidal Kleisli Bicategories and the Arithmetic Product of Coloured Symmetric Sequences. Nicola Gambino, Richard Garner, Christina Vasilakopoulou. 2022.
• Robin Milner's Work on Concurrency: An Appreciation. Samson Abramsky. 2022.
• On the Pre- and Promonoidal Structure of Spacetime. James Hefford, Aleks Kissinger. 2022.
• Notes on Presheaf Representations of Strategies and Cohomological Refinements of K-Consistency and K-Equivalence. Samson Abramsky. 2022.
• On the Equivalence of the Lurie's ∞-Operads and Dendroidal ∞-Operads. Vladimir Hinich, Ieke Moerdijk. 2022.
• Regular Monoidal Languages. Matthew Earnshaw, Paweł Sobociński. 2022.
• What Makes a Strong Monad?. Dylan McDermott, Tarmo Uustalu. 2022.
• Interpreting Type Theory in a Quasicategory: A Yoneda Approach. El Mehdi Cherradi. 2022.
• Formalising Fisher\'s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. Chelsea Edmonds, Lawrence C. Paulson. 2022.
• Univalent Categories of Modules. Jarl G. Taxerås Flaten. 2022.
• An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear Π-Calculus. Luca Ciccone, Luca Padovani. 2022.
• The Compatibility of the Minimalist Foundation With Homotopy Type Theory. Michele Contente, Maria Emilia Maietti. 2022.
• The D-Separation Criterion in Categorical Probability. Tobias Fritz, Andreas Klingler. 2022.
• Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus. Marcelo Fiore. 2022.
• Elimination and Cut-Elimination in Multiplicative Linear Logic. Daniel Murfet, William Troiani. 2022.
• Deformations of Yang-Baxter Operators via N-Lie Algebra Cohomology. Mohamed Elhamdadi, Emanuele Zappala. 2022.
• Frobenius Structures in Star-Autonomous Categories. Luigi Santocanale, Cédric de Lacroix. 2022.
• Nominal Matching Logic. James Cheney, Maribel Fernández. 2022.
• Algebraic Groups in Non-Commutative Probability Theory Revisited. Ilya Chevyrev, Kurusch Ebrahimi-Fard, Frédéric Patras. 2022.
• Covariant-Contravariant Refinement Modal Μ-Calculus. Huili Xing. 2022.
• Programs as Diagrams: From Categorical Computability to Computable Categories. Dusko Pavlovic. 2022.
• Type-Theoretic Approaches to Ordinals. Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. 2022.
• Traced Monads and Hopf Monads. Masahito Hasegawa, Jean-Simon Pacaud Lemay. 2022.
• Proof Engineering With Predicate Transformer Semantics. Christa Jenkins, Mark Moir, Harold Carr. 2022.
• Computads for Weak ω-Categories as an Inductive Type. Christopher J. Dean, Eric Finster, Ioannis Markakis, David Reutter, Jamie Vicary. 2022.
• Applications of the Fixed Point Theorem for Group Actions on Buildings to Algebraic Groups Over Polynomial Rings. Peter Abramenko, Andrei S. Rapinchuk, Igor A. Rapinchuk. 2022.
• Grammars Over the Lambek Calculus With Permutation: Recognizing Power and Connection to Branching Vector Addition Systems With States. Tikhon Pshenitsyn. 2022.
• Relational Models for the Lambek Calculus With Intersection and Constants. Stepan L. Kuznetsov. 2022.
• The Functional Machine Calculus II: Semantics. Chris Barrett, Willem Heijltjes, Guy McCusker. 2023.
• Computing Cohomology Rings in Cubical Agda. Thomas Lamiaux, Axel Ljungström, Anders Mörtberg. 2022.
• Affine Monads and Lazy Structures for Bayesian Programming. Swaraj Dash, Younesse Kaddar, Hugo Paquet, Sam Staton. 2022.
• The Functional Machine Calculus. Willem Heijltjes. 2023.
• Builtin Types Viewed as Inductive Families. Guillaume Allais. 2023.
• Inductive Reasoning for Coinductive Types. Alexander Bagnall, Gordon Stewart, Anindya Banerjee. 2023.
• Fast Matching of Regular Patterns With Synchronizing Counting (Technical Report). Lukáš Holík, Juraj Síč, Lenka Turoňová, Tomáš Vojnar. 2023.
• Monadic Expressions and Their Derivatives [extended Version]. Samira Attou, Ludovic Mignot, Clément Miklarz, Florent Nicart. 2023.
• A Typed Lambda-Calculus for Establishing Trust in Probabilistic Programs. Francesco A. Genco, Giuseppe Primiero. 2023.
• A Framework for Higher-Order Effects & Handlers. Birthe van den Berg, Tom Schrijvers. 2023.
• Coinductive Guide to Inductive Transformer Heads. Adam Nemecek. 2023.
• 𝒬-Sets and Friends: Categorical Constructions and Categorical Properties. José Goudet Alvim, Caio de Andrade Mendes, Hugo Luiz Mariano. 2023.
• 𝒬-Sets and Friends: Regarding Singleton and Gluing Completeness. José Goudet Alvim, Caio de Andrade Mendes, Hugo Luiz Mariano. 2023.
• The Formal Theory of Relative Monads. Nathanael Arkor, Dylan McDermott. 2023.
• Kleene Algebra With Tests for Weighted Programs. Igor Sedlár. 2023.
• Effects and Effect Handlers for Programmable Inference. Minh Nguyen, Roly Perera, Meng Wang, Steven Ramsay. 2023.
• Beyond Initial Algebras and Final Coalgebras. Ezra Schoen, Jade Master, Clemens Kupke. 2023.
• Regexes Are Hard: Decision-Making, Difficulties, and Risks in Programming Regular Expressions. Louis G. Michael IV, James Donohue, James C. Davis, Dongyoon Lee, Francisco Servant. 2023.
• Stabilized Profunctors and Stable Species of Structures. Marcelo Fiore, Zeinab Galal, Hugo Paquet. 2023.
• . . 2022.
• Typing With Leftovers - a Mechanization of Intuitionistic Multiplicative-Additive Linear Logic. Guillaume Allais. 2018.
• Unifying Cubical Models of Univalent Type Theory. Evan Cavallo, Anders Mörtberg, Andrew W Swan. 2020.
• For Finitary Induction-Induction, Induction Is Enough. Ambrus Kaposi, András Kovács, Ambroise Lafont. 2020.
• Why Not W?. Jasper Hugunin. 2021.
• Synthetic Integral Cohomology in Cubical Agda. Guillaume Brunerie, Axel Ljungström, Anders Mörtberg. 2022.
• Division by Two, in Homotopy Type Theory. Samuel Mimram, Émile Oleon. 2022.
• On Lookaheads in Regular Expressions With Backreferences. Nariyoshi Chida, Tachio Terauchi. 2022.
• Decision Problems for Linear Logic With Least and Greatest Fixed Points. Anupam Das, Abhishek De, Alexis Saurin. 2022.
• A Stratified Approach to Löb Induction. Daniel Gratzer, Lars Birkedal. 2022.
• A Combinatorial Approach to Higher-Order Structure for Polynomial Functors. Marcelo Fiore, Zeinab Galal, Hugo Paquet. 2022.
• Realisability and Adequacy for (Co)induction. Ulrich Berger. 2009.
• Least and Greatest Fixed Points in Ludics. David Baelde, Amina Doumane, Alexis Saurin. 2015.
• Nominal Presentation of Cubical Sets Models of Type Theory. Andrew M. Pitts. 2015.
• Finitary Corecursion for the Infinitary Lambda Calculus. Stefan Milius, Thorsten Wißmann. 2015.
• On the Positive Calculus of Relations With Transitive Closure. Damien Pous. 2018.
• A Syntax for Higher Inductive-Inductive Types. Ambrus Kaposi, András Kovács. 2018.
• Completeness for Identity-Free Kleene Lattices. Amina Doumane, Damien Pous. 2018.
• Local Validity for Circular Proofs in Linear Logic With Fixed Points. Rémi Nollet, Alexis Saurin, Christine Tasson. 2018.
• Recursion Schemes and Logical Reflection. Christopher Broadbent, Arnaud Carayol, Luke Ong, Olivier Serre. 2010.
• Point-Free, Set-Free Concrete Linear Algebra. Georges Gonthier. 2013.
• Introduction to the Calculus of Inductive Constructions. Christine Paulin-Mohring. 2014.
• Infinitary Proof Theory : The Multiplicative Additive Case. David Baelde, Amina Doumane, Alexis Saurin. 2016.
• Synthetic Philosophy of Mathematics and Natural Sciences Conceptual Analyses From a Grothendieckian Perspective. Giuseppe Longo. 2016.
• Constructive Completeness for the Linear-Time Μ-Calculus. Amina Doumane. 2017.
• Fixed-Point Elimination in the Intuitionistic Propositional Calculus (Extended Version). Silvio Silvio.Ghilardi@unimi.It Ghilardi, Maria Joao Gouveia, Luigi Santocanale. 2018.
• Regular Language Representations in the Constructive Type Theory of Coq. Christian Doczkal, Gert Smolka. 2018.
• State Complexity of Unambiguous Operations on Deterministic Finite Automata. Galina Jirásková, Alexander Okhotin. 2018.
• Infinets: The Parallel Syntax for Non-Wellfounded Proof-Theory. Abhishek De, Alexis Saurin. 2021.
• Bisimulation and Coinduction Enhancements: A Historical Perspective. Damien Pous, Davide Sangiorgi. 2020.
• Implicit Automata in Typed Λ-Calculi I: Aperiodicity in a Non-Commutative Logic. Lê Thành Dũng Nguyễn, Cécilia Pradic. 2023.
• Cyclic Proofs, System T, and the Power of Contraction. Denis Kuperberg, Laureline Pinault, Damien Pous. 2020.
• The Braga Method: Extracting Certified Algorithms From Complex Recursive Schemes in Coq. Dominique Larchey-Wendling, Jean-François Monin. 2021.
• A Recursion-Theoretic Characterization of the Probabilistic Class PP. Ugo Dal Lago, Reinhard Kahle, Isabel Oitavem. 2021.
• Observational Equality: Now For Good. Loïc Pujet, Nicolas Tabareau. 2021.
• Parallelism in Soft Linear Logic. Paulin Jacobé de Naurois. 2021.
• Focusing Gentzen's LK Proof System. Chuck Liang, Dale Miller. 2021.
• Computational Logic Based on Linear Logic and Fixed Points. Matteo Manighetti, Dale Miller. 2022.
• A Constructive and Synthetic Theory of Reducibility: Myhill's Isomorphism Theorem and Post's Problem for Many-One and Truth-Table Reducibility in Coq (Full Version). Yannick Forster, Felix Jahn, Gert Smolka. 2022.
• Decision Problems for Linear Logic With Least and Greatest Fixed Points. Anupam Das, Abhishek De, Alexis Saurin. 2022.
• Λμ-Calculus and Λμ-Calculus: A Capital Difference. Hugo Herbelin, Alexis Saurin. 2010.
• Regular Expression Containment as a Proof Search Problem. Vladimir Komendantsky. 2011.
• A Mechanized Theory of Regular Trees in Dependent Type Theory. Régis Spadotti. 2017.
• On the Infinitary Proof Theory of Logics With Fixed Points. Amina Doumane. 2019.