screwlispJun 13

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.

José A. AlonsoMay 23
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
Readings shared May 22, 2025

The 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

Vestigium
José A. AlonsoMay 22
A formalization of elementary linear algebra: Part I. ~ David M. Russinoff. https://www.russinoff.com/papers/linear1.pdf #ITP #ACL2 #Math
José A. AlonsoMay 22
Readings shared May 21, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/21-readings_shared_05-21-25 #ACL2 #AI #AlphaEvolve #CommonLisp #CompSci #Emacs #GeneticAlgoritm #ITP #LLMs #LeanProver #Math #OrgMode #Programming #Python
Readings shared May 21, 2025

The readings shared in Bluesky on 21 May 2025 are Will computers prove theorems? ~ Kevin Buzzard. #ITP #LeanProver #Math Formalizing the future: Lean’s impact on mathematics, programming, and AI. ~ L

Vestigium
José A. AlonsoMay 21
A formalization of the correctness of the Floodsub protocol. ~ Ankit Kumar, Panagiotis Manolios. https://ankitku.github.io/stuff/floodsub-acl2ws.pdf #ITP #ACL2
José A. AlonsoMay 5
Readings shared May 4, 2025. https://jaalonso.github.io/vestigium/posts/2025/05/04-readings_shared_05-04-25 #ACL2 #Coq #FunctionalProgramming #Haskell #ITP #Math #Rocq
Readings shared May 4, 2025

The readings shared in Bluesky on 4 May 2025 are Formalizing resource ownership semantics of spinlocks with the Coq proof assistant. ~ Sebastian Luis S. Ortiz et als. #ITP #Coq #Rocq Formalizing reve

Vestigium
José A. AlonsoMay 4
Formal verification of blockchain nonforking in DAG-based BFT consensus with dynamic stake. ~ Alessandro Coglio, Eric McCarthy. https://alessandrocoglio.info/techrep-2025-aleobft.pdf #ITP #ACL2
Frank’s TingApr 16
Oh well unlike Corica, Ufuk (off) won’t get to leave having just won a trophy. Go and play your Strategically flawed football with inflexible tactics some where else #SydneyIsSkyBlue #mastodonfc #ACL2
Frank’s TingApr 9
Now the idiot brings Sega on. Honestly I had Roy Hodgson coaching #LFC one time and that drove me spare, but Talay at Sydney is running it close. #ACL2
Frank’s TingApr 9
I’m sure Ufuk Talay will tell us that this is all part of his plan and we shouldn’t worry that he keeps coaching like a fella looking for hairs on the palm of his hand. #SydneyIsSkyBlue #ACL2 #mastodonfc