Partial Compilers and Problems

 

A compiler does not always have to do everything in one go.

A compiler pass might take a program, simplify it, lower it to another representation, split a computation between machines, or choose a different representation — and then hand the result to another compiler. The second compiler does another piece of the job, and eventually something produces the final target program. This is the idea behind a partial compiler.

But there is an interesting question that the usual description leaves out:

How do we know that a compiler pass has not introduced an error?

There is a surprisingly simple answer. Put back something that the original definition threw away.

A compiler that leaves the job unfinished

A partial compiler takes a source program and produces a reduced source program. But it also has to remember enough information to put the final answer back together.

Schematically, we can think of a partial compiler as having two parts:

• a way to reduce the source;

• a way to assemble the final target from the original source and whatever comes back from the next compiler.

The second part is important. If I take something out of a program in the first pass, I may need the original program again when I assemble the final result.

This is exactly the shape studied by Budiu, Galenson and Plotkin in their work on the Compiler Forest. Partial compilers can be composed: one pass hands its reduced program to the next, and the results are assembled in the reverse order. There is already a beautiful mathematical structure here. Partial compilers form a category. And there is an even older mathematical structure hiding underneath.

This looks  like Dialectica

In the Dialectica interpretation, an object consists roughly of two kinds of things:

witnesses and counterexamples.

A witness is proposed evidence that something is true. A counterexample is a challenge to that evidence.

A Dialectica morphism has exactly the same two pieces of data as a partial compiler:

• something going forward, turning one witness into another;

• something going backward, turning a challenge to the output into a challenge to the input.

The backward map is allowed to depend on the original witness. This is precisely what a partial compiler needs when it has to remember the source while reconstructing the target. So a partial compiler is not merely similar to a Dialectica morphism.

It is a Dialectica morphism with one important thing missing: the relation.

This identification is not new.  The authors of the Compiler Forest work themselves connect their construction with Dialectica through Blass's questions and answers and Milner's tactics. I also pointed it out in a talk on partial compilers and Dialectica spaces in 2011.

What is interesting and new is what happens when we stop throwing the relation away.

Put the counterexamples back

Suppose that for every source program S and target program T we have a relation saying that T is a bad implementation of S. Then a compiler pass is correct when it respects that relation. What does that mean?

Suppose the pass turns S into a smaller source f(S). Later, another compiler produces a target for f(S), and our pass uses that target to assemble a final target T for S. If T is wrong for S, then the target that came back from the next compiler must already have been wrong for f(S).

In other words: the pass itself has introduced no new errors.

That is exactly the Dialectica morphism condition, once we read the relation as a relation of refutations rather than as a relation saying that something is correct. And this gives a rather pleasant interpretation of the categorical composition.

A stack of compiler passes does not need a new correctness proof for the composite. Instead, take the specification at the end and push it backwards through the passes, one pass at a time. The specification that arrives at one pass tells us exactly what that pass has to guarantee.

This is a weakest-precondition calculation, but with the program running in two directions: witnesses move forward and counterexamples move backward.

Why "counterexample" rather than "correctness"?

There is a small but important subtlety here. One could have defined the relation the other way around: perhaps α(S,T) says that T is a correct implementation of S.

But then the direction of the Dialectica condition is wrong for what we want from a compiler. The useful reading is asymmetric:

the source is what we are trying to implement; the target is what can refute the implementation.

That is why counterexamples travel backwards. There is something rather satisfying about this. Correctness is not extra information that a compiler has to carry around. The compiler already has its two pieces of data.

The relation is a specification against which those pieces can be checked. A compiler either satisfies it or it doesn't.

Something unexpected happens: copying

Once we have the relation back, we can ask questions that are difficult to see in the original compiler description. One of them is:

Can a compiler duplicate its source?

This turns out not to be a question about the source. It is a question about the target type.

To copy something in the Dialectica category, the target has to know how to combine two copies into one. In mathematical language, it needs a suitable commutative monoid structure.

This makes visible the reason for a phenomenon reported in the Compiler Forest work. If compile-time effects are moved inside the construction, one might expect to get another category. But composition is no longer associative.

The Dialectica analysis explains why. The source appears in both the reduction and the generation part of a partial compiler. In effect, it is being used twice. Copying is free in a cartesian world.

It is not free in general.

The target type has to be able to absorb those two copies. A single outer monad can restore the situation because it keeps the effect outside this copying problem. So a categorical question about whether composition is associative turns out to have a very concrete interpretation:

Can this kind of target be copied?

What about cost?

The same construction also lets us replace ordinary truth values by quantitative ones. Instead of saying simply

this target is a counterexample

we can assign a value measuring how bad it is.

For example, the value might represent:

• size,
• running time,
• register pressure,
• or another resource.

The natural example is the Lawvere quantale, where the monoidal operation is addition. Then the Dialectica relation becomes a kind of cost model.

