Readings shared June 28, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/29-readings_shared_06-28-25 #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Prologp

Multiparty asynchronous session types: A mechanised proof of subject reduction. ~ Authors Dawit Tirore, Jesper Bengtson, Marco Carbone. https://drops.dagstuhl.de/storage/00lipics/lipics-vol333-ecoop2025/LIPIcs.ECOOP.2025.31/LIPIcs.ECOOP.2025.31.pdf #ITP #CoqProver

Readings shared June 23, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/24-readings_shared_06-23-25 #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Maxima

A verified algebra of cognition: A Coq formalization of the distinction field. ~ Andrey Shkursky. https://philarchive.org/archive/SHKAVA #ITP #CoqProver

Readings shared June 19, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/20-readings_shared_06-19-25 #AI #AIforMath #CoqProver #ITP #IsabelleHOL #LLMs #LeanProver #Math #Rocq

Making concurrent hardware verification sequential. ~ Thomas Bourgeat, Jiazheng Liu, Adam Chlipala, Arvind. https://dl.acm.org/doi/pdf/10.1145/3729331 #ITP #CoqProver #Rocq

Readings shared June 16, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/17-readings_shared_06-16-25 #CoqProver #ITP #LeanProver #Math #Rocq

Toward a formalization of secure multiparty computation stack. ~ Cheng-Hui Weng, Reynald Affeldt, Jacques Garrigue, Takafumi Saikaaw. https://www.math.nagoya-u.ac.jp/~garrigue/papers/weng-ppl2025.pdf #ITP #CoqProver #Rocq

Readings shared June 15, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/16-readings_shared_06-15-25 #AI #AIforMath #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Lisp #Math #Programming #Rocq

BiCoq: Bigraphs formalisation with Coq. ~ Cécile Marcon et als. https://www.dcs.gla.ac.uk/~michele/papers/SAC2025.pdf #ITP #CoqProver #Rocq #Math

Readings shared June 13, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/14-readings_shared_06-13-25 #AI #AIforMath #Autoformalization #CoqProver #HOL_Light #ITP #IsabelleHOL #LLMs #LeanProver #Logic #MLLMs #Math #Rocq

Reseña de «MATP-BENCH: Can MLLM be a good automated theorem prover for multimodal problems?». https://jaalonso.github.io/vestigium/posts/2025/06/13-resena-de-matp-bench-can-mllm-be-a-good-automated-theorem-prover-for-multimodal-problems/ #AI #MLLMs #Math #ITP #IsabelleHOL #LeanProver #CoqProver #AIforMath

MATP-BENCH: Can MLLM be a good automated theorem prover for multimodal problems? ~ Zhitao He et als. https://arxiv.org/abs/2506.06034 #AI #MLLMs #Math #ITP #IsabelleHOL #LeanProver #CoqProver #AIforMath

Formal verification of relational algebra transformations in Fiat2 using Coq. ~ Christian Teshome. http://adam.chlipala.net/theses/teshome.pdf #ITP #CoqProver #Rocq

Readings shared June 12, 2025. https://jaalonso.github.io/vestigium/posts/2025/06/13-readings_shared_06-12-25 #ATP #CoqProver #FunctionalProgramming #Haskell #ITP #LLMs #LeanProver #Logic #Math #Rocq

Can large language models verify system software? A case study using FSCQ as a benchmark. ~ Jianxing Qin et als. https://dl.acm.org/doi/pdf/10.1145/3713082.3730382 #LLMs #ITP #CoqProver #Rocq

Readings shared May 27, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/26-readings_shared_05-26-25 #CoqProver #ITP #LeanProver #Math #Programming

A foundationally verified intermediate verification language. ~ Joshua M. Cohen. https://www.cs.princeton.edu/~jmc16/docs/thesis.pdf #ITP #CoqProver #Wyh3