![[Berkeley Seminar] Michael Arntzenius | UC Berkeley @ToposInstitute](https://i.ytimg.com/vi/_A9qrqL2D28/maxresdefault.jpg)
Uploaded April 2026 | Updated September 2026, 2 weeks ago
Title: A type system for finitely supported functions via pointed sets, Part 2
ABSTRACT:
Finite maps, in the form of dictionaries, associative arrays, or tables, are a key data type in most language’s standard libraries, but constructing and manipulating them is generally very explicit and loopful. In this talk I’ll demonstrate work in progress on a type system that can guarantee that functions written directly as lambda-expressions are finitely supported, and therefore can be represented as tables. This yields a higher-level, more declarative syntax, similar to logic programming languages or database query languages.
The semantics of my language live in Set, the category of pointed sets and point-preserving maps. In order to define the support of a function f: A → B, one needs a point nil ∈ B; then support f = {x ∈ A : f x ≠ nil}. In fact, finitely supported maps form a graded monad on Set; they are graded by their domain A. To fully flesh out the semantics and type system, I also need the free/forgetful adjunction between Set and Set*.
Unfortunately the typing rules get quite complex. I’d like to know if there’s a simpler way to accomplish the same goals, or a simpler or more general framework for presenting the type system itself.
Paper preprint for the interested: rntz.net/files/finite-functional-programming.pdf
Date: April 7, 2026
Title: A type system for finitely supported functions via pointed sets, Part 2
ABSTRACT:
Finite maps, in the form of dictionaries, associative arrays, or tables, are a key data type in most language’s standard libraries, but constructing and manipulating them is generally very explicit and loopful. In this talk I’ll demonstrate work in progress on a type system that can guarantee that functions written directly as lambda-expressions are finitely supported, and therefore can be represented as tables. This yields a higher-level, more declarative syntax, similar to logic programming languages or database query languages.
The semantics of my language live in Set, the category of pointed sets and point-preserving maps. In order to define the support of a function f: A → B, one needs a point nil ∈ B; then support f = {x ∈ A : f x ≠ nil}. In fact, finitely supported maps form a graded monad on Set; they are graded by their domain A. To fully flesh out the semantics and type system, I also need the free/forgetful adjunction between Set and Set*.
Unfortunately the typing rules get quite complex. I’d like to know if there’s a simpler way to accomplish the same goals, or a simpler or more general framework for presenting the type system itself.
Paper preprint for the interested: rntz.net/files/finite-functional-programming.pdf
Date: April 7, 2026
![[Berkeley Seminar] Michael Arntzenius | UC Berkeley](https://i.ytimg.com/vi/_A9qrqL2D28/mqdefault.jpg "[Berkeley Seminar] Michael Arntzenius | UC Berkeley
Title: A type system for finitely supported functions via pointed sets, Part 2
ABSTRACT:
Finite maps, in the form of dictionaries, associative arrays, or tables, are a key data type in most language’s standard libraries, but constructing and manipulating them is generally very explicit and loopful. In this talk I’ll demonstrate work in progress on a type system that can guarantee that functions written directly as lambda-expressions are finitely supported, and therefore can be represented as tables. This yields a higher-level, more declarative syntax, similar to logic programming languages or database query languages.
The semantics of my language live in Set, the category of pointed sets and point-preserving maps. In order to define the support of a function f: A → B, one needs a point nil ∈ B; then support f = {x ∈ A : f x ≠ nil}. In fact, finitely supported maps form a graded monad on Set; they are graded by their domain A. To fully flesh out the semantics and type system, I also need the free/forgetful adjunction between Set and Set*.
Unfortunately the typing rules get quite complex. I’d like to know if there’s a simpler way to accomplish the same goals, or a simpler or more general framework for presenting the type system itself.
Paper preprint for the interested: https://www.rntz.net/files/finite-functional-programming.pdf
Date: April 7, 2026")
![[Oxford Seminar] Q Le | Free PLTL Algebras and A Coalgebraic LTL Extension of Hyperdoctrines](https://i.ytimg.com/vi/_IHFAxbHYfM/mqdefault.jpg "[Oxford Seminar] Q Le | Free PLTL Algebras and A Coalgebraic LTL Extension of Hyperdoctrines
Oxford Seminar, 18th of September 2025
Abstract: In this seminar, I describe the work I had done over the summer of 2025 at the Topos Institute with José Vitor Paiva Miranda de Siqueira. Inspired by the free Boolean/Heyting algebra of a given set, we develop a free-forgetful adjunction between posets and PLTL temporal algebras, where PLTL denotes propositional linear temporal logic. We provide a description of their induced Eilenberg-Moore categories. We describe how this could be used to temporalise systems and logics through hyperdoctrines and connect this to the stream comonad. We end with future research directions, connecting this topic with the cofree comonad of polynomial functors and temporalising doxastic logic.")
![[DOTS Lectures] 16. Monadicity of double operad algebras](https://i.ytimg.com/vi/_suTwV_UQtc/mqdefault.jpg "[DOTS Lectures] 16. Monadicity of double operad algebras
Part of a lecture series on the Double Operadic Theory of Systems (DOTS) presented by David Jaz Myers.
Some material from these lectures can be found in Davids book on categorical systems theory:
https://www.davidjaz.com/Papers/DynamicalBook.pdf")
![[Berkeley Seminar] Victoria Vollmer | From Graded Foundations to the Foundations of Grading](https://i.ytimg.com/vi/_wLFg3YNfsE/mqdefault.jpg "[Berkeley Seminar] Victoria Vollmer | From Graded Foundations to the Foundations of Grading
Title: From Graded Foundations to the Foundations of Grading
Abstract: In recent decades, monads have come to be an indispensable tool in programming language theory and practice. Graded monads, which generalise monads by allowing the operations of a monad to be ‘stratified’ by a monoid, are a relatively recent innovation which provides the same utility as monads but utilises the monoid structure to provide more fine-grained control. As the use of graded monads rises so does the need to understand them formally. This work examines graded monads as lax 2-functors, to build up to a 2-category of graded monads. This provides concrete definitions of morphisms between graded monads, graded monad distributive laws, and composition of graded monads. We then demonstrate the utility of the 2-category of graded monads by providing the free graded monad construction. Further we show how using the notion of internal graded monad, we can define graded multicategories–which can be used to model graded base logics–as an extension of Leinster’s generalized multicategories.
Date: May 14, 2026")
![[Oxford Seminar] Tim Hosgood | Open translations in mathematics](https://i.ytimg.com/vi/ac7laU1WH7o/mqdefault.jpg "[Oxford Seminar] Tim Hosgood | Open translations in mathematics
Oxford Seminar, 20th of March 2025
Translation, in full generality, is a nuanced and complex art form that requires serious expertise and a holistic approach. So how can we as mathematicians hope to solve the problem of translation in our domain? Furthermore, can we do so without making access to academia even harder for non-native English speakers or hurrying a domain collapse of non-English languages? I believe that the answer to both of these questions can only possibly be yes if we approach translation as a community-driven activity. In this talk, I will speak about my experiences in working on large translation projects with an open-source approach — the technology and methodology that was helpful for doing so, as well as some of the difficulties — and describe the sorts of resources that I believe would have been helpful. Hopefully this can form a starting point for community thought on the types of projects that we could focus on in the future. (This talk is a repeat of a talk given recently at the Isaac Newton Institute).")
![[Berkeley Seminar] Michael Arntzenius (Topos Institute) | A perfect join algorithm?](https://i.ytimg.com/vi/ambisA2jegA/mqdefault.jpg "[Berkeley Seminar] Michael Arntzenius (Topos Institute) | A perfect join algorithm?
Title: A perfect join algorithm? Answering queries in optimal time: Yannakakis’ algorithm
Abstract: If we have a query over some database, how fast can we find all answers for it? If we don’t assume any additional structure (such as indexes on the database), the best possible time is O(IN + OUT): that is, the size of the input (the database) plus the size of the output (the matches for the query). Since we didn’t assume anything about the structure the database is in, any part of it could be relevant, so we have to read the entire database; and by definition we have to write the entire output. Is this achievable? It is, for a particular class of queries: the α-acyclic queries. In this talk I’ll explain how to view queries (and databases) as labelled hypergraphs, define α-acyclicity, and show why and how it allows us to answer queries in linear time using Yannakakis’ algorithm (YA). If I have time, I may: - explain more practical variants on YA such as TreeTrackerJoin - explain the fractional edge cover bound on a query/hypergraph, and how to achieve it using worst-case optimal joins, which handle cyclic queries. - (unlikely) explain further generalizations such as hypertree decompositions of queries.
Date: Aug 4, 2026")
![[Berkeley Seminar] Kevin Carlson | Does it matter whether there are infinite sets?](https://i.ytimg.com/vi/bHKvT1ZACLY/mqdefault.jpg "[Berkeley Seminar] Kevin Carlson | Does it matter whether there are infinite sets?
Title: Does it matter whether there are infinite sets?
Abstract: This talk is mostly an exposition of a bit of philosophy and a bit of math due to JP Mayberry, included by but not necessarily co-limited to (1) the claim that yes, Virginia, you actually do want a foundation (2) that its set theory (3) that this has to be given in the naive Euclid-style sense of the axiomatic method (4) that what this foundation founds is, mainly, the modern structuralist sense of the axiomatic method (so that set theory and category theory are friends after all!) (5) that youre supposed to actually believe the axioms in a traditional Euclid-style axiomatic system (6) that, actually, its not hard to give an explanation of set theory that leads to you actually believing all the axioms (7) EXCEPT the so-called axiom of infinity, which is profoundly non-obvious (8) but highly fruitful so could we really get away without it? (9) a beginning of an anti-Cantorian set theory (so every set is finite) in which nonetheless you seem to have a good chance at doing modern math.
Well...Who cares? I suggest that you might care if you are (a) someone who programs, no doubt having noted that your data structures are actually always finite (b) someone who deals with large objects such as the category of all sets in your math. Mayberrys anti-Cantorian set theory has a clearer treatment of how we ought to correctly approach big objects than any other treatment I know.")
![[Berkeley Seminar] Dennis Chen | Cartesian polynomial monads in HoTT](https://i.ytimg.com/vi/bw3F3iUXBas/mqdefault.jpg "[Berkeley Seminar] Dennis Chen | Cartesian polynomial monads in HoTT
Title: Cartesian polynomial monads in HoTT
Date: November 13, 2024
Abstract: Modern math has shown the necessity of higher categories and higher structures. Infinite coherence data arises quite naturally as one considers various types of topological spaces and homotopy theory, as well as modern treatments of algebraic geometry. One can see simple versions of this problem already when looking at path composition in a topological space. Path composition is not strictly associative, but only associative up to a higher cell. One promising method of presenting higher structures is the development of homotopy type theory, which formulates spaces (up to homtopy equivalence) as its basic objects. However one major obstacle is notating the infinite coherences of infinity categories in homotopy type theory. This is due to the autophagy problem: how can one talk about algebraic structures on types, if the algebraic structures themselves are encoded as types? Here we discuss a solution to the problem by Finster, Allioux, and Sozeau by axiomatizing the nature of polynomial monads, hence allowing themselves certain computational equalities. They then go on to use these polynomial monads to discuss higher structures including higher categories. Essential to their method is Baez and Dolans slice construction, which is able to capture infinite coherences of polynomial monads even if one starts from very strict, classical polynomial monads. This integration of HoTT with polynomial monads I believe is incredibly interesting and could prove to be a very useful foundation/computational system.
https://topos.site/events/berkeley-seminar/")
![[Oxford Seminar] David Corfield | Charles Peirce, inference, and category theory](https://i.ytimg.com/vi/c6-rGLK1Mps/mqdefault.jpg "[Oxford Seminar] David Corfield | Charles Peirce, inference, and category theory
Oxford Seminar, 20th of February 2025
The American philosopher Charles Saunders Peirce (1839-1914) had much to say about the nature of intellectual enquiry. In the realm of deductive logic, category theorists have made important use of his string-diagrammatic logical calculus. But Peirces interests in inference extended beyond deduction to induction and abduction. In this talk I shall be exploring the thesis that we can understand this triple in terms of the category-theoretic notions of composition, extension and lift. We will also touch on his broader semiotics and his account of concept formation.")
![[Berkeley Seminar] Gabriel Goren-Roig | Arboreal coreflections](https://i.ytimg.com/vi/cBtySZMrtgA/mqdefault.jpg "[Berkeley Seminar] Gabriel Goren-Roig | Arboreal coreflections
Title: Arboreal coreflections
Abstract: Arboreal categories are categories of objects with an intrinsic, tree-like process structure giving rise to a bisimilarity relation between objects. This relation can then be transported along an adjunction into an “extensional” category, whose objects are usually relational structures. In this way, the main examples of these so-called arboreal adjunctions recover logical equivalence for various fragments of infinitary first-order logic. This abstract framework provides a solid foundation for game comonads and has been used to obtain extensions and variations of substantial resource-sensitive model-theoretic results such as Rossman’s equirank preservation theorem. However, a key open question is whether we can systematically chart the landscape of the correspondence between logics and arboreal adjunctions.
In this talk, we explore this landscape by focusing on coreflective arboreal adjunctions. As is well known, the theory of (co)monads simplifies greatly in the idempotent case and, accordingly, known idempotent game comonads correspond to variants of basic modal logic, which sit on the lower end of the expressive power spectrum. After reviewing the definition of arboreal categories, we will introduce the concept of a “seed”: a full subcategory of structures generating an arboreal coreflective subcategory via colimit. We will explain some results that help us identify seeds and hence move towards a potential classification theorem. In particular, we will leverage density comonads to characterize coreflective subcategories without explicitly constructing the coreflector. Finally, we will show some examples of arboreal categories that can be obtained employing our results.
Date: July 2, 2025
https://topos.institute/events/berkeley-seminar/")