A compiler pass may add cost, but it cannot magically make the cost disappear. And, just as before, specifications can be pushed backwards through a stack of compiler passes.

There is another nice coincidence here.

When a compiler is lifted from individual sources to lists of sources, the specification for a list can be obtained simply by combining the specifications of its elements.

For costs, that means adding them. So the same mathematical operation — the monoidal structure — appears on opposite sides of the relation. On the target side, it describes how targets can be assembled or copied. On the specification side, it describes how costs can be aggregated.

From verified compilers to a type of verified compilers

There is one more step that I find particularly intriguing.

Suppose we do not want to say merely that a compiler has a specification. We want to restrict its source type to the sources for which the specification is actually satisfied. Then we are no longer talking about a class of programs carrying a side condition. We are constructing a new object consisting only of the sources that meet the condition.

In categorical language, this is a comprehension construction, and in the paper it leads to a proposed object of verified partial compilers. The idea is that the verified compilers themselves should form a type. There is even a natural adjunction suggested by this construction: a function-space-like object of verified partial compilers should be right adjoint to product with the source problem.

What I like about this story

The original partial compilers were motivated by a very concrete problem: compiling programs in stages and assembling the pieces later.

The mathematical construction reveals that the same pattern occurs in several places. A problem can be reduced to another problem and a solution can be assembled from a solution of the reduced problem. That is Kolmogorov's interpretation of intuitionistic logic as a calculus of problems. It is also the shape of Milner's tactics: reduce a goal to subgoals, then assemble a proof from their solutions. And it is the shape of a partial compiler.

Dialectica categories provide a common mathematical language for all of these.

The striking point for me is not that we can redescribe compilers categorically. It is that restoring the relation gives us things that were invisible when the relation was discarded:

1. correctness,
2. a criterion for copying,
3. quantitative cost,
4. and potentially a type of verified partial compilers.

None of this requires changing the compiler. The passes are the same passes. The composition is the same composition. The extra ingredient is simply the relation that says what counts as a counterexample.

So perhaps the moral is a very small one:

Sometimes the most useful information is precisely the information that was thrown away.

But another useful one is the (not-quite-ready) preprint. 

 

Polynomials with Predicate: a Dialectica reading

I have just put up a new preprint, Polynomials with Predicates: a Dialectica Reading. It started from a fairly simple observation: if you take a Dialectica object and forget its predicate, what remains looks very much like a polynomial.

But the more I looked at the comparison, the more I thought the interesting story was actually the other way around.

Polynomial functors give us a useful language for seeing the shape of structures that Dialectica has been carrying for a long time. They do not replace the Dialectica construction, because they forget precisely the part that makes it logical: the predicate saying which witnesses withstand which challenges.

And the comparison becomes particularly interesting when we look at dependence and sequencing.

Witnesses, challenges, and shape

A Dialectica object consists of witnesses, challenges, and a relation saying which witness withstands which challenge. There is an obvious interaction pattern here. A witness is chosen; a challenge is presented; and the predicate tells us whether the witness swins the challenge.

If we forget the predicate, the witnesses become the positions of a polynomial and the challenges become its directions. The forward map on witnesses and backward map on challenges are exactly the shape of a polynomial morphism. So a polynomial is, in this sense, the shape of a Dialectica object.

It records who chooses what and what may depend on what. It does not record whether the resulting interaction succeeds. That distinction is important throughout the paper.

 

A familiar collection of connectives

Once we look only at the shape, most of the polynomial operations on monomials line up with Dialectica linear logic connectives. But this is not a correspondence that starts with the recent polynomial literature.

The main Dialectica connectives go back to the original Dialectica construction in the late 1980s. The ordinary tensor, additive conjunction, and implication already appear there, together with their characteristic witness/challenge asymmetry.

Then, in 1993, Blass introduced another tensor in which the challenge to one component may depend on the witness chosen in the other. The pre-existing cross-product of the Girard Dialectica construction gives the corresponding two-sided dependence.

So there is a first chain:

ordinary tensor → Blass tensor → cross product

where the successive steps allow more dependence of challenges on witnesses. But there is another chain, going in the opposite direction. Instead of making challenges depend on witnesses, we can make witnesses depend on challenges:

ordinary tensor → ◁ → par.

The middle operation is the one I want to emphasize. The two chains are not independent: linear negation swaps witnesses and challenges, so it swaps the chains term by term, and ◁ is the dual of Blass's tensor — which is how one could have known the connective was there before anyone wrote it down.

 

Sequencing is not new

The operation ◁ says that the witness for the second component may be chosen in response to a challenge to the first. In plain language:

first play A, see how A is challenged, and then choose how to play B.

This is precisely the sort of dependence one expects from sequential composition. But I want to stress something that could easily be obscured by the polynomial terminology.

This sequential understanding is not new in this paper.

The sequential construction already appeared in the Dialectica models of state, and in particular in my 2014 paper Linear Logic Model of State Revisited. The sequential modality and the distinction between parallel and sequential use were already there.

