Readings shared July 14, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/15-readings_shared_07-14-25 #Coq #ITP #IsabelleHOL #LLMs #LeanProver #Math
Readings shared July 14, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/15-readings_shared_07-14-25 #Coq #ITP #IsabelleHOL #LLMs #LeanProver #Math
Pyrosome: Verified compilation for modular metatheory. ~ Dustin Jamner, Gabriel Kammer, Ritam Nag, Adam Chlipala. https://arxiv.org/abs/2507.06360v1 #ITP #Coq
Readings shared July 7, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/08-readings_shared_07-07-25 #Coq #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Maxima
Curso "Razonamiento automático (2018-19)". https://jaalonso.github.io/cursos/m-ra-18 #DemostraciónInteractiva #ProgramaciónFuncional #IsabelleHOL #Coq
Readings shared May 31, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/31-readings_shared_05-31-25 #Agda #Coq #FunctionalProgramming #Haskell #HoTT #ITP #LeanProver #Logic #Math #Minlog #Rocq
A Coq formalization of Lagois connections for secure information flow. ~ Casper Stahl et als. https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper80.pdf #ITP #Coq #Rocq
Verifying Z3 RUP proofs with the interactive theorem provers Coq/Rocq and Agda. ~ Harry Bryant et als. https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper67.pdf #ITP #Coq #Rocq #Agda
Readings shared May 29, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/29-readings_shared_05-29-25 #AI #Agda #Coq #Emacs #ITP #IsabelleHOL #LeanProver #Lisp #Logic #Math
Construire des preuves mathématiques. ~ Thierry Coquand, William Rowe-Pirra. https://interstices.info/construire-des-preuves-mathematiques/ #ITP #Coq
Les trois bizarres de la #basseCour, ceux qui sont toujours derrière toi quand tous les autres sont partis.
Il y a Jean-Gab, le #canard moche mais sympas. Souvent il s'avance vers toi en ayant l'air de se tripoter les mains dans le dos, timide mais cou tendu : "bouffe ? oh, sans vouloir vous déranger, hein".
Et puis deux "broilers brothers", comme des chats, ils vont où on est et ils se couchent pas loin… ou devrais-je dire ils s’assoient… ou… mais sérieux, c'est quoi cette position ?
#coq
Readings shared May 19, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/19-readings_shared_05-19-25 #CommonLisp #Coq #ITP #IsabelleHOL #LeanProver #Math #Programming #Python #Rocq
Formally specifying contract optimizations with bisimulations in Coq. ~ Derek Sorensen. https://drops.dagstuhl.de/storage/01oasics/oasics-vol129-fmbc2025/OASIcs.FMBC.2025.11/OASIcs.FMBC.2025.11.pdf #ITP #Coq #Rocq
Lógicas de orden superior y verificación formal [Slides]. ~ Lourdes del Carmen González Huesca. https://drive.google.com/drive/folders/1cE1a0N-2ZMrVx8i58W0KG8s3KMVHawZn #Logic #Math #Haskell #FunctionalProgramming #ITP #Coq #Rocq
Lógicas de orden superior y verificación formal. ~ Lourdes del Carmen González Huesca. https://youtu.be/9uTD7BMvbjw #Logic #Math #Haskell #FunctionalProgramming #ITP #Coq #Rocq
A graphical interface for category theory proofs in Coq. ~ Luc Chabassier. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ThEdu24.2.pdf #ITP #Coq #Rocq #CategoryTheory
Proof assistants for teaching: A survey. ~ Frédéric Tran Minh, Laure Gonnord and Julien Narboux. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ThEdu24.1.pdf #ATP #ITP #IsabelleHOL #LeanProver #Coq #Rocq #Education