Monday, June 12, 2023

Networked Mathematics: small approaches to a big problem










The reason for this blog post is to find easily a presentation of mine that has not been recorded. 

 I have discussed this subject at least three times: once in the Topos Institute internal seminar, once with a physicist friend interested in information theory and mathematics (Simone Severini), and once in a talk for the Brazilian UD (Universal Dependencies) group. 

This last occasion has produced the slide deck at "Networked Mathematics: NLP tools for Better Math", May 2023. 

Now Networked Mathematics is a big problem. I have discussed it in several blog posts in the Topos blog, namely:

1.  Introducing the MathFoldr Project 

2. The many facets of Networked Mathematics

3. Mathematical concepts: how do you recognize them? 

4. Preparing for Networked Mathematics 

One of our partial approaches for solving the problem is the idea of recognizing and extracting mathematical concepts from text. That means using NLP technologies for the specific domain of Mathematics. 

But I have been working on other, related solutions to the problem, discussed in the presentation above. I hope to write more about these other solutions soon. 

For the time being I leave you with an interesting, old blog post about another problem that has not been solved, so far: Connecting The Dots: Lessons in Rebellion From the Math Network

Now, because this reminded me of the Math Genealogy, I cannot resist posting this other picture. Of course there are several ways to connect a mathematician to Paul Erdős and some are nicer than others. For many years the AMS tool gave me as my shortest connection to Erdős the one via Vaughan Pratt and Frances Yao. Now it is given me the one below, which I think it is even nicer.

Monday, March 13, 2023

Women in Logic: the history so far

First appeared in the Topos Institute blog, March 6th, 2023

Women in Logic
Picture from

This year we’re having the 7th Women in Logic (WiL) Workshop in Rome, associated with FSCD and CADE. Considering that we never had grants to help us defray costs of the workshop, I think getting to our seventh anniversary is a big milestone. Everyone who works for Women in Logic does it for free and because they find the cause important. You may be wondering, “what is Women in Logic?”

Women, like some other demographics groups, are very badly represented in STEM (Science, Technology, Engineering and Mathematics) subjects. While on paper we have the right to be part of our STEM communities, in reality the obstacles are very strong and sometimes even insurmountable for women participation in Academia. The infamous “glass ceiling” is still very much with us and many of our colleagues do not notice it. (ha, this is why it’s called a “glass” ceiling, right?) Even the colleagues that are notionally aware of the issues, many times do not see them, when they happen in their own lives. The sexism in STEM is systemic and entrenched, it affects both men and women. And it is not a small action like WiL that will defeat it, but WiL does help, a little, to shed some light on some of the issues.

Women in Logic (WiL) started for me in 2013, when Orna Kupferman, who was the Program Chair of LICS that year, presented her LICS chair findings and showed this slide:

Statistics concerning women at LiCS

Until then, while I knew about all the prevalent sexism in society, (it’s hard to ignore the many manifestations, from murdered women to silenced ones) I thought that my community was a bit better than most. My colleagues seemed to me more helpful and more enlightened. Thus when I saw the numbers, it was a shock: how come there were no awards for women? How come there were no women on the advisory board? how come only 3.7% of the submissions in 2013 were by women? It all did seem TERRIBLE!

Much more disturbing was the discovery that, despite many efforts, things were not getting better, they were even getting worse! A representative graph was provided by the AAUW (American Association of University Women) in their report entitled “Solving the Equation”, 159 pages of dismaying facts. As you can see below, while the numbers of women in Mathematics and Computer Science improved from 1960 till around 1990, from then on they dropped, being in 2013 lower than they were in 1960! Engineering, traditionally considered one of the worst areas for women, at least has increasing numbers, but from 9% in 1990 to 12% in 2013. This is a minuscule improvement, leading to, in general, the prediction that at the current rate of progress, the pay gap will not close until 2111.

A graph of women in selected STEM occupations