The present paper is not discovering sequencing by looking at polynomial substitution. Rather, polynomial substitution gives us a particularly clean way of recognizing the shape of a sequential Dialectica connective that was already present.

This is one reason I like the comparison. It tells us that the polynomial operation is not the source of the logical idea. The logical idea was already there; the polynomial viewpoint makes its shape easier to see.

The history of ordered contexts is older still

There is another piece of history that belongs here. The ordered-context story is not something that has been invented to justify the current categorical terminology either. The relevant orders are the series-parallel orders: start with a point, combine things side by side, and combine things in sequence. The work of Béchet, de Groote and Retoré in 1997 gives the relevant axiomatization of the inclusion between these orders. 

This matters because the later categorical picture is not introducing an arbitrary notion of “before”. There is already a well-understood combinatorial structure behind the ordered contexts. The linear-logic models of state paper put this order into the logic; the present paper puts the corresponding dependence into the shape of the Dialectica object.

From the two chains to interchange

Once the two tensors are seen together, something rather nice happens. We have the ordinary, parallel tensor and the sequential tensor ◁. There is a natural map from parallel to sequential combination: a witness chosen for the second component independently can simply be regarded as a sequential strategy that ignores the challenge to the first.

More importantly, there is the middle interchange law

(A ◁ B) ⊗ (C ◁ D) → (A ⊗ C) ◁ (B ⊗ D).

In words, two processes that each have an internal order can be run side by side and then resequenced. This is exactly where the series-parallel story comes back in. The point is not that we have discovered yet another useful natural transformation. The point is that the old ordered-context structure tells us that this is the right transformation to look for. Once the two monoidal structures share a unit, the middle interchange contains the other ways of adding order as special cases.

So the categorical statement that the Dialectica construction carries a normal duoidal structure is really organizing several pieces of older logic and category theory into one picture.

Then reuse follows

There is a final consequence that I particularly like. The usual exponential modality ! corresponds to reuse in parallel. Its challenges are finite multisets: the order in which things are reused is irrelevant.

The sequential modality † corresponds to reuse in sequence. Its challenges are words: now order matters. Again, neither of these ideas is new. They already occur in the earlier Dialectica models of state. What the present organization shows is how they fit together.

Because the two tensors are related by the natural map above, the comonoid structure for the ordinary tensor gives a comonoid structure for the sequential tensor as well. In particular:

whatever may be reused in parallel may also be reused in sequence.

What had appeared as another structural requirement in the models of state becomes a consequence of the relationship between the two tensors. That is, for me, the real mathematical payoff of the paper.

So what do polynomials contribute?

Not the logic. Not the predicate. Not the idea of sequencing. What they contribute is a good way of exposing the shape of dependence.

The two chains

challenges depend on witnesses

and

witnesses depend on challenges

make a collection of Dialectica connectives much easier to organize. They also make visible the intermediate operation ◁ and its relationship with polynomial substitution.

But the predicate still matters. Two Dialectica objects can have exactly the same interaction pattern and therefore exactly the same polynomial shape, while differing completely in which witnesses withstand which challenges.

That is why the title of the paper says Polynomials with Predicates. The polynomial tells us the shape.The predicate tells us what that shape means.

And the historical point is worth making explicit: the main Dialectica connectives appeared in 1989; Blass's tensor followed in 1993; the series-parallel analysis appeared in 1997; and the sequential Dialectica construction was already present in 2014. The polynomial viewpoint comes later.

What is new here is not the invention of these structures, but the way of putting these pieces together and seeing the polynomial structure underneath them. For me, that is the useful lesson of the comparison: sometimes a new vocabulary is most valuable not because it gives us a new construction, but because it lets us recognize the structure that was there before.

 

 (Hermann and Marcelo from work on Linear Logic Model of State, 1996)

Natural Language Is Not Going Away

Quite a few weeks ago, my friend Simone Severini sent me a book he wrote with Andrea Borghini, Science, Ltd.: Notes on the Research Enterprise in the Age of Machines. He told me, rather modestly, that they had quoted me in it.

It turns out that they quoted me quite a lot.

The conversations behind the book go back to May 2023, although the message Simone sent me about the finished book arrived in August 2025. Reading the book now was an interesting exercise, because I discovered that I still believe everything that I told him then—and that much of what I have been working on in the intervening years has gone in precisely that direction.

The book is about a large question: how should the scientific enterprise change when machines become capable not simply of calculating things for scientists, but of reading, organizing and connecting scientific knowledge at scales that humans cannot?

One of the problems Simone and Andrea discuss is particularly acute in mathematics. We have millions of papers. We have more mathematics than any individual could possibly read. But the relationships between mathematical ideas are still mostly buried inside those papers, expressed in the language mathematicians use to talk to one another.

This was the context in which they asked me about formalization.

I apparently said:

