June 2025 - Categories - categories.org.au

Lecture notes by Bill Lawvere
by Michael Barr, Prof. 23 Apr '26

23 Apr '26

I got a request from someone named C. Muster who is searching for a set of lecture notes by Bill that he gave at U. Laval in 1974. Does anyone have a copy that they would be willing to send to him. Michael You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>

5 4

7th Workshop on Formal Topology (7WFTop)-( first annoucement)
by Maria Emilia Maietti 12 Feb '26

12 Feb '26

================================== 7th Workshop on Formal Topology (7WFTop). >From topology to dynamic constructivism, and back. (first announcement) > ------------------------------ The 7th Workshop on Formal Topology will take place in Venice, Italy, on April 13-17, 2026 at Convento di San Francesco della Vigna. This is the seventh of a series of successful meetings on the development of Formal Topology and its connections with related approaches. The first six have been held in Padua (1997), Venice (2002), Padua (2007), Ljubljana (2012), Stockholm (2015), and Birmingham (2019). The meeting is supported by Dipartimento di Matematica “Tullio Levi-Civita” (Università di Padova). ------------------------------ Dynamic constructivism is a new approach to the foundation of mathematics proposed by Giovanni Sambin starting from the 90s and whose forthcoming book is a first organic exposition. The main claim is that mathematics is the result of a dynamic, human process, which stems from the interplay between the construction of mathematical entities, by abstraction and by idealization, and their selection according to their effectiveness in applications to reality and in the organization of mathematics itself. Pointfree topology in the form of Formal Topology and the more recent Positive Topology provides a key tool to link the effective content of mathematics with its ideal one, and thus achieve a synthesis of computation and visual intuition. A careful management of information within a dynamic view "back and forth" from mathematics to its foundation inevitably leads to accepting a plural vision of mathematics, thus enlightening connections between different constructive or even classical approaches to it. INVITED SPEAKERS: Steve Awodey, Andrej Bauer, Ingo Blechschmidt, Francesco Ciraulo, Maria Manuel Clementino, Thierry Coquand, Laura Crosilla, Tom de Jong, Martín Escardó, Hugo Herbelin, Hajime Ishihara, Tatsuji Kawai, Ansten Klev, Takako Nemoto, Michael Rathjen, Giovanni Sambin, Göran Sundholm, Mark van Atten, Steve Vickers, David Wärn, Joshua Wrigley. CONTRIBUTED TALKS There will be room for some contributed talks. Information about abstract submission will appear soon in the website of the workshop. ACCOMODATION The organizers will be happy to help you find accommodation, given the peculiarities of the city of Venice, and are making agreements with some facilities to guarantee partecipants a convenient price for their stay. If you are interested, please write to the workshop email address 7wftop(a)math.unipd.it<mailto:7wftop@math.unipd.it> as soon as possible, indicating "accommodation" in the subject. Finding accommodation at a reasonable price will be difficult or virtually impossible after June-July 2025. REGISTRATION The registration form will be available soon on the workshop website https://events.math.unipd.it/7wftop/. Participation will require a registration fee. SCIENTIFIC COMMITTEE Ingo Blechschmidt (University of Antwerp) Thierry Coquand (Gothenburg University) Martín Escardó (University of Birmingham) Maria Emilia Maietti (University of Padua) Per Martin-Löf (Stockholm University) ORGANIZING COMMITTEE Cipriano Junior Cioffo (University of Pisa) Francesco Ciraulo (University of Padua) Maria Emilia Maietti (University of Padua) Samuele Maschio (University of Padua) Pietro Sabelli (Czech Academy of Science) Giovanni Sambin (University of Padua) CONTACTS For inquiries, please send an e-mail to: 7wftop(a)math.unipd.it<mailto:7wftop@math.unipd.it> You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>

1 3

CfR: Proof Society Summer School and Workshop, Ghent (Belgium), 1-5 September 2025
by Giovanni Solda 01 Jul '25

01 Jul '25

