LICS 2026: Logic in Computer Science

1. Overview

The 41st Annual Symposium on Logic in Computer Science (LICS 2026). Lisbon, 20–23 July 2026. Part of FLOC 2026.

Papers tagged by relevance to current research threads on this site.

Cavallo, Sattler. "Eliminating reversals from cubical type theories"
Coquand, Höfer, Sattler. "Constructive higher sheaf models of type theory with applications to synthetic mathematics"
Felicissimo, Leray, Pujet, Tabareau, Tanter, Winterhalter. "Definitional Proof Irrelevance Made Accessible"
Gratzer, Weinberger, Buchholtz. "The infinity category of infinity categories in simplicial type theory"
Hart, Milner. "Classifying 2-Groups in Homotopy Type Theory"
Huang, Angiuli. "Fat cell structures and generalized algebraic theories"
Ljungström, Pujet. "Cellular Methods in Homotopy Type Theory"

Abate, Giacobbe, Ichtchenko, Roy. "Complete Supermartingale Certificates for omega-Regular Properties"
Barton, Ljungström, Milner, Mörtberg. "A computer formalisation of the Serre finiteness theorem"
de Medeiros, Liu, Li, Aguirre, Birkedal, Tassarotti. "Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic"
Glover, Hoffmann. "LFPL: Revisited and Mechanized"
Garlik, Gryaznov, Lu, Santhanam, Tzameret. "Meta-mathematics of Algebraic Complexity"

Almagor, Arbel, Sheinvald. "A Complexity Bound for Determinisation of Min-Plus Weighted Automata"
Bojańczyk, Casares, Manthe, Parys. "Automata for MSO over infinite trees with quantification over Borel sets of branches"
Casares, Löding, Walukiewicz. "Layered automata: A canonical model for automata over infinite words"
Lehtinen, Prakash, Skrzypczak. "Checking History-Determinism for Parity Automata is in NP"
Puppis, Bianchini. "Minimization of streaming transducers"
Shirmohammadi, Ait El Manssour, Cheval, Worrell. "Differential Tree Automata"

Batz, Kaminski, Kehrer, Klein, Urbat, Schmid. "The Algebra of Iterative Constructions"
Clemente. "Commutative algebras of series"
Fujii, Tsai, Montacute, Hasuo. "Monads and Distributive Laws in Substructural Contexts"
Gao, Shaikh, Kissinger. "Graphical Algebraic Geometry: From Ideals and Varieties to Quantum Calculi"
Gavazzo. "A Pointfree Algebraic Metatheory of Syntax-Based Systems"
Heunen, Kaarsgaard, Lemonnier. "One rig to control them all"
Laurent. "The Logic of Intersection Subtyping"
Lenke, Milius, Urbat. "A Unified Treatment of Substitution for Presheaves, Nominal Sets, Renaming Sets, and so on"
Melliès, Moreau. "A cartesian closed fibration of regular languages"

Barsse, Péchoux, Perdrix. "Quantum Control and General Recursion beyond the Unitary Case"
Barthe et al. "Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions"
Clément. "A Complete Equational Theory for Real-Clifford+CH Quantum Circuits"
Hirata, Tsukada. "Causality in Pure Quantum Computation with Quantum Control"

Ahman, Kammar, Møgelberg. "A convenient fibration for dependently-typed probability theory"
Bacci, Møgelberg. "Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability"
Castellan, Paquet. "Lazy Categorical Semantics for Algebraic Effects"
Cornish, Wang. "A synthetic account of Metropolis–Hastings via categorical probability"
Crubillé. "Interpreting De Finetti's Theorem in the Category of Integrable Cones"
Peterseim, Lopuhaä-Zwakenberg. "Fixed-parameter tractable inference for discrete probabilistic programs, via string diagram algebraisation"

Bizière et al. "Reachability in VASS Extended with Integer Counters"
Guttenberg, Keskin, Meyer. "PVASS Reachability is Decidable"
Balasubramanian, Schmidt. "The Complexity of Nested Reset Counter Systems"
Kawałek, Krzaczkowski. "Complexity Classes Arising from Circuits over Finite Algebraic Structures"

Sakayori, Sangiorgi, Castellan, Clairambault. "Wiring the Pi-calculus to Denotational Semantics"
Zouari. "Forgetting Event Order in Higher-Dimensional Automata"
Brice, Henzinger, Thejaswini. "Dicey Games: Shared Sources of Randomness in Distributed Systems"

Knudstorp, Galatos, Ramanayake, Jipsen. "The logic of bunched implications is undecidable"
Elad, Shoham. "Decidability Results for Fragments of First-Order Logic via a Symbolic Model Property"
Feller, Pinsker. "Decidability of Interpretability"
Colcombet, Rabinovich. "The uniformisation of monadic second-order logic over countable ordinals"
de Jong, Kraus, Mohammadzadeh, Nordvall Forsberg. "Generalized Decidability via Brouwer Trees"

Paper	Thread
Cavallo, Sattler (cubical reversals)	reversible pipeline transforms
Barton et al. (Serre formalisation)	type systems, one tool four ways (Lean section)
Felicissimo et al. (proof irrelevance)	Keeler theorem (Lean formalization)
Castellan, Paquet (algebraic effects)	transform pipeline (effect-free codec contract)