“My goal is to try to overcome this lack not of data, but of annotations on data when working in mathematics, so that we can explore the scientific literature and understand texts in depth. And we should try to extract as much information as possible with natural language before proceeding with formalization.”

I still think this is right. (annotations here is an euphemism for semantics)

There is a very understandable temptation, when thinking about mathematics and machines, to conclude that the solution is to formalize everything. Formal mathematics is great, and formal proof assistants are becoming extraordinarily powerful.  But formalization requires choices: a formal system, a representation, a particular piece of software, conventions about what is made explicit and what isn't.

Mathematicians themselves don't normally communicate that way. We talk, write papers, draw diagrams, invent terminology, abuse notation, leave things implicit and rely on enormous amounts of shared mathematical culture.

So I also told them:

“When we collaborate, we speak in our language. Moreover, when you decide to formalize something, you have to make a technical choice and adopt a tool that, all of a sudden, might become obsolete as soon as a better formalization is discovered. See programming languages. However, it is unlikely that the use of natural language will become obsolete: it is an excellent tool that has evolved over thousands of years.”

Here, for once in my life, I underestimated a number. (Brazilians are known for exaggerating them!)

Language has been with us for considerably longer than “thousands of years.” Exactly how much longer is a fascinating and disputed question, because spoken language leaves no fossils. Estimates for fully developed human language often reach well beyond 100,000 years, and some researchers argue for a much older origin still.

So perhaps I should have said: natural language is an extraordinarily successful technology that humans have been developing for at least tens of thousands, and very possibly hundreds of thousands, of years. It would be surprising if the arrival of proof assistants and large language models suddenly made it obsolete.

What I wanted instead—and still want—is a good interface between these two worlds.

In the years since those conversations, this has increasingly become, for me, the idea of Network Mathematics: representing mathematical knowledge not as a pile of documents and not as a single enormous formal library, but as an extended knowledge graph connecting the different ways in which mathematics exists.

Some of our work since then has been about trying to build pieces of precisely this bridge. MathGloss tries to identify and align mathematical concepts across resources written for humans and resources intended for machines; more recently, our work on extracting mathematical relations asks whether language models can recover some of the relationships that mathematicians leave implicit in mathematical prose. Concepts are hard enough to identify; relations between them are harder still. But extracting both may give us enough overlapping evidence to begin reconstructing the network that is already there in the literature. 

Definitions, concepts, theorems, examples, papers, informal explanations, formal statements, proofs, databases and libraries should be connected. A mathematical concept appearing in ordinary mathematical English should be able to point toward its occurrence in Wikipedia or Wikidata, toward related concepts, toward its use in papers, and eventually toward one or several formalizations of it. 

 

The point is not to replace informal mathematics by formal mathematics, nor formal mathematics by informal mathematics.

The point is to build the bridges.

 This is why I was particularly pleased to discover that Simone and Andrea return to our conversation later in the book, when they start imagining “science in a graph.” They ask what the vertices of such a graph should be, what language should describe them, and how the connections between them should be represented. Existing scientific databases give us the documents, but most of the interesting conceptual relationships are still hidden inside those documents and recoverable only by readers who already understand the field.

Yes. Exactly.

This is also why the recent explosion of language models seems important to me. If machines are becoming much better at dealing with the language scientists actually use, perhaps we don't have to choose between the enormous human inheritance encoded in natural language and the precision and computational possibilities of formal systems.

We can try to connect them.

Simone and Andrea's book goes much further than mathematics. It asks how publishing, peer review, funding, scientific databases and ultimately the institutions of science might have to change if scientific knowledge becomes genuinely machine-readable and machine-navigable. It is also appropriately suspicious of the idea that simply making science faster automatically makes science better.

But I was delighted to find my 2023 self appearing in their argument.

Especially because, three years later, I would give them essentially the same answer. Despite all the proposals and papers rejected on that. I am stubborn.

Except for the number.

What Is Actually Linear Here?

                                         [Andrea Schalk, Summer 2007, from her webpage]

I have been playing with a very small variation on the Schalk–de Paiva construction (more here) and it has turned into a rather larger question than I expected. The experiment is almost embarrassingly simple:

Take lineale-valued sets, and replace relations by structure-preserving functions.

That is essentially the whole idea behind a new preprint, Functional Lineale-valued Sets.

Why bother? The original construction, usually called FP-Set, is a remarkably uniform way of producing models of linear logic. You take a set, put values from a lineale between its elements, and use relations as morphisms. With suitable choices of the lineale, you get familiar linear logic models  such as phase spaces, coherence spaces, or hypercoherences. Also a whole host of other models that people did not seem to have played much with.

But relations do a lot of the work in the construction. So I wanted to ask a slightly impolite question:

What happens if we take the relations away?

 

In the functional version, an object is still just a set equipped with a lineale-valued notion of similarity. But now a morphism is an ordinary function which preserves that structure. And something rather interesting happens. The linear structure does not disappear. Instead, it becomes much easier to see where it is coming from.

