José A. Alonso<p>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. <a href="https://www.educacion.gob.es/teseo/imprimirFicheroTesis.do?idFichero=LiV3M7i%2FrIg%3D" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">educacion.gob.es/teseo/imprimi</span><span class="invisible">rFicheroTesis.do?idFichero=LiV3M7i%2FrIg%3D</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ACL2</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
Verwaltet von:
#ACL2
1 Beitrag1 Beteiligte*r0 Beiträge heute
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
Vestigium · Readings shared July 18, 2025The readings shared in Bluesky on 18 July 2025 are
Teaching software specification (Experience report). ~ Cameron Moy, Daniel Patterson. #CompSci #Teaching #ITP #LeanProver #ACL2
CSLib: An open-sourc
Robust, end-to-end correctness proofs of industrial divide and square root RTL designs. ~ Sol Swords, Cuong Chau. https://www.arith2025.org/proceedings/215900a149.pdf #ITP #ACL2
Play Static Games, Win Static Prizes https://screwlisp.small-web.org/programming/play-static-games-win-static-prizes/
#staticTyping #typechecking #staticProgramAnalysis #commonLisp #lisp #sbcl #series #acl2
In which I look at modern and to some extent historical static program analysis popularly used with common lisp #programming.
I accidentally make the really good point that even if #sbcl is not your deployment target, you can still use its static type checking, for which I work an example.
#lazyEvaluation and formal theorems are also included.
Readings shared May 22, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/22-readings_shared_05-22-25 #ACL2 #ITP #LeanProver #Lisp #Math #Programming
Vestigium · Readings shared May 22, 2025The readings shared in Bluesky on 22 May 2025 are
A formalization of elementary linear algebra: Part I. ~ David M. Russinoff. #ITP #ACL2 #Math
Lean-auto: An interface between Lean 4 and automated the
A formalization of elementary linear algebra: Part I. ~ David M. Russinoff. https://www.russinoff.com/papers/linear1.pdf #ITP #ACL2 #Math
#formalMethods #gamedev #programming #commonLisp #acl2 #itch https://lispy-gopher-show.itch.io/lispmoo2/devlog/907091/formal-game-logic
Since yesterday I advocated strong use of defgeneric, defmethod and McCLIM's define-command, here I present
just giving lisp's defun to acl2's first order #logic.
I present a batch processing style for using acl2 both in #shell and in #lisp with a worked example.
Thoughts and opinions, gamedevs and logical types?
itch.io(formal) game logic - lispmoo2 by screwtape1. Intro This begins part 2 of https://lispy-gopher-show.itch.io/lispmoo2/devlog/906389/my-programming-principles-for-game-dev-12 . Which contains the first five parts. These second five parts contain...
Persib Bandung Kembali Berlatih, Setelah Kalah di Negeri Tirai Bambu https://www.koranmandala.com/sport/104370/persib-bandung-kembali-berlatih-setelah-kalah-di-negeri-tirai-bambu/ #Sport #ACL2 #BRILiga1 #Headline #Maungbandung
KoranMandala.com · Persib Bandung Kembali Berlatih, Setelah Kalah di Negeri Tirai Bambu - KoranMandala.comPersib Bandung Kembali Berlatih setelah sebelumya bertanding diluar Bandung yaitu menghadapi Madura dan juga Zhejiang FC...
Antwortete im Thread
This week I hosted a monthly meetup of Lisp Ireland, where Rafael Sadykov presented his talk "Lisp & Hardware Verification with ACL2".
ACL2 is a theorem prover implemented in a subset of Common Lisp, and the talk discussed how it can be used for formal verification of various systems, and for hardware verification in particular.
The recording was uploaded here: https://www.youtube.com/watch?v=iFEb9p54x_Q
YouTubeLisp Ireland, February 2024 Meetup - Lisp & Hardware Verification with ACL2Rafael Sadykov presents the talk "Lisp & Hardware Verification with ACL2".Join our Lisp meetup to learn about using ACL2 for hardware verification. We'll sho...
Antwortete José A. Alonso
@Jose_A_Alonso
I think the problem is the opposite one found by the authors.
An #acl2 first order proof is to many intents and purposes the same today as five years ago. Instead the authors are criticising fly-by-night commoditisation of proof apps, that turn out to not be reliably correct.