Med-Mastodon

José A. AlonsoReadings shared July 25, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/07/26-readings_shared_07-25-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/07/26-readings_shared_07-25-25</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a> <a href="https://mathstodon.xyz/tags/AI4Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#AI4Math</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

José A. AlonsoExtended abstract: Partial-encapsulate and its support for floating-point operations in ACL2. ~ Matt Kaufmann, J Strother Moore. <a href="https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL2in2025.6" rel="nofollow noopener" translate="no" target="_blank">https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL2in2025.6</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a>

José A. AlonsoRV32I in ACL2. ~ Carl Kwan. <a href="https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL2in2025.4" rel="nofollow noopener" translate="no" target="_blank">https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL2in2025.4</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a>

José A. AlonsoA proof of the Schröder-Bernstein theorem in ACL2. ~ Grant Jurgensen. <a href="https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL2in2025.3" rel="nofollow noopener" translate="no" target="_blank">https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL2in2025.3</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

José A. AlonsoA formalization of elementary linear algebra: Part II. ~ David Russinoff. <a href="https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL2in2025.2.pdf" rel="nofollow noopener" translate="no" target="_blank">https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL2in2025.2.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

José A. AlonsoA formalization of elementary linear algebra: Part I. ~ David Russinoff. <a href="https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL2in2025.1.pdf" rel="nofollow noopener" translate="no" target="_blank">https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL2in2025.1.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

José A. AlonsoReadings shared July 18, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/07/19-readings_shared_07-18-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/07/19-readings_shared_07-18-25</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#CompSci</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a> <a href="https://mathstodon.xyz/tags/Rust" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rust</a> <a href="https://mathstodon.xyz/tags/Teaching" class="mention hashtag" rel="nofollow noopener" target="_blank">#Teaching</a>

José A. AlonsoTeaching software specification (Experience report). ~ Cameron Moy, Daniel Patterson. <a href="https://ccs.neu.edu/~camoy/pub/lsl.pdf" rel="nofollow noopener" translate="no" target="_blank">https://ccs.neu.edu/~camoy/pub/lsl.pdf</a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#CompSci</a> <a href="https://mathstodon.xyz/tags/Teaching" class="mention hashtag" rel="nofollow noopener" target="_blank">#Teaching</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a>

José A. AlonsoReadings shared July 9, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/07/10-readings_shared_07-09-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/07/10-readings_shared_07-09-25</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a> <a href="https://mathstodon.xyz/tags/CAS" class="mention hashtag" rel="nofollow noopener" target="_blank">#CAS</a> <a href="https://mathstodon.xyz/tags/CoqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#CoqProver</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Rust" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rust</a> <a href="https://mathstodon.xyz/tags/SAT" class="mention hashtag" rel="nofollow noopener" target="_blank">#SAT</a>

José A. AlonsoRobust, end-to-end correctness proofs of industrial divide and square root RTL designs. ~ Sol Swords, Cuong Chau. <a href="https://www.arith2025.org/proceedings/215900a149.pdf" rel="nofollow noopener" translate="no" target="_blank">https://www.arith2025.org/proceedings/215900a149.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a>

screwlispPlay Static Games, Win Static Prizes <a href="https://screwlisp.small-web.org/programming/play-static-games-win-static-prizes/" rel="nofollow noopener" translate="no" target="_blank">https://screwlisp.small-web.org/programming/play-static-games-win-static-prizes/</a> <a href="https://gamerplus.org/tags/staticTyping" class="mention hashtag" rel="nofollow noopener" target="_blank">#staticTyping</a> <a href="https://gamerplus.org/tags/typechecking" class="mention hashtag" rel="nofollow noopener" target="_blank">#typechecking</a> <a href="https://gamerplus.org/tags/staticProgramAnalysis" class="mention hashtag" rel="nofollow noopener" target="_blank">#staticProgramAnalysis</a> <a href="https://gamerplus.org/tags/commonLisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#commonLisp</a> <a href="https://gamerplus.org/tags/lisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#lisp</a> <a href="https://gamerplus.org/tags/sbcl" class="mention hashtag" rel="nofollow noopener" target="_blank">#sbcl</a> <a href="https://gamerplus.org/tags/series" class="mention hashtag" rel="nofollow noopener" target="_blank">#series</a> <a href="https://gamerplus.org/tags/acl2" class="mention hashtag" rel="nofollow noopener" target="_blank">#acl2</a> In which I look at modern and to some extent historical static program analysis popularly used with common lisp <a href="https://gamerplus.org/tags/programming" class="mention hashtag" rel="nofollow noopener" target="_blank">#programming</a>.I accidentally make the really good point that even if <a href="https://gamerplus.org/tags/sbcl" class="mention hashtag" rel="nofollow noopener" target="_blank">#sbcl</a> is not your deployment target, you can still use its static type checking, for which I work an example.<a href="https://gamerplus.org/tags/lazyEvaluation" class="mention hashtag" rel="nofollow noopener" target="_blank">#lazyEvaluation</a> and formal theorems are also included.

José A. AlonsoReadings shared May 22, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/05/22-readings_shared_05-22-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/05/22-readings_shared_05-22-25</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Lisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#Lisp</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="nofollow noopener" target="_blank">#Programming</a>