The tensor comes from the lineale. The internal hom comes from residuation. Negation comes from the choice of a dualizing element. Modal structure comes from a storage operator. Even the conditions giving duplicable objects are conditions on the values in the lineale.

In other words, the sets are not providing the linear structure. The lineale is. Most of the structure is "imported" from the codomain, which is a familiar situation in mathematics.

What the functions give us is something different: ordinary categorical structure. Products and coproducts are computed on the underlying sets. Equalizers and coequalizers are available. With a complete lineale, the resulting category is complete and cocomplete.

This is quite different from the relational construction, where the relational notion of morphism is closely tied to the way the structure is built. So the little experiment seems to separate two things which are rather thoroughly entangled in the usual presentation:

the linear structure comes from the values, while the ordinary categorical structure comes from the functions.

This also raises the question of whether there is a linear analogue of the familiar theory of H-sets and Q-sets. For readers who have not met them: an H-set or Q-set is, roughly, a set in which equality is replaced by a degree of similarity. Instead of asking whether two elements are equal, we assign a value measuring how similar, or how equal, they are. These structures grew out of the study in the frame-valued case, and are closely connected with sheaves and topos theory. 

This is precisely why they are tempting here. We already have a lineale supplying values between elements, so why not use those values to describe a linear version of “being the same”? And if the resulting objects behaved like their classical H-set/Q-set counterparts, perhaps we could recover some of the beautiful categorical constructions that come with them.

There is a natural way to do this. The off-diagonal values describe similarity between elements, while the diagonal values describe their extent. One can then write down conditions resembling symmetry, transitivity, boundedness and a local identity condition.

At first sight these conditions look nicely linear. But this is where things get more interesting. When you examine what the conditions actually say, most of the apparently linear behaviour has a rather cartesian origin. The local identity condition, in particular, forces the extents to be idempotent. So there is a curious phenomenon:

the conditions look linear in form, but cartesian structure is hiding in their provenance.

And this seems to matter. The tempting next step would be to imitate the familiar tripos-to-topos story and try to build a topos-like category from these linear H-sets, or LinSets. But the local identity condition gets in the way. The problem is not with the doctrine. For a quantale, the usual powerset construction gives a perfectly good linear analogue of the predicate doctrine, and the Frobenius property obtains. The problem appears when we try to build the objects on top of that doctrine.

In the ordinary H-set story, the predicate itself supplies the identity relation. In the functional linear setting, identities are already ordinary functions, and the lineale-valued predicate does not have to be an identity. Requiring it to play that role introduces precisely the idempotence condition that pushes us back towards the cartesian world.

So at the moment I see several possible ways forward. Perhaps one should develop a genuinely functional version of linear H-sets, accepting that some of the familiar universal properties will have to change. Perhaps there are useful conditions under which functions and functional relations coincide. Or perhaps the moral is more radical: a linear completion should not necessarily be expected to look like a topos.

There is also a nice comparison with Dialectica constructions. In a Dialectica category, we have two sorts of data: witnesses and counterexamples. A map evaluates one against the other in the lineale. Here those two sides have been collapsed into one set. So LinSet can be viewed as an extreme case of the Dialectica idea: there is no longer a separate witness side and counterexample side. There is just the evaluation structure on a single set.

And that small change seems to move the crucial assumptions around.

This is why I am sending this one out as a conversation starter rather than as a finished theory. I would particularly like to hear from people who know the H-set and Q-set literature, people who know the linear logic side, and people who have thought about functional relations and topos constructions.

Have I isolated something useful here, or have I simply moved the difficulty somewhere else?

I would be delighted by either reaction: I want to work on this with you or no, this is wrong, and here is why.

 

Counting LICS again

 

I wish I could be bringing better news.

I have been counting LICS committees again. All the numbers below come from two places, both public. The committees from 1986 to 2025 are on the LICS committee archive page, which lists every program committee, organising committee, advisory board and steering committee since the first meeting in 1986. The 2026 committee is not on that page yet, so I took it from the LICS 2026 call for papers. Forty-one conferences in total.

These are rough first calculations. I counted by hand, and gender is inferred from names and from knowing who these people are, so some entries are judgement rather than data. The earliest committees are listed by initial only, which makes 1986, 1988 and 1989 the least reliable rows. I will be revisiting these numbers and I would be glad of corrections.

Where I give an aggregate it is weighted by committee size: total women's seats over total seats in the period, not the average of the yearly percentages. Committees have grown a great deal over forty years, and averaging percentages would let a committee of fourteen count for as much as a committee of forty-nine.

The whole run - 41 years - in one picture, but other pictures help to see it.

The first twenty-five years

