#acl2 — Public Fediverse posts

DEAD MIC #lispyGopherClimate live installing #acl2 #lisp #fol and #lambdamoo using #emacs #tramp over #i2p #ssh .

https://toobnix.org/w/7BpQvVU9KQnKWVsVWF2HNb

A very little about #acl2 and #commonLisp - reading some Kaufmann and Moore on floats.

https://toobnix.org/w/4L9y5HxErbaajwcHgskJTS

Readings shared October 20, 2025. https://jaalonso.github.io/vestigium/posts/2025/10/21-readings_shared_10-20-25 #ACL2 #Autoformalization #FunctionalProgramming #Haskell #ITP #LLMs #LeanProver #Logic #Math #Mizar #RustLang

Towards verifying the "Three amigos". ~ Carl Kwan. https://repositories.lib.utexas.edu/server/api/core/bitstreams/aaa69649-caa2-4c06-bd35-3b585e008c56/content #ITP #ACL2 #Math

Readings shared October 4, 2025. https://jaalonso.github.io/vestigium/posts/2025/10/05-readings_shared_10-04-25 #ACL2 #AI #Algorithms #FunctionalProgramming #ITP #IsabelleHOL #LLMs #Math

A formal Y86 simulator with CHERI features. ~ Carl Kwan , Yutong Xin, William D. Young. https://repositum.tuwien.at/bitstream/20.500.12708/219552/1/Kwan-2025-A%20Formal%20Y86%20Simulator%20with%20CHERI%20Features-vor.pdf #ITP #ACL2

Verificación formal en ACL2 de polinomios de múltiples variables y su aplicación al problema de la decisión en la lógica proposicional clásica. ~ Francisco Palomo Lozano. https://www.educacion.gob.es/teseo/imprimirFicheroTesis.do?idFichero=LiV3M7i%2FrIg%3D #ITP #ACL2 #Logic #Math

Readings shared July 25, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/26-readings_shared_07-25-25 #ACL2 #AI4Math #FunctionalProgramming #Haskell #ITP #LeanProver #Math

Extended abstract: Partial-encapsulate and its support for floating-point operations in ACL2. ~ Matt Kaufmann, J Strother Moore. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL2in2025.6 #ITP #ACL2

RV32I in ACL2. ~ Carl Kwan. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL2in2025.4 #ITP #ACL2

A proof of the Schröder-Bernstein theorem in ACL2. ~ Grant Jurgensen. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL2in2025.3 #ITP #ACL2 #Math

A formalization of elementary linear algebra: Part II. ~ David Russinoff. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL2in2025.2.pdf #ITP #ACL2 #Math

A formalization of elementary linear algebra: Part I. ~ David Russinoff. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL2in2025.1.pdf #ITP #ACL2 #Math

Readings shared July 18, 2025. https://jaalonso.github.io/vestigium/posts/2025/07/19-readings_shared_07-18-25 #ACL2 #CompSci #FunctionalProgramming #Haskell #ITP #LLMs #LeanProver #Rocq #Rust #Teaching