References

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