Afficher plus

New blog-post on Gagallium by François Pottier, demonstrating the use of its library "fix", to construct an automata from a regular expression. Enjoy!

gallium.inria.fr/blog/fixin-yo

Petit écho rigolo à ma conférence de Numérique en commun[s] (dont on me parle encore ! 😉)

@MartinShadok À propos de l'axiome GD, il semblerait que ça soit la logique de Gödel-Dummett, mais je n'arrive pas à trouver grand chose dessus... Il semblerait que GD => WEM, et qu'on puisse faire des modèles de GD dont les valeurs de vérité soient n'importe quel sous-ensemble de [0, 1] contenant 0 et 1, mais je n'arrive pas à trouver beaucoup plus que ça :/

@MartinShadok Aucun des deux n'est prouvable en logique intuitionniste, car en logique intuitionniste, si tu peux prouver `A \/ B` sans hypothèses, tu peux pouver `A` ou tu peux prouver `B` (par exemple, s'il s'agit d'un terme Coq, il suffit de regarder si le terme de preuve réduit commence par `or_introl` or `or_intror`).
Par contre, je sais pas trop à quoi ils servent, mais ncatlab me dit que WEM est équivalent à une des formules de De Morgan.

Liste de projets fous à faire un jour (c'est vraiment raisonnable?) :
- Réécrire Bourbaki en espéranto, avec pour axiomes la théorie des ensembles
- Faire la même chose pour l'informatique
- Écrire un assistant de preuve pour la théorie des ensembles
- Utiliser cet assistant pour formaliser les deux premiers points
- Inventer une langue "juste parce que c'est marrant"
- Écrire une encyclopédie imaginaire comme dans Tlön, Uqbar, Orbis Tertius
- Trouver plus de choses à rajouter dans cette liste

New blogpost on gagallium by @nore about statically typing algebraic effects using MLsub!

gallium.inria.fr/blog/safely-t

Framapiaf

Framapiaf est un service de microblog similaire à Twitter. Il est libre, décentralisé et fédéré. Il permet de courts messages (max. 500 caractères), de définir leur degré de confidentialité et de suivre les membres du réseau sans publicité ni pistage.