The 7th International School and Workshop on Proof Theory will be organized by Ghent University under the auspices of The Proof Society>. This annual event continues its tradition of uniting students, researchers, and practitioners to explore both the applied and foundational aspects of proof theory. Following the format of previous editions, the event begins with a three-day Summer School (September 1–3) offering five tutorials on a variety of topics related to proof theory. This will be followed by a two-day Workshop (September 4–5) featuring invited lectures and contributed talks. Guided by The Proof Manifesto>, this event embraces the notion of proofs in its broadest sense, welcoming participation and contributions from logic, computer science, mathematics, and beyond. More information can be found on the website: https://proof2025.ugent.be/ IMPORTANT DATES * Notification of acceptance for submitted abstracts: 14th of July * Registration deadline: 31st of July * Summer School: 1st to 3rd of September * Workshop: 4th and 5th of September REGISTRATION Registration is now open. The fees are: * Summer School (regular): 150 euros * Summer School (students): 100 euros * Workshop (regular): 150 euros * Workshop (students): 100 euros * Social dinner: 40 euros * Excursion: 20 euros Further information (and discounts for Flemish students) can be found on the conference website. BEST STUDENT PRESENTATION AWARD As is traditional for the proof Society Workshop, there will be an award for the best student presentation. TUTORIAL SPEAKERS FOR THE SUMMER SCHOOL * Mohammad Ardeshir * Ali Enayat * Raheleh Jalali * Henry Towsner * Albert Visser INVITED SPEAKERS FOR THE WORKSHOP * Juan Pablo Aguilera * Toshiyasu Arai * Iris van der Giessen * Anton Setzer * Arnold Beckmann, who will give a talk in memoriam of Wolfram Pohlers PROGRAM COMMITTEE * Fedor Pakhomov * Bahereh Afshari * Lev Beklemishev * Benno van den Berg * Lorenzo Carlucci * David Fernández-Duque * Balthasar Grabmayr * Stefan Hetzl * Jan Heylen * Rosalie Iemhoff * Mateusz Łełyk * Maria Emilia Maietti * Nicholas Pischke * Takako Nemoto * Monika Seisenberger * Johannes Stern ORGANIZING COMMITTEE * Andreas Weiermann * Fedor Pakhomov * Giovanni Soldà * Mojtaba Mojtahedi * Brett McLean * Alakh Dhruv Chopra * Philipp Provenzano * Lukas Matthias Zenger * Vlad Lazar * Jan Heylen * Daisie Job Rock * Jozefien D’haeseleer * Morgan Callewaert * Joke Meheus You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>

1 0

Call for Papers - RAMiCS 2026 (Będlewo, Poland, 7–10 April 2026)
by Luigi Santocanale 30 Jun '25

30 Jun '25

Apologies for multiple copies of this email; please distribute as you see fit. CALL FOR PAPERS RAMiCS 2026 21st International Conference on Relational and Algebraic Methods in Computer Science Institute of Mathematics of the Polish Academy of Sciences Będlewo, Poland, 7-10 April 2026 https://ramics-conf.github.io/2026 The RAMiCS conference series is the main venue for research on relational algebras, Kleene algebras and similar algebraic formalisms, and their applications as conceptual and methodological tools in computer science and beyond. RAMiCS 2026 will be organized at the Research and Conference Center of the Institute of Mathematics of the Polish Academy of Sciences in Będlewo, close to Poznań in Poland, and will feature both a classical conference and interactive sessions. IMPORTANT DATES * Abstract submission deadline: 1 November 2025 * Paper submission deadline: 6 November 2025 * Author notification: 20 January 2026 * Final version due: 10 February 2026 * Conference dates: 7-10 April 2026 INVITED SPEAKERS * TBA PROGRAM COMMITTEE * Henning Basold, The Netherlands * Manuel Bodirsky, Germany * Andrew Craig, South-Africa * Uli Fahrenberg, France (co-chair) * Wesley Fussner, Czech Republic (co-chair) * Roland Glück, Germany * Damas Gruska, Slovakia * Walter Guttmann, New Zealand * Robin Hirsch, UK * Peter Höfner, Australia * Marcel Jackson, Australia * Ali Jaoua, Qatar * Peter Jipsen, USA * Bartek Klin, UK * Tomasz Kowalski, Poland * Sławek Lasota, Poland * Ioana Leuştean, Romania * Roger Maddux, USA * Nelma Moreira, Portugal * Luigi Santocanale, France (co-chair) * Jas Šemrl, UK * Eugenia Ternovska, Canada * Sara Ugolini, Spain * Michael Winter, Canada * Krzysztof Ziemiański, Poland SCOPE Since 1994, the RAMiCS conference series has been the main venue for research on relational algebras, Kleene algebras and similar algebraic formalisms, and their applications as conceptual and methodological tools in computer science and beyond. Theoretical aspects include semigroups, residuated lattices, semirings, Kleene algebras, relation algebras, quantales and other algebras; their connections with program logics and other logics; their use in the theories of automata, concurrency, formal languages, games, networks and programming languages; the development of algebraic, algorithmic, category-theoretic, coalgebraic and proof-theoretic methods for these theories; their formalisation with theorem provers. Applications of these formalisms span a wide range of domains, including tools and techniques for program specification, verification, and correctness; qualitative and quantitative models of computing systems; algorithm design; automated reasoning; network protocol analysis; optimisation; control; and even social choice theory. We are calling for submission of original work not published or under review for publication elsewhere. The proceedings will be published as part of Springer LNCS. As for earlier RAMiCS conferences, we intend to publish a journal special issue with revised and extended versions of a selection of the best papers. Submission is via EasyChair at https://easychair.org/conferences/?conf=ramics2026 For more information, see https://ramics-conf.github.io/2026/ Please feel free to forward this announcement to interested colleagues. Best regards, The RAMiCS 2026 Organizing Committee -- Luigi Santocanale, professeur, LIS/AMU You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>