José A. AlonsoA formalization of elementary linear algebra: Part I. ~ David M. Russinoff. <a href="https://www.russinoff.com/papers/linear1.pdf" rel="nofollow noopener" translate="no" target="_blank">https://www.russinoff.com/papers/linear1.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

José A. AlonsoReadings shared May 21, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/05/21-readings_shared_05-21-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/05/21-readings_shared_05-21-25</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener" target="_blank">#AI</a> <a href="https://mathstodon.xyz/tags/AlphaEvolve" class="mention hashtag" rel="nofollow noopener" target="_blank">#AlphaEvolve</a> <a href="https://mathstodon.xyz/tags/CommonLisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#CommonLisp</a> <a href="https://mathstodon.xyz/tags/CompSci" class="mention hashtag" rel="nofollow noopener" target="_blank">#CompSci</a> <a href="https://mathstodon.xyz/tags/Emacs" class="mention hashtag" rel="nofollow noopener" target="_blank">#Emacs</a> <a href="https://mathstodon.xyz/tags/GeneticAlgoritm" class="mention hashtag" rel="nofollow noopener" target="_blank">#GeneticAlgoritm</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/OrgMode" class="mention hashtag" rel="nofollow noopener" target="_blank">#OrgMode</a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="nofollow noopener" target="_blank">#Programming</a> <a href="https://mathstodon.xyz/tags/Python" class="mention hashtag" rel="nofollow noopener" target="_blank">#Python</a>

José A. AlonsoA formalization of the correctness of the Floodsub protocol. ~ Ankit Kumar, Panagiotis Manolios. <a href="https://ankitku.github.io/stuff/floodsub-acl2ws.pdf" rel="nofollow noopener" translate="no" target="_blank">https://ankitku.github.io/stuff/floodsub-acl2ws.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a>

José A. AlonsoReadings shared May 4, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/05/04-readings_shared_05-04-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/05/04-readings_shared_05-04-25</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a>

José A. AlonsoFormal verification of blockchain nonforking in DAG-based BFT consensus with dynamic stake. ~ Alessandro Coglio, Eric McCarthy. <a href="https://alessandrocoglio.info/techrep-2025-aleobft.pdf" rel="nofollow noopener" translate="no" target="_blank">https://alessandrocoglio.info/techrep-2025-aleobft.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a>

vintage screwlisp account<a href="https://mastodon.sdf.org/tags/formalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#formalMethods</a> <a href="https://mastodon.sdf.org/tags/gamedev" class="mention hashtag" rel="nofollow noopener" target="_blank">#gamedev</a> <a href="https://mastodon.sdf.org/tags/programming" class="mention hashtag" rel="nofollow noopener" target="_blank">#programming</a> <a href="https://mastodon.sdf.org/tags/commonLisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#commonLisp</a> <a href="https://mastodon.sdf.org/tags/acl2" class="mention hashtag" rel="nofollow noopener" target="_blank">#acl2</a> <a href="https://mastodon.sdf.org/tags/itch" class="mention hashtag" rel="nofollow noopener" target="_blank">#itch</a> <a href="https://lispy-gopher-show.itch.io/lispmoo2/devlog/907091/formal-game-logic" rel="nofollow noopener" target="_blank">https://lispy-gopher-show.itch.io/lispmoo2/devlog/907091/formal-game-logic</a>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 <a href="https://mastodon.sdf.org/tags/logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#logic</a>.I present a batch processing style for using acl2 both in <a href="https://mastodon.sdf.org/tags/shell" class="mention hashtag" rel="nofollow noopener" target="_blank">#shell</a> and in <a href="https://mastodon.sdf.org/tags/lisp" class="mention hashtag" rel="nofollow noopener" target="_blank">#lisp</a> with a worked example.Thoughts and opinions, gamedevs and logical types?

José A. AlonsoReadings shared March 15, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/15-readings_shared_03-15-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/03/15-readings_shared_03-15-25</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener" target="_blank">#AI</a> <a href="https://mathstodon.xyz/tags/CHR" class="mention hashtag" rel="nofollow noopener" target="_blank">#CHR</a> <a href="https://mathstodon.xyz/tags/Constraint" class="mention hashtag" rel="nofollow noopener" target="_blank">#Constraint</a> <a href="https://mathstodon.xyz/tags/Constraints" class="mention hashtag" rel="nofollow noopener" target="_blank">#Constraints</a> <a href="https://mathstodon.xyz/tags/Emacs" class="mention hashtag" rel="nofollow noopener" target="_blank">#Emacs</a> <a href="https://mathstodon.xyz/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalVerification</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#LogicProgramming</a> <a href="https://mathstodon.xyz/tags/MachineLearning" class="mention hashtag" rel="nofollow noopener" target="_blank">#MachineLearning</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/NLP" class="mention hashtag" rel="nofollow noopener" target="_blank">#NLP</a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="nofollow noopener" target="_blank">#Prolog</a>

José A. AlonsoA proof of the Schröder-Bernstein theorem in ACL2. ~ Grant Jurgensen. <a href="https://grantjurgensen.com/posts/schroder-berstein-acl2/" rel="nofollow noopener" translate="no" target="_blank">https://grantjurgensen.com/posts/schroder-berstein-acl2/</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#ACL2</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

Recent searches

Search options

Administered by:

Server stats:

#acl2