So I started to think about how to do something about this sad state of affairs. Three years later, at LICS2016, Nat Shankar asked me if I wanted to say a few words about LICS and I said I’d love to, but he might not be pleased with what I had to say. Having talked about how bad things were in the LICS community, I decided to organize the first Women in Logic Workshop, which happened as an associated workshop to LICS in Reykjavik, Iceland the next year. It was easy to find several friends who wanted to do this too, so our collective was formed.

Since then the Workshop has occurred in Oxford 2018 (UK), Vancouver 2019 (CA), Paris 2020 (online), Rome 2021 (online) and Haifa, 2022 (Israel). By most accounts the workshops have been very successful. The invited speakers, so far always two in each workshop, have been excellent and they showcased many different facets of logic in computing, mathematics and philosophy: from Software Engineering to Automated Reasoning to Computational Biology and Artificial Intelligence.

We have received some small grants from the Special Interest Group of the ACM for Logic (SIGLOG), the Vienna Center for Logic and Algorithms (VCLA), the Institute of Logic, Language and Computation of the University of Amsterdam (ILLC).These allowed us to help students and young researchers attend our workshop. We also had some donations to help us to organize dinners after the workshop in Oxford and Haifa, from Prof Ursula Martin (EPSRC and Wadham College) and from Microsoft Outreach, via Nikolaj Bjorner, to whom we’re also very grateful.

Alexandra Silva speaking at the Haifa 2022 workshop
Dinner at Haifa, 2022, with Alexandra Silva speaking

Most recently we have also received important clerical support from the Topos Institute, to process these smaller grants. More substantial effort from the Topos Institute came in the shape of the help to establish a Women in Logic website. Producing this website has been an important step to consolidate the several activities of the collective. Many thanks are due to, especially Juliet Szatko and Tim Hosgood, for all the help provided!