1 0

Harold Schellinx 1956-2025
by Valeria de Paiva 30 Jun '25

30 Jun '25

Dear colleagues, Sadly, I write to tell you that Harold Schellinx passed away on 9th June 2025. Harold was a brilliant linear logician and musician, as well as a good friend, https://worm.org/2025/06/11/harold-schellinx-rip/. My sentiments to family and friends. Rest in power, Harold! -- Valeria -- Valeria de Paiva http://vcvpaiva.github.io/ https://topos.institute/ You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>

3 2

Paul Blain Levy wins the 2025 the Alonzo Church Award!
by Jon Sterling 24 Jun '25

24 Jun '25

Dear colleagues, I’m very glad to hear that Paul Blain Levy has won the 2025 Alonzo Church Award for Outstanding Contributions to Logic and Computation, for Call-By-Push-Value. See the announcement here: https://siglog.org/winner-of-the-2025-alonzo-church-award/, from which I quote below: > Initiated by Alonzo Church, the research programme into the λ-calculus as an abstract model of computation has spurred volumes of fundamental research in logic and computation. By the end of the 20th century, the studies of the λ-calculus in its purely logical form and its applied effectful form bifurcated. In an outstanding contribution, Levy has reunited the many existing research streams into the study of one subsuming calculus: Call-by-Push-Value (CBPV). Levy developed and presented an extraordinarily large body of evidence spanning a cross-section of the semantic theory of the λ-calculus and its application to programming language modelling, including: algebraic datatypes, operational semantics, denotational semantics, and equational theories. To date, CBPV remains a unifying starting point in the study of computational and logical phenomena, including: effects, polarisation, term normalisation, type-isomorphisms, and program transformations. In addition to its scientific contribution, the nominated monograph is a unique access-point into the culmination of decades of logic and programming language semantics. — A well-deserved distinction—congratulations, Paul! Best, Jon You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>

1 0

MathOverflow PSA
by David Roberts 24 Jun '25

24 Jun '25

Dear all, I’m writing in my capacity as an elected moderator on MathOverflow (MO), with the knowledge of my fellow mods, and with the permission of the mailing list moderator, with a public service announcement. This is not to start a discussion, but to respond to a recent email calling for people to upvote specific posts on MO. MathOverflow is a community of users with, by now, more than 15 years of accumulated culture. It has an organic fabric and interactions with it will enrich and grow it like a delicate forest. It is a valuable resource that is maintained through a system of collegial trust as well as metrics (mostly invisible) that allow trusted community members to help with the somewhat voluminous quality control process, such as flagging inappropriate posts (outright spam, AI-generated nonsense answers or questions, undergraduate exercises and so on). Part of this ecosystem is the voting process. The community at large will vote as it seems fit. Some users will be present more often and vote more regularly, others might visit only on occasion and rarely cast any votes. Users gain "reputation" points (or as I like to call them “imaginary internet points”) that helps them accumulate trust in the eyes of the software, but these are hidden by default to avoid unwanted secondary effects of gamifying “reputation” as the software-centric designers of the platform have done. However, individual posts (questions and answers) have their net voting score visible, as **a** signal for the quality of the post itself (and not the person). Think of this as analogous to an article-level metric, rather than a journal- or person-level metric. We all want our research to be judged on its own merits, not the container it’s published in, and certainly not for who we personally are. One thing such voting scores reflect is the extent to which a question or answer is working ‘within the rules’ of the site. Since MO is a question-and-answer site, intended to replicate discussion at morning tea, or a colleague down the hall, or a break at a conference, the established norms of the site preclude merely asking a Dorothy Dixer question with the intent to advertise one’s own work. Answering *someone else’s* question with a pointer to one’s own work is of course ok, and useful, and welcome! Similarly, MO is not a blogging service, nor a personal website to track one’s own developing work purely for self-promotion. Edits to posts should be done only as necessary and not too frequently (the software automatically flags what it deems ‘excessive editing’ for mods to respond to). In this context, callings users to go and vote on one's behalf, in any capacity, is a type of voting fraud. It breaks this complex mix of organic structure and (out of expediency) software-driven machine of MO and sows disharmony. Doing this in response to accumulated downvotes on posts that are misaligned with social norms on MO is unhelpful to say the least—regardless of the merits of the mathematical content. I have seen great mathematics on MO that interests and, dare I say it, excites me, but if it is clearly not working within how MO is designed to operate, then I would agree with community downvotes that are attempting to signal this is a misuse of the site. In response to perceived patterns of voting—both *up* and down, though few complain about the former—that are driven by *who the person is*, rather than the mathematical content and the appropriate use of the site, the best course of action is to raise a flag or send the moderators an email so that we can investigate further and, if need be, have the votes reversed and the relevant users warned or suspended. We do this as moderators because this is exactly the type of behavior that is damaging to the organic fabric of the site. An upvoting spree on every post by one’s friend is just as system-straining as a downvoting spree on an adversary, or someone with a (real or perceived) infraction of site norms in a single case. It behoves us as category theorists to raise the profile of our field by sharing our knowledge in a collegial way, by providing a chance for our more junior members to make a reputation for themselves outside the community. MathOverflow is an excellent opportunity to do this. We welcome questions and if people know their tentative steps onto that big scary platform will be answered appropriately (and yes, the site can always improve, but it is a very large and slow ship - the board that oversees MO really does care about this issue), then it will lift CT and spread appreciation in a number of small ways. Your humble servant, David Michael Roberts You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>

