@jfdm @edwinb We may be around Edinburgh at some point in the next few weeks.

@JacquesC2 @pigworker Next SPLS should be in October & you'll be around so I guess we could think of inviting Marcelo.

@pigworker I don't think so. It's based on github.com/DimaSamoz/agda-soas but during the talk Marcelo has been really emphasising the tension between the mathematics done in CT and the encoding in proof assistants.

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 ! youtu.be/mhZU6RWlyo0

@framasky @AdrienneCharmet Quand tout le reste est fermé, il reste les fish&chips près de la gare (avec même des deep-fried pizzas !)

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) gallais.github.io/blog/termina

A Prettier Printer by Philp Wadler - buff.ly/2us0Dal

#poem #tree #parsing #printing pic.twitter.com/FkBOBOjl9n

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 ! gallais.github.io/pdf/draft_fs

La Quadrature du Net - Mastodon - Media Fédéré

Mamot.fr est un serveur Mastodon francophone, géré par La Quadrature du Net.