From the first meeting in 1986 until 2011, LICS program committees ran from thirteen to twenty-six people, and the number of women on them ran from zero to four. Seven of those twenty-six years had none at all: 1986, 1987, 1990, 1992, 1994, 2001 and 2004. Pooling the seats rather than averaging the years, women held 7 of 153 in the first decade and 13 of 192 in the second, which is 4.6 and 6.8 per cent. Across the period the figure does not climb so much as wander — a year with two, a year with none, a year with one — in a field perfectly capable of naming women who worked on these topics.

New Orleans 2013

In 2013 Figure 1 shows  the share reaches 34.3 per cent, twelve women on a committee of thirty-five. That is still the highest figure in the whole run, and it comes straight after 24 per cent in 2012.

2013 is the year Orna Kupferman chaired LICS, the first woman ever to do so, twenty-eight years in. It is also the year she stood up at the business meeting and put the numbers on a screen. I have written about that evening before: people were drinking beer and not paying much attention, which is what people do at business meetings, and I had the feeling I was the only one listening. What the slide showed was that no awards had gone to women, that there were no women on the advisory board, and that women had written only 3.7 per cent of that year's submissions.

What I took away from it, sitting there, was that LICS was not merely as bad as any other computer science conference but a good deal worse. I should say plainly that this was my conclusion not  hers. Orna showed the numbers. The reaction is mine, and so is everything I did afterwards. Her slide is in that post. It is worth looking at again.

Something did change after that. Pooling all the program committee seats in a period and asking how many of them women held, the answer for 2006 to 2015 is 47 seats out of 271, or 17.3 per cent, and for 2016 to 2026 it is 107 out of 394, or 27.2 per cent. That is a real difference and I do not want to talk it away.

What the last fifteen years actually look like

The trouble is what happens inside that better average. (which is not good, let me note!)

The year after Orna's committee, in 2014, the share fell from 34.3 per cent to 14.3 per cent. Twenty points in a single year. 2013 stands alone: the year before it was 24 per cent and the year after it was 14.3, and nothing about the conference in between had changed except who was assembling the list. It climbed back to 25 in 2015 and 33.3 in 2016. It held between 25 and 33 for several years. Then 2023 was 20 per cent, and 2024 was 15 per cent, six women on a committee of forty, the biggest committee LICS had assembled up to that point and the lowest share since 2010. Then 21.6 per cent in 2025, and 32.7 per cent in 2026, sixteen women out of forty-nine.

Since 2012 the average year-on-year change is seven percentage points, in one direction or the other. The distance between the worst recent year and the best is more than half the whole range the conference has ever occupied.

That is the finding. Not decline and not progress. Volatility.

I want to be exact about 2026, because it is a good year and it would be dishonest to bury it. The story I could tell you would be a great deal cleaner if I had stopped counting in 2025: a decade of hard-won gains, thrown away in three years, a scandal. That version was written and then I decided to look at 2026 and  had to start again. This is the difference between counting and campaigning, and it is why I keep doing the counting. 

32.7 per cent puts 2026 among the strongest committees in the history of the conference, sixteen women out of forty-nine, the largest LICS has ever assembled. It is below 2013 and it does not reach the level of the best years we have had, but it is close to them, and it is far better than 2024. Close enough that I should say how small these numbers really are. One appointment is worth 2.9 percentage points on the 2013 committee of thirty-five and 2.0 points on the 2026 committee of forty-nine, so the distance between 2026 and the best year on record is less than a single person on either committee. Counted by heads rather than by share, 2026 has sixteen women and no other year has more than twelve. At these sizes a percentage is not a precise instrument, and neither an improvement nor a decline of a couple of points means very much on its own. That applies to my counting as much as to the committees: I am reading gender off names and off knowing people, and one name I have wrong moves this figure by two points.

The 2026 committee was chaired by Claudia Faggian with Joost-Pieter Katoen, and it introduced Associate Chairs sitting inside the committee, one of whom is Orna Kupferman.

But look at what that number sits on top of. The four years 2023 to 2026 together are 37 women's seats out of 161, which is 23 per cent, against 78 out of 265, or 29.4 per cent, for 2015 to 2022. A single strong committee does not undo two weak ones, and nothing about how these committees are assembled makes the strong one likely to repeat. In 2014 we found out exactly how fast a good year can be followed by a bad one.

My own reading of the weak years is that the committees put together in 2022 and 2023 were drawing on a pipeline the pandemic had damaged. That women's research output took the worst of those years is well established: a meta-analysis in eLife pooling 55 studies found the gender gap in research productivity widened by about 7 per cent relative to where it stood before the pandemic, and a study of 2329 Elsevier journals found women submitting proportionally fewer manuscripts during the first wave, with the deficit sharpest among junior women.

Chairs and boards

Program chairs, since it is the chair who assembles the committee. Across forty-one conferences there have been forty-five chair slots, because several years had two chairs. Six went to women, all of them since 2013: Orna Kupferman in 2013, Catuscia Palamidessi in 2015, Patricia Bouyer in 2019, Christel Baier in 2022, Barbara König in 2025 and Claudia Faggian in 2026. Six out of forty-five is worth recording for its own sake, as a count of who has been trusted with the job, whatever effect it does or does not have on the committee that follows.

