Guillaume Munch-Maccagnoni

@JacquesC2@types.pl @de_Jong_Tom@mathstodon.xyz To clarify my question, I am interested in it from a point of view of governance of commons.

• If someone opens a PR containing LLM-generated code, can it be closed as a consequence of people reminding that “there is no consensus in accepting LLM-generated code”?
• If someone proposes a PR that adds a section to CONTRIBUTING.md informing that “there is no consensus in allowing LLM-generated code”, will it be accepted?

I'd very naively expect the answer to be yes to both according to the reasoning used.

In any case seeing this opposition by many people reflects well on the #agda community in my opinion. When #ocaml adopted a lukewarm policy, few people paid attention (apart from people with ties to Jane Street for some reason). The discussion did not focus on the ethical issues whereas the legal issues were sidestepped the way those policies usually do.

@de_Jong_Tom@mathstodon.xyz So Agda developers decided that AI-written code can be allowed (within some limits), without consensus, by claiming that there was no consensus to impose a ban on AI-written code? Without addressing the ethical and legal concerns that were raised? I'm outside of this community but I'm interested in understanding what happened.

RE: @gadmm@mathstodon.xyz

We've uploaded on arXiv the new version of our paper “Linear effects, exceptions, and resource safety: a Curry-Howard correspondence for destructors” (jww. Sidney Congard, and Rémi Douence). This version takes the feedback from the reviewers of ESOP into account, who we thank for helping us make the paper clearer. It is a slightly longer version with more details of the paper published at ESOP.

https://arxiv.org/abs/2510.23517

@MartinEscardo @jonmsterling @antoinechambertloir Not breaking things has been a value for many ecosystems of old, but I have the impression that people have forgotten its value, even in LaTeX to some (limited) extent.

I wish I was present at the @ETAPSconf@mastodon.education business meeting, unfortunately I could not attend the conference.

On the subject of licensing differences between LNCS and LipiCS, it was reported to me that the LipiCS representative affirmed that there was “no formal difference” with Springer. Could someone who was there clarify what was said?

The claim is very surprising, given that the contract I signed with Springer for ESOP demanded exclusive rights that allow relicensing (i.e. Springer has all rights who then give some back to everyone including authors via a CC license, with rights to sell more permissive licences to LLM companies), whereas an author agreement form for LipiCS which I could find online demands non-exclusive rights (roughly speaking providing LipiCS with a CC license). This sounds like a very formal difference!

edit: since there are a lot of acronyms in this post:
- LNCS: Lecture Notes in Computer Science (Springer book series)
- LipiCS: Leibniz International Proceedings in Informatics by Dagstuhl Publishing
- ESOP: a computer science conference part of @ETAPSconf@mastodon.education
- CC: creative commons
- LLM: large language model

The continuations debate in programming languages can be summarised as follows: one camp debates whether we should use CPS or not for compilation. The other camp believes that the recurrence of the concept of continuation in many places in computer science and logic is revealing a fundamental structure of computation; syntax is not arbitrary, good syntactic artifacts let us get a glimpse of and benefit from this structure underneath.

In the paper "Compiling with continuations, or without? Whatever", Cong, Osvald, Essertel and Rompf propose to capture the second-class nature of continuations used in compilation in a type-theoretic way. Seemingly advocating for the first camp, it places itself in the second.

Seeking to understand their CPS from the point of view of sequent calculus, Jean Caspar and I propose at PEPM 2026 (this morning) an understanding of their calculus from the point of view of polarised classical S4 sequent calculus. Continuations used in compilation are in-between intuitionistic (linearly-used) and classical (unrestricted use). Polarised S4 realises this mixing of classical and intuitionistic logic due to the Gödel-McKinsey-Tarski theorem which states the intuitionistic nature of the modal fragment of S4.

"S4 modal sequent calculus as intermediate logic and intermediate language" (with paper available):
https://popl26.sigplan.org/details/pepm-2026-papers/6/S4-modal-sequent-calculus-as-intermediate-logic-and-intermediate-language-Short-Pape

@chrisamaphone @cbaberle The logical relation with a monoid thing reminded me of Dal Lago's and Hofmann's quantitative realisability [1] and Aloïs Brunel's PhD work extending it to biorthogonality/forcing [2,3], which was a precursor to Brunel et al.'s coeffect/graded calculus. It is probably more remote (they do not investigate linear parametricity results to my knowledge, and definitely do not look at ordered logic) but Aloïs's PhD work is amazing and I thought you might like to hear about it (I suspect that one might not easily stumble upon it). [1] https://www.sciencedirect.com/science/article/pii/S0304397510007164 [2] https://theses.hal.science/tel-01162997 [3] http://arxiv.org/abs/1201.4307