Marcelo Fiore is engaging in an experiment: how many times can you formulate the wish for inductive families in the presheaf category before @pigworker materialises in the room.

🎥 NOUVELLE VIDÉO ! Aujourd’hui on parle de comment on gère le réseau électrique et on le fait depuis le centre de contrôle du réseau électrique du pays. Parce que pourquoi pas !

Part of the beauty of this paper is that the algorithm is total and it's relatively easy to prove (and therefore to implement in Type Theory). You only need to use 3 tricks to make Agda accept the whole development (two for the code, one for an example)

A Prettier Printer by Philp Wadler -

#poem #tree #parsing #printing

This weekend my great coauthors and I shipped a draft about a universe of scope safe syntaxes with binding, their semantics and proofs! Plenty of , and even !

La Quadrature du Net - Mastodon - Media Fédéré est un serveur Mastodon francophone, géré par La Quadrature du Net.