The line on the 2013 slide about the advisory board was correct, and the situation was worse than a snapshot of 2013 suggests. The board existed from 1998 until 2015, when it was replaced by the steering committee, and in its entire history it had three women: Mariangiola Dezani and Jeannette Wing from 1998 to 2003, then Ursula Martin from 2004 to 2012. Never two at the same time after 2003. Its last three years had none at all, so the body ended its existence in exactly the state the slide had recorded.

The steering committee that replaced it is a flatter story. Since 2016 the share of women has moved between 21 and 32 per cent with no trend in either direction: 54 seats out of 212 across the eleven years, just over a quarter. The 2026 steering committee has five women out of twenty.
What I take from this

It is not about who chairs. That was my first guess and the numbers do not bear it out. Committees chaired by women come to 63 seats out of 219, or 28.8 per cent, and committees chaired by men since 2012 come to 75 out of 302, or 24.8 per cent. There is a gap, but it is small and almost all of it comes from two particular years. Two of the strongest committees in the whole record were assembled by men, and some of the weaker recent ones were assembled by women. Whatever is moving this number, it is not the gender of the person in the chair.

Organization

What did seem to shift the floor was slower and came later. The sustained stretch starts around 2015 and 2016, which is when a few of us began organising rather than merely being appalled, and it holds for the better part of a decade. The shape is the shape.

Nothing holds it in place. There is no policy at LICS that produces a balanced committee, so a good committee is one chair's good judgement and a weak one is another chair's inattention, and the number swings by twenty points between them. Note that the fall after 2013 needed no shock to explain it, and neither did the fall after 2022. Erosion manages perfectly well on its own, and there is now a great deal of help available to it. When someone tells you the problem is solved because this year looks good, ask them what happened the year after the last good year. In 2014 we found out.

And we can only see any of this because someone counts LICS. This is one conference. It is the one I have paid  most attention to, and it is the one with a public archive going back to 1986 that makes an afternoon of arithmetic possible. I do not have these numbers for the other conferences we care about, and neither does anybody else as far as I know (we started collecting them and then gave up). A field that cannot say whether it is at 15 per cent or 33 per cent cannot tell whether anything it does is working.

So we count again, and we should count more widely. If you are chairing anything, count your own committee before the invitations go out rather than after. If you have the patience to do for another conference what I have done here for LICS, please do it and send it to me and we will put it on this blog. And if you find errors in my arithmetic, send those too, because I would rather be corrected than wrong.

Synthetic Mathematics in the Amazon

Talking about Synthetic Mathematics in the middle of the Amazon rainforest felt slightly surreal.

Parintins is famous for the Festival do Boi-Bumbá, for the river, for the forest, for the extraordinary cultural life of the Amazon. It is not the place most people imagine when they think about categorical logic, proof theory, Curry–Howard, or the future of AI-assisted mathematics.

And yet perhaps it was exactly the right place.

My talk at EMALCA Amazonas 2026 was about revolutions in mathematics: how mathematics periodically changes not only its results, but its understanding of what mathematics itself is.

The first great revolution of the twentieth century was the revolution of rigor. Frege, Hilbert, Gentzen, Gödel, Turing, Church: suddenly proofs themselves became mathematical objects. Formalization ceased to be merely philosophical and became technical infrastructure. Mathematics acquired syntax.

That revolution produced modern logic, proof theory, computability theory, formal systems, and eventually computer science itself.

But a second revolution was quietly unfolding in parallel.

The Curry–Howard correspondence — “proofs as programs, propositions as types” — revealed that proofs were not merely static certificates of truth. They had computational content. They could be transformed, executed, normalized, composed. Category theory then provided the missing global language of structure: proofs became morphisms, composition became central, and semantics became unavoidable.

I increasingly think that this second revolution is still incomplete.

We have the theory. We have fragments of the practice. But mathematics as a whole still has not fully absorbed the structural viewpoint introduced by categorical logic and semantics. Neither have Computer Science or Logic done the same. Why?

But now AI arrives.

Large language models can generate mathematical text at astonishing scale. They conjecture, sketch proofs, suggest strategies, translate between formalisms, and increasingly interact with proof assistants. Systems like Lean, Rocq, Isabelle, and Agda are no longer niche curiosities. Formal verification is becoming practical infrastructure.

And AI also reopens the oldest foundational wounds.

LLMs operate probabilistically, not semantically. They produce convincing mathematical language without any guarantees of correctness. They manipulate symbols fluently while remaining disconnected from proof in the classical sense.

This is why the current moment feels less like a purely technological revolution and more like the collision of earlier mathematical revolutions.

The first revolution demanded rigor. The second revealed deep structures connecting proofs, programs, and categories. The third — the AI revolution — suddenly makes those abstract structural questions operationally necessary.