After the worst (we hope) of the COVID19 pandemic, we are now in the process of restructuring and rethinking how to make the collective Women in Logic more efficient. We have several social media channels, managed by several members of the original group. So we are present on the web (Women in Logic), on Facebook (Women on Logic group), on Twitter ([@WomeninLogic1]( and on Slack ( We also have our blog ( and a YouTube channel, which we haven’t, as yet, populated much. Instead we have, so far, collected already recorded talks by women in logic and posted them on our GitHub (

But much remains to be done and we want to count on all of you, women in STEM and allies, to help change the terrible state that we still find ourselves in. Because as we know is not

Nature or nurture? No, it’s bias

Research shows that there is no inherent difference in math and science capability between girls and boys. It’s also a myth that girls aren’t interested in science: In elementary, middle, and high school, girls and boys take math and science courses in roughly equal numbers, except in engineering and AP computer science, according to the National Science Foundation. One study found that the apparent gender gap in mathematics is smaller in countries with greater gender equality, suggesting that gender differences in math are largely due to cultural and environmental factors, not ability.

 The STEM Gap, Why it Matters?

So join us, let us make a difference together!

Group photo at the Haifa 2022 workshop

Thursday, February 2, 2023

The road to Networked Mathematics


The map of mathematics

Networked mathematics is one of my main projects at the Topos Institute (the other is Dialectica categories and its extended family of formalisms). We have not had much luck getting the funding agencies to pay attention to it, yet. But the work is progressing, albeit slowly.

Brendan and I discussed some initial ideas in the blog post Introducing the MathFoldr Project. Then I updated some of the previous ideas in the blog post The many facets of Networked Mathematics, as we consider MathFoldr a key component of Networked Mathematics.

We have been working on the suggestion that formalized mathematics will eventually be one of the main ways of producing mathematics. It seems sensible to believe that proof assistants will become really useful tools for mathematicians, and if so, formalized math will become the usual practice, not the exception.

The logo for the Hausdorff Institute of Mathematics trimester on formalized mathematics

To discuss the issues of formalized mathematics and to prepare for the Hausdorff Institute of Mathematics trimester on “Prospects of Formal Mathematics” in 2024 we have had in the Topos Colloquium talks by several people involved with proof assistants and automated deduction.

July 2021

We started with Larry Paulson on Formalising Contemporary Mathematics in Simple Type Theory. A recent talk by Larry, Formalised Mathematics: Obstacles and Achievements might be a better introduction to his research as far as mathematical formalization in Isabelle is concerned.

The Isabelle logo

I worked for Larry as a postdoc in the Computer Lab, Cambridge University many moons ago, which is possibly the reason I am so fascinated by formalized mathematics. His blog, Machine Logic is super interesting and I always loved the idea that Isabelle was not conceived as a single logic, but as a generic logical framework, and it can represent reasoning in several different systems. (Together with Sara Kalvala I did some small experiments in Linear Logic in Isabelle.) I still want to develop the ideas of a project I wrote with Larry and Prof Roger Needham on modal logics for authentication and privacy, but it is getting late.

The vast library of mathematical results in Isabelle is called AFP, the Archive of Formal Proofs, or as they say, more precisely: A vast collection of Isabelle examples and applications is available from the Archive of Formal Proofs.

August 2021

We had Kevin Buzzard talking to us about What is the point of Lean’s maths library? Kevin’s style of online demo and talk was a huge success with the audience of applied category theorists, which helped to consolidate my ability to invite other speakers not exactly categorically minded. Kevin has this awesome sentence on his website:

“I believe that computers will be able to help humans with proofs within my lifetime, and I am actively trying to make this happen sooner by (a) helping to build a database of modern mathematical theorems and definitions and (b) trying to teach mathematics undergraduates how to use the software.”

Inspiring stuff!

September 2021

We had Florian Rabe talking about MMT: A UniFormal Approach to Knowledge Representation. Florian is interested in the more general problem of implementing “a universal framework for the formal representation of knowledge”, not only mathematical knowledge, but also other generic computing systems. His system is described in Florian’s system MMT has been in development since 2006 and he has worked with Prof. Dr. Michael Kohlhase in several versions of knowledge management at KWARC, Erlangen, Germany. One of Florian’s main goals is to obtain foundation-independent mechanized results, thus much effort is spent on languages and meta-languages. (I also worked with Florian and other colleagues on extending the Curry-Howard correspondence to Goguen’s institutions a long time ago.)

November 2021

We had Jeremy Avigad talking about Formal mathematics, dependent type theory, and the Topos Institute and Lean. This was similar in some ways to Buzzard’s talk, but coming from a more philosophical perspective, was easier to understand. As Avigad says “Formal mathematics is finally getting some recognition” and the press is ready to acknowledge the big pull of the area. Recent good press exemplified by Quanta: “Building the mathematical library of the future” (2020). Also at Quanta “At the Math Olympiad, computers prepare to go for the gold” (2021), and in Nature “Mathematicians welcome computer-assisted proof in ‘grand unification’ theory”" (2021).

The Lean logo

June 2022

Christoph Benzmueller talked to us about Logico-pluralistic exploration of foundational theories with computers. Chris discussed his work on formalization of logic, particularly in formalizing computational metaphysics (instead of mathematics) with collaborators, including Dana Scott, Topos’ senior advisor. Personally I am very interested in Chris’ work on modal logic, also in the benchmarking of modal theorems, less so in God’s ontological existence arguments.

July 2022

Josef Urban talked about Combining learning and deduction over formal math corpora and his work on combining deep learning with automated deduction. Josef, unlike many others, has an agnostic attitude to the different logical foundations and merits of different provers and implementations, so it’s interesting to discuss those kinds of issues with him.

September 2022

Jacques Carette talked to us about What I learned from formalizing Category Theory in Agda, which was particularly interesting to me, as together with Eric Bond and Charlotte Aten I wanted to implement dialectica categories in Agda.

September also had Johan Commelin talking to us about Breaking the one-mind-barrier in mathematics using formal verification. Johan is doing impressive work on formalization of extremely recent work (2020) in Mathematics, the Tensor Liquid Experiment, of Peter Scholze. (if this sounds a bit like a band name, well, it is.)

October 2022

We had Angeliki Koutsoukou Argyraki talking about the Project Alexandria in Cambridge (the one on mathematical knowledge, not the Microsoft one on business knowledge). Her talk was entitled The new era of formalised mathematics and the ALEXANDRIA Project. This was very exciting because the project has a strong component in the direction we are working, that is the direction to do with mathematical language. Mathematical English poses special challenges for NLP (Natural Language Processing) tools.

An engraving of the library of Alexandria

And also in October we had Richard Zanibbi, in the most relevant talk for the directions we’re aiming at with Networked Mathematics. Richard talked about Mathematical Information Retrieval: Searching with Formulas and Text. His project MathSeer and the several demos he showed us were wonderful!

November 2022

We had Gilles Dowek talking about Dedukti in From the Universality of Mathematical Truth to the Interoperability of Proof Systems. Dedukti emphasizes the importance of rewriting in proofs. Gilles’ talk made a series of important points, and it reminded me of other work I’m doing with Luiz Carlos Pereira and Elaine Pimentel on Ecumenical Systems, based on an idea of Dag Prawitz.

So slowly, but surely we’re investigating the issues of formalization of mathematics, as well as its affordances. I hope we will continue to do so in the near future, as there are many loose ends that need tying up.

  • Goguen, J.A., Mossakowski, T., De Paiva, V., Rabe, F. and Schröder, L., 2007. An Institutional View on Categorical Logic. Int. J. Softw. Informatics, 1(1), pp.129-152.
  • E Pimentel, LC Pereira, V de Paiva,2021, An ecumenical notion of entailment, Synthese 198 (22), 5391-541.

Saturday, December 24, 2022

Dialectica Categories in Computing


In the first half of the year we had an AMS Mathematical Research Community (MRC) on Applied Category Theory, in Beaver Hollow, NY. John Baez blogged about it in “Learn Applied Category Theory!” Here’s a poster advertising the whole program.

The AMS poster for MRCs

We also had a paper in the Notices of American Mathematical Society, describing our proposal:

Applied Category Theory in Chemistry, Computing, and Social Networks John Baez, Simon Cho, Daniel Cicala, Nina Otter, and Valeria de Paiva.

An MRC is a bit like a version “on steroids” of the ACT Adjoint School, as there are many more researchers in a research subgroup in the MRC than in a Adjoint School group. While my ACT Adjoint School group had four students and a TA, my MRC group had thirteen researchers. So from four to thirteen people you have more than three times the number of people to do interesting research with. Plenty of fun, but it can be unsettling to think about research problems for so many people you don’t know, especially for me (well, I haven’t had that much experience directing other people’s research).

I was very worried to begin with, but when we got going, it was exhilarating. Great fun to discuss serious math problems with people interested in similar problems, with similar tastes to yours and with plenty of ideas of their own. The program had three mentors (John, Nina and myself), and I ended up with a group of 13, subdivided into 4 smaller groups. Things were going very well (you can check some of the discussions in the Zulip channel [practice:Dialectica]) until two days before the meeting in upper New York state I got ill, and ended up in the ER in the Stanford hospital. Twice.

I couldn’t go to the research meeting in Beaver Hollow, but Jérémie Koenig, my trusted deputy, managed to get everyone working well together into the four groups we had established before:

  1. Dialectica and Polynomials,
  2. Dialectica and Games,
  3. Dialectica and Lenses,
  4. Dialectica Petri net Processes.

They sent me a lovely picture from Beaver Hollow.

The MRC group on ACT in Beaver Hollow

The neat thing about MRCs is that they give the participants some funds to make academic visits and I was very touched when my group decided to come and visit me in California, using their funds. This meant that we had another smaller meeting in Cupertino, in the middle of the Summer. Well, it was already September and usually the weather over here is good most of the time, but we had some bad luck, and this week was a heatwave, the worst one this summer. But we had some fun. Now the problem is reworking what happened in the many discussions.

A third component of the MRC program is still to come. Of course we all hope that the math we discussed during the summer will mature nicely into preprints and papers and programs, and these are supposed to be presented in the AMS Joint Mathematics Meetings (JMM) in Boston in early January. So one organizer was chosen from each mentor’s group and I am very happy that Charlotte Aten accepted to be the organizer for our group, despite being in the last weeks of her PhD and interviewing for jobs. Then sometime in September we were told everyone needed to write up some ideas that they hoped could make solid papers before January 2023. I’m glad to report that every one of our four subgroups was able to produce an abstract and I hope the papers are in the process of being written as I write this.

Now this post was meant to be about the four subgroups above and why I am so excited for the mathematics we’re doing. But I am a bit behind with my processing of the knowledge we shared when people visited here (and over Zulip!). So, while I could possibly wait for the JMM to get to grips with more of the new math that people are producing, I think I will try to explain, at least a little, how the themes above interact.

I started my research career working on Gödel’s Dialectica Interpretation. On bad days I think not only have I never left the dialectica, but even today I hardly understand the stuff, after all these many years. Then I console myself with the thought that the stuff is really fascinating and full of surprising consequences and applications!

Someone else who’s awed by the Dialectica Interpretation is Jules Hedges. His blog post Lenses for Philosophers shows some of the badly understood consequences and connections of the work on categorical dialectica construction. In some ways the MRC Dialectica categories for Computing is an attempt to clarify some of the interrelations described in Hedges’ post.

Gödel’s Dialectica Interpretation is a proof interpretation of intuitionistic arithmetic into a quantifier-free theory of functionals of finite type, called System T.

The interpretation’s original use was to show the consistency of Heyting (or intuitionistic) arithmetic. When combined with Gödel’s double-negation interpretation, which reduces classical arithmetic to intuitionistic arithmetic, the Dialectica interpretation yields a reduction of the classical theory as well.

As explained by Fernando Ferreira,

The stated purpose of Gödel’s Dialectica paper is to present a consistency proof of first-order Peano arithmetic PA by way of an extension of the finitary viewpoint according to which the requirement that constructions must be of and over “concrete” objects is relaxed to be of and over certain abstracta, namely computable functionals of finite type over the natural numbers.

Thus the Dialectica interpretation can be considered a relaxed (or liberalized) form of Hilbert’s program, where instead of insisting on the finitary viewpoint, we accept ‘computable functionals of finite type’ as (sort-of) concrete objects. To understand the interpretation itself, I recommend A.S. Troelstra’s “Introductory Note to the Dialectica paper” in Gödel’s Collected works, volume II, where we can read that “Gödel presents his results as a contribution to a liberalized version of Hilbert’s program: to justify classical systems, in particular arithmetic, in terms of notions as intuitively clear as possible.” From there one can graduate to more complete work of Troelstra himself (Metamathematical investigation of intuitionistic arithmetic and analysis (1973)), of Avigad and Feferman (Godel’s Functional (“Dialectica”) Interpretation) and of Kohlenbach and his school.

The categorical internal versions of the Dialectica construction, starting in de Paiva’s thesis in 1988 (out as a technical report in 1991), have spelled out some of the requirements and consequences of the interpretation, especially its connection to Linear Logic. The categorical dialectica construction was generalized to fibrations, by Hyland (2002), Biering (2008) and Hofstra (2011). Generalizations to dependent type theories appeared in van Glehn (2016) and Moss (2018) and then together (2018). More recently Trotta et al, building on this work introduced Gödel fibrations and Gödel doctrines, rekindling the connections of the categorical dialectica construction to logic and making sure that the three dialectica principles (Independence of Premise, Markov Principle and Axiom of Choice) get their categorical explanation.

Some members of the MRC group

The main connections of the Dialectica construction discussed in the MRC, as anticipated above, are between ‘lenses’ and dialectica categories, between ‘polynomials’ and dialectica categories (see Nelson Niu’s blog post and Sean Moss’ talk), between ‘games’ and dialectica categories (already hinted at in Blass’ original paper on games for linear logic) and between concurrency theories and dialectica categories in the shape of Dialectica Petri nets Processes and their implementation in Agda. I hope the abstracts for the extended discussions of these four sets of connections will be available soon.

But it is clear that we’re only scratching the surface of this rich story of interconnections. Hopefully much more will come to light in the near future.

Extracting Mathematical Concepts

by Valeria de Paiva , Jacob Collard originally posted Wednesday, 16 Nov 2022

Categories: [research]
Tags: [AI] , [NLP] , [MathFoldr]

Humans are very good at recognizing the words they do not know, the concepts they haven’t met yet. To help with these they invented dictionaries, glossaries, encyclopedias, wikipedias, crib sheets, etc. Initially, they did it via laborious manual work, more recently through automated construction techniques. Natural language processing (NLP) tools have improved impressively in the last decade. Most of this incredible improvement happened to newspaper text and hence named entities of the kind found in news text can be detected and classified (usually into people, organizations, places and dates) with much greater accuracy than in the recent past.

Samuel Johnson
Dr Johnson, the author of the 1755 A Dictionary of the English Language.

However, for domain specific text, like the academic literature in different sciences (e.g. Medicine, Biology, Chemistry), or in the Humanities (History, Sociology, Philosophy, etc.) things are more complicated. Thus extracting technical terms/concepts from papers is important, interesting and usually difficult.

How do you detect mathematical concepts in text? As a human mathematician (or not), you probably recognize that the ovals in the snippet in this picture correspond to mathematical concepts. But there is some uncertainty in this choice, and several metrics might be used to decide whether the automated system used is getting it right or not.

An example of term extraction on a single paragraph of text

We wanted to see how well ‘automatic term extractors’ (ATE) systems work for mathematical text, especially for Category Theory, if we simply use them out-the-box. It seems reasonable to establish baselines using available, open source systems and this is what we do in our paper “Extracting Mathematical Concepts from Text”. The paper was presented at the 8th Workshop on Noisy User-generated Text (W-NUT) at Coling 2022 and you can find a short, technical video describing the work below.

This work is part of a larger project on Networked Mathematics that we started describing in “Introducing the MathFoldr Project” and broadened the discussion in “The many facets of Networked Mathematics”. We hope to provide more information on the project soon.

Thursday, December 1, 2022

Networked Mathematics


The many facets of Networked Mathematics

by Valeria de PaivaMonday, 18 Apr 2022

Categories: [research]
Tags: [MathFoldr] , [AI] , [NLP]

Last year we started a discussion on the production of mathematics, the pre-industrial kind of process that we all still follow of solving problems and taking the solutions to the market of ideas (conferences, seminars, blog posts, twitter, coffee breaks in the department, etc.) as drafts/preprints/submissions and all the difficulties that this process involves. In particular we discussed the difficulties of checking whether the work had been done before or not, and the difficulties of searching for other, similar work that might help us with a given question.

As a group we settle on a path of trying to apply the new tools of NLP and knowledge representation (neural nets, word embeddings, transformers, ontologies, semantic web tools, etc.) to what might be called mathematical English. We reasoned that, yes eventually we will need to get to the semantics of equations and diagrams, but it would be useful to know how much we can learn simply from using the tools of NLP to extract mathematical concepts from abstracts of articles.

We also decided that Category Theory would be our prototype domain. First because category theory is about the organization of Mathematics in general, discovering the backbones of the subject and the hidden similarities between, in principle, unrelated sub-areas. But secondly because we are category theorists, after all. So this is the domain in which we are domain experts.

We realized early on that corpora of mathematical text were needed, and we hoped this wouldn’t be a problem. Category theory was, after all, one of the first areas of Mathematics to have a free open-source journal, namely TAC (Theory and Applications of Categories) in 1995. But we need much more data than simply one journal. While we also have both the nLab and the whole of the Wikipedia Math Portal, as beautiful mathematical open resources,  even the licensing of the arXiv is more problematic than we knew.

As we explained in the earlier blog post, we have chosen to work with a corpus of TAC abstracts and one (snapshot) of the nLab from the beginning of 2021. The TAC abstracts are clean, with not so much LaTex thrown in, and form a small corpus of 3.2K sentences. The nLab is a bit more noisy, one needs to remove the wiki markup and sections and headings get lost, a traditional nightmare of processing scientific text.

We now have spaCy processing of all this data, as well as a collection of experiments on term extraction, using different tools: TextRank, OpenTapioca, DyGIE++ and Parmenides, a special tool of our NIST collaborators. There are plenty of interesting observations to make about the processing and the comparison between these tools, and we are preparing have now a write-up about it. However, the major problem with domain specific NLP strikes again: we have no golden standard for mathematical concepts in mathematical texts, much less for category theory concepts. Our predicament is not only ours: many others have the same issue and have tried to make do with not guaranteed good results. 

Meanwhile, we have been working on the idea that formalized mathematics will eventually be the way of producing mathematics, which is a new kettle of fish altogether. To discuss the issues of formalization (somewhat an eventual goal) we have had in the Topos Colloquium talks by several people involved with automated deduction: Jeremy Avigad, Kevin Buzzard, Larry Paulson, Florian Rabe, for example. We hope to have more talks this year. Finally, we’re happy to be helping to organize a Hausdorff Institute of Mathematics trimester on “Prospects of Formal Mathematics” in 2024.

The poster for the Prospects of formal mathematics trimester program
The “Prospects of formal mathematics” trimester program will run at the Hausdorff Institute of Mathematics from the 6th of May to the 16th of August 2024.

Wednesday, November 30, 2022

Women in Logic website

 If there is anything the internet has shown me, it is that repetition is useful. More duplication of posts from the Topos Institute blog.

Women in Logic website launched

by Valeria de PaivaThursday, 17 Mar 2022

Categories: [announcement]
Tags: [logic]

World Logic Day is an international day proclaimed by UNESCO in association with the International Council for Philosophy and Human Sciences (CIPSH) in 2019. The idea is to celebrate it on the 14th of January every year.

Last year we celebrated Logic Day. Not this Logic:

Logic (the rapper)

but more like the Logic of the ideas described below:

Logic (mathematical)
Also logic.

This year we decided to celebrate Logic Day by launching the 

 Women in Logic website:

Women in Logic (WiL) is a collective of women working in logic, as well as a forum that brings together women conducting research in logic and closely related areas, with the goals of enhancing the experience of women in these communities, making their achievements known, and increasing the number of women in logic.

The WiL website
The new Women in Logic website!

The flagship activity of the collective is the Women in Logic workshop that has happened every year since 2017. This workshop is usually associated with one of the big conferences in logic for Computer Science, so either FLoC (Federated Logic conference), LiCS (Logic in Computer Science) or FSCD (Conference on Formal Structures for Computation and Deduction), so far. The workshop has happened in Reykjavík (Iceland), Oxford (UK), Vancouver (Canada), Paris (online due to covid) and Rome (online due to covid). The next workshop should be happening happened in Haifa, Israel, as part of FLoC, on July 31st, 2022.

Women are chronically underrepresented in the Logic communities in Computer Science, in Philosophy, in Cognitive Science and in Mathematics; consequently they sometimes feel both conspicuous and isolated, and hence there is a risk that the under-representation is self-perpetuating. The WiL workshops provide an opportunity for women to increase awareness of one another and one another’s work, to combat the feelings of isolation. It provides an environment where women can present to an audience comprising mostly women, replicating the experience that most men have at most CS meetings, and lowering the stress of the occasion; we hope that this will be particularly attractive to early-career women.

The workshop Women in Logic (WiL) is supported by small grants provided by ACM’s SIGLOG, the Vienna Center for Logic and Algorithms, the Institute of Logic, Language and Computation of the University of Amsterdam and the Topos Institute. Thank you friends!!