1 0

Emily Riehl talk in Birmingham
by Paul Levy 24 Jun '25

24 Jun '25

Emily Riehl is this year’s Hardy lecturer, sponsored by the London Mathematical Society. She is touring the UK and her talks are listed here: https://www.lms.ac.uk/events/lectures/hardy-lectureship#Hardy%20Current On Wednesday 2 July at 11:00 she is speaking in Birmingham (title and abstract below), followed by a lunch reception. To register for this free event, please register at https://forms.cloud.microsoft/e/mjghTazu5h After lunch, there will be an Assume meeting: https://tdejong.com/ASSUME/ Best regards, Paul -- Prospects for formalizing the theory of weak infinite-dimensional categories Emily Riehl (Johns Hopkins University) Over the past several years, mathematicians have launched increasingly ambitious computer formalization projects targeting increasingly complex areas of mathematics. This talk will present a high level case study involving ∞-category theory. A peculiarity of the ∞-categories literature is that proofs are often written without reference to a concrete definition of the concept of an ∞-category, a practice that creates an impediment to formalization. We describe three broad strategies that would make ∞-category theory formalizable, which may be described as “analytic,” “axiomatic,” and “synthetic.” We then highlight two parallel ongoing collaborative efforts to formalize ∞-category theory in two different proof assistants: the “axiomatic” theory in Lean and the “synthetic” theory in Rzk. We show some sample formalized proofs to highlight the advantages and drawbacks of each approach and explain how you could contribute to this effort. You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>

1 0

Lawvere's characterization of adjunctions
by Uwe Egbert Wolter 23 Jun '25

23 Jun '25

Dear all, What reference you would recommend for Lawvere's characterization of adjunctions by means comma categories? Best regards, Uwe You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>

3 2

Vietoris locale construction: proof of preservation of compactness
by Townsend, Christopher (Leonardo, UK) 19 Jun '25

19 Jun '25

[Cross post from Math overflow.] Let X be a locale. Then there is the Vietoris locale construction, V, introduced by Johnstone (it's in Stone Spaces, but see also the 1985 paper, 'Vietoris Locales and Localic Semilattices'). The functor V:Loc→Loc is something like taking the locale of all finite sublocales; e.g., if X is discrete then the points of V(X) are the finite subsets of X. In his 1985 paper Johnstone alludes to the fact that if X is compact then so is V(X). But the proof, which is not explicit in the paper, uses a transfinite induction. I believe there is a much simpler proof, but have not found any references to this in the literature. Does anyone know about this specific result being published in the last 25 years? Thanks, Christopher Leonardo UK Ltd Registered Office: 1 Eagle Place, St James’s, London SW1Y 6AF A company registered in England & Wales. Company no. 02426132 ******************************************************************** This email and any attachments are confidential to the intended recipient and may also be privileged. If you are not the intended recipient please delete it from your system and notify the sender. You should not copy it or use it for any purpose nor disclose or distribute its contents to any other person. ******************************************************************** You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.as…> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>

1 0