What counts as a proof?
How do we represent mathematical structure?
How do we verify transformations?
What is the semantic content of a generated argument?
How do we move between informal mathematical language and formal systems?

These questions are no longer philosophical luxuries. They are engineering problems for the future of mathematics.

This is one reason I spoke about Dialectica categories in Parintins.

Gödel’s Dialectica interpretation and Girard’s linear logic both force us to think carefully about structure, interaction, resources, witnesses, and transformations. Category theory provides a language capable of relating these ideas without collapsing their distinctions.

I am not claiming that category theory “solves AI”.

Far from it. But I am claiming that the automation of mathematics makes it impossible to ignore semantics any longer.

For decades, categorical logic often seemed abstract, beautiful, and somewhat distant from mainstream mathematical practice. Today the situation is changing. As mathematical reasoning becomes partially automated, questions about meaning, translation, compositionality, verification, and structure move from the foundations to the center.

And perhaps this is why speaking about these ideas in the Amazon felt unexpectedly appropriate.

The Amazon constantly reminds us that scale changes everything. Small local interactions produce vast global structures. Networks matter. Flows matter. Translation between levels matters. Structure matters.

Mathematics is entering a similar moment. We are moving from isolated proofs to ecosystems of formalization, machine assistance, semantic translation, and large-scale mathematical computation. The foundational questions of the twentieth century are returning — but now under computational pressure.

The second revolution is no longer optional.

 

 

Kolmogorov and Alexandrov on a trip. From CultureMath, 2022. 

 

Problems, Problems Everywhere 

There’s a particular kind of mathematical paper that begins with a modest goal and ends up quietly connecting half a century of ideas across logic, category theory, and the philosophy of mathematics. Today I want to talk about one of those papers.

In Kolmogorov–Veloso Problems and Dialectica Categories, Samuel and I set out to understand something that sounds deceptively simple: what is a problem?

Now, if you’re a working mathematician, you might be tempted to answer: “a problem is something I can’t solve yet.” Fair enough. But historically, people have taken this question much more seriously—and much more abstractly.

Kolmogorov, for instance, thought of problems as primitive mathematical objects. Not sets, not functions, not proofs—but problems. Meanwhile, Veloso developed a notion of problems that behave beautifully… provided you are willing to assume the Axiom of Choice. And Blass came along and reframed problems as games of questions and answers, connecting them to computation and complexity.

So naturally, we thought: what could possibly tie all of these together?

Enter Dialectica categories.

If you’ve ever met a Dialectica construction, you’ll know it has a certain personality. It takes something familiar—a category—and turns it into something slightly uncanny: objects become pairs of “witnesses” and “counter-witnesses,” morphisms become strategies, and suddenly everything starts to look like a dialogue. Or a duel.

Or, as it turns out, a problem.

One of the small delights of this paper is realizing that Kolmogorov had already intuited something like this decades earlier. His abstract notion of a problem—so far removed from computation or complexity—fits remarkably well into the Dialectica perspective. It’s as if he had glimpsed the categorical structure before the language was available.

Veloso’s problems, on the other hand, are a bit more demanding. They work beautifully—but only if you’re willing to pay the price of the Axiom of Choice. This gives the whole story a slightly mischievous twist: some problems exist only if you believe in certain kinds of choice, while others are perfectly happy in a more constructive world.

And then there’s Blass, who brings everything down to earth with his questions-and-answers framework. Suddenly, problems are not just abstract entities—they are interactive processes. You ask, I answer; I challenge, you respond. It’s mathematics as conversation, or perhaps as negotiation.

What the categorical perspective does—quietly, but powerfully—is show that these are not competing views. They are different facets of the same underlying structure. A version of the Dialectica construction acts as a kind of translator, moving between Kolmogorov’s abstractions, Veloso’s set-theoretic universe, and Blass’s interactive games.

Along the way, something else becomes clear: the Axiom of Choice is not just a technical convenience. It shapes the very nature of the problems we are allowed to talk about. With full choice, Veloso’s world opens up. With weaker forms—countable or dependent choice—we get more nuanced landscapes. And without choice, we are back in a more constructive, and perhaps more disciplined, universe.

So, what is a problem?

After all this, we still don’t have a single answer—and that’s probably a good thing. Instead, we have a small constellation of answers, connected by categorical structure:

•   a problem as an abstract mathematical entity (Kolmogorov),
•   a problem as a set-theoretic construction (Veloso),
•   a problem as an interactive process (Blass),
•   and a problem as a kind of a Dialectica object, living somewhere in between.

If there’s a moral to the story, it might be this: sometimes the best way to understand a concept is not to define it once and for all, but to see how it transforms as you move between different worlds.

And if those worlds happen to be connected by category theory—well, that’s just a bonus.

---------------------------------------------------------------------------------

de Paiva, Valeria, and Samuel G. da Silva. "Kolmogorov-Veloso problems and Dialectica categories." arXiv preprint arXiv:2107.07854 (2021).