I use em-dashes with consistent spacing.

@MartinEscardo what matters for typetopology: we've optimised lexing, parsing, handling of names (these primarily affect time spent in garbage collection), implemented a faster hashtable for serialisation, changed the semantics of -j to avoid a minor-but-quadratic overhead in worker startup (in addition to properly sharing project (= agda-lib file) state across workers), optimised syntactic equality, optimised metavariable pruning, removed a quadratic overhead from the types of metavariables, optimised the representation of and a bunch of code that deals with telescopes (≈ contexts), and made it so parameterised module applications only "pay" for the definitions they actually use¹

¹ in some libraries (1lab, agda-categories) this was a lot of the typechecker time, but typetopology only spends ~5s in the ApplySection profiling point so it shouldn't affect its timing too much.

@de_Jong_Tom @totbwf

@amy

In the machine I am using now, with -j, I get 54s for Agda (development version) and 33s for Mikan.

Nice!

Can you summarize what you optimized?

@de_Jong_Tom @totbwf

The realities of modern warfare make hosting your applications and data in data centers a risky proposition. However, with novel coding techniques, it may be possible to install applications, and maybe even store data, on end users’ own devices

#veilleesr « J’en ai assez de ce sentiment d’échec et d’injustice » : l’amertume des jeunes chercheurs qui n’arrivent pas à décrocher un poste à l’université
« En attendant de décrocher un poste, les jeunes docteurs doivent multiplier, à l’image d’Axelle, les contrats courts de recherche et d’enseignement pour vivre et continuer à enrichir leur CV. Tout en passant des semaines à monter des dossiers de candidature complexes. « Ce double agenda professionnel, qui dure souvent plusieurs années, a un impact important sur l’organisation de leur vie personnelle », commente Alexis Alamel, maître de conférences en géographie à Sciences Po Rennes, et auteur d’une étude, à paraître fin 2026, sur le parcours de ces docteurs. Cette grande salle d’attente pour entrer officiellement dans la carrière est synonyme de précarité et d’incertitudes. « Elle implique surtout de nombreuses concessions, des déménagements réguliers en fonction des contrats, des relations dégradées avec les proches, des projets familiaux retardés – et parfois, des couples qui se séparent. Et, in fine, une fatigue physique et psychologique importante… », complète le chercheur. »

https://www.lemonde.fr/campus/article/2026/09/29/j-en-ai-assez-de-ce-sentiment-d-echec-et-d-injustice-l-amertume-des-jeunes-chercheurs-qui-n-arrivent-pas-a-decrocher-un-poste-a-l-universite_6785592_4401467.html

Mechanising Denotational Semantics in Agda

Peter D. Mosses, Jesper Cockx, Bernhard Reus
https://arxiv.org/abs/2610.14898 https://arxiv.org/pdf/2610.14898 https://arxiv.org/html/2610.14898

arXiv:2610.14898v1 Announce Type: new
Abstract: Mechanisation of a mathematical definition (also referred to as formalisation) has many benefits. Here, we focus on mechanising denotational semantic definitions of programming languages by embedding them in the Agda language. The Agda type-checker detects and reports any issues with the wellformedness and type correctness of the embedded definitions.
To minimise the effort required, and to facilitate correlation of the original definition with its Agda embedding, mechanisation should not involve significant reformulation or extension. Here, we show how to embed conventional Scott-Strachey denotational definitions in Agda with almost no changes to $\lambda$-notation or domain equations.
Agda notation for definitions of types and functions corresponds closely to the conventional meta-notation of denotational semantics. We have developed a collection of Agda modules with postulated types for commonly used domain constructors and their associated operations.
We illustrate our approach with mechanisations of three denotational definitions: a model of the untyped $\lambda$-calculus, Plotkin's denotational semantics of PCF, and a semantics of a sublanguage of Scheme. In previous work, similar mechanisations in Agda have revealed several unsuspected wellformedness issues in published denotational definitions.
Some of the postulated properties of our definitions are inconsistent with a classical set-theoretic interpretation of Agda. We conjecture that they would be consistent with an interpretation of Agda in a higher-order intuititionistic logic, such as that used by Simpson in his work on synthetic domain theory. After recalling previous work on mechanising domain theory, we consider the possibility of mechanising synthetic domain theory in Agda.

toXiv_bot_toot

@henk @MarloesdeKoning
"De politie in Amsterdam liet de server ophalen op basis van een Amerikaans rechtshulpverzoek. „Dat voer je dan gewoon uit”, zegt een woordvoerder telefonisch."
Kunnen we dus net zo goed alles op Amerikaanse servers zetten.
Ongelofelijk dit!
#soevereiniteit #VS #privacy
@thefirewall @EricChrSmit @marleenstikker

Amsterdam police seize server of Italian internet service provider A/I on US request

(translated from dutch)

#autistici #autisticiInventati @MarloesdeKoning

"A unit of the Amsterdam police on Tuesday at a data center at the Science Park in Amsterdam seized a server from the Italian internet service provider Autistici/Inventati (A/I). That happened on the basis of a U.S. legal assistance request. A copy of the server's content is now sent to the US."

https://www.nrc.nl/nieuws/2026/10/14/politie-amsterdam-neemt-op-amerikaans-verzoek-server-in-beslag-van-italiaanse-internetdienstverlener-a-i-a4938960?gift_token=4938960~1792586921~AUC73w4BRcmMEYMgr2r6uw~YMvykHFdRdiyZ5Xpc9k8dKoJLTLtZC05mIVPgp6n-xI

Aaron Swartz was charged on July 14th, 2011 with wire fraud and computer fraud (under the Computer Fraud and Abuse Act). He potentially faced 30 years in jail and a fine of 1 million dollars or more. The theory was that he exceeded authorized access by automated scraping through 4.8 million JSTOR articles.

Contrast with...

AI crawlers crawl trillions of documents, often ignoring any ToS the prohibit automated scraping.

OpenAI downloaded pirated books from Library Genesis and created internal datasets that became the foundation for GPT-3's training.

Meta torrented 80+ TB of data from Anna's Archive for Llama 4. There are records of internal discussions at Meta that the data set was known to be pirated content.

Where is the federal prosecutor to throw charges at OpenAI and Meta? That's right. No charges.

> En France, les coopératives de location ont été dissoutes dans les années 1970, alors que la majorité des autres pays européens ont conservé ce modèle. Alors que nous traversons aujourd’hui une tempête, ce modèle est pourtant très utile chez nos voisins. À Genève, par exemple, les coopératives gèrent plus de 5 % des logements du canton, avec des loyers 40 % inférieurs au marché. Et là où beaucoup se cassent les dents, ces coopératives continuent d'investir. Fort de ce succès, le canton a récemment voté par référendum pour doubler la proportion de logements coopératifs et atteindre 10 % du parc de logements.

https://www.transitions.city/newsletter257/

The right solution always seems obvious in hindsight. It’s important to remember that it certainly wasn’t obvious just a bit ago.

Als de voorspelde uitbouw van datacenters voor het gebruik van AI zich voltrekt, wordt het wel erg moeilijk om de klimaatopwarming binnen de afgesproken grenzen te houden. Dat blijkt uit nieuwe berekeningen van professor @wim_v12e (University of Glasgow).

“Als we doen wat de AI-industrie wil, dan wordt het simpelweg een ramp.”

https://apache.be/2026/10/12/geplande-ai-datacenters-bedreigen-haalbaarheid-van-klimaatdoelen?cdlnk=cE9PbTRJVVcrb0R2VE13cXJpN082MTUxOExlb21uOEdIU3JqSHJCa0RBU0RVRUp3cllaUzdmVUNOTEd3bUpIUzhQTlRUVlNrMFhucU5OalRtcnhxMnZlOThNYTVid2pqeFE9PTo6ODBiMDIxMGNjMGJiYzQ3YTUxNDU2Y2YxN2MzZmI4MDA%3D

Interesting choice of Springer Nature to put the DOI of a paper not in the doi field of an exported bibtex reference, but rather in the ID, where it does not show up in the citation and is probably overwritten by a more tractable ID by any citer.

@HydrePrever @gfadrelle

"A second favorite criterion for rejection is obviousness. However, most good ideas are obvious in retrospect, and humans are very bad at realizing that they just learned something when presented with such an idea. We all react as, “oh yeah, of course, that’s true,” not realizing that it wasn’t true to us an hour ago. Instead, we favor the esoteric, the difficult to read, and the obscure. If a paper is easy to read, it is deemed obvious."

https://sigbed.org/2022/08/22/the-toxic-culture-of-rejection-in-computer-science/

I'm not sure they're good at categorizing who is sentient and what is not, but I think silicon valley is on to something with this idea that sentient beings must be treated morally right.

Dutch is the Natural Language.

I'm not a native speaker myself, but I would say that OpenAI is testing models on problems, not problems on models.

@tito
Not just a generation of people. If the chain of transmission is broken, we'll be rebuilding entire fields. Sure, we'll have the writing, but to understand it you have to already be in the field, and that knowledge is usually bootstrapped by teaching, not just reading.

A message from my colleague Benedikt Ahrens:

Hi all,

I have funding for a postdoc position at TU Delft on combining computer proof assistants and computer algebra systems in the area of category theory, and I would be happy to hear from potential applicants before the formal advert goes out.

I am looking for someone who is interested in all three of proof assistants, computer algebra systems, and category theory, and who has some experience in at least one or two of them.

The position ideally starts no later than March 2027.

If you are interested, please email me at B.P.Ahrens@tudelft.nl with a short note about your background and your research interests. Informal questions are very welcome.

Please feel free to forward this to anyone who might be a good fit.

Best wishes, Benedikt

Update: the position is now open!

https://careers.tudelft.nl/job/Delft-Postdoc-Category-Theory%2C-Computer-Proof-Assistants-and-Computer-Algebra-Systems-2628-CD/1373970157/

In between giving up on maintaining order altogether, and bringing real grenades to a school kids protest, French law enforcement has plenty of other options, e.g. tear gas and water cannons.

Citizens of France should never be led to believe that losing body parts is a risk you have to take when joining citizen protests. Surrounding countries do not seem to have this, I only ever hear this about France.

That it now hits minors is atrocious.

https://www.franceinfo.fr/societe/education/blocage-des-lycees/un-adolescent-de-15-ans-a-eu-la-main-arrachee-par-une-grenade-a-lens-une-enquete-de-l-igpn-ouverte-annonce-le-procureur-de-bethune_8223337.html