banner
LightNews
jalonso.bsky.social
José A. Alonso
@jalonso.bsky.social
1.7K followers 660 following 4.9K posts
Mathematician interested in the study and teaching of computational logic, functional programming and interactive theorem proving. Homepage: https://jaalonso.github.io Sevilla, Spain
jaalonso.github.io
Posts Media Videos Starter Packs
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 5h
Verifying the functional correctness of Braun trees with LiquidHaskell. ~ Felipe de León, Alberto Pardo, Marcos Viera. systemf.epfl.ch/etc/vstte202... #Haskell #FunctionalProgramming #LiquidHaskell
1 1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 5h
Rely-guarantee verification of queue locks with proof support in Isabelle/HOL. ~ Robert J. Colvin, Scott Heiner, Peter Höfner, Roger C. Su. systemf.epfl.ch/etc/vstte202... #ITP #IsabelleHOL
1 1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 5h
Separation logics for probability, concurrency, and security. ~ Kwing Hei Li. dl.acm.org/doi/abs/10.1... #ITP #Rocq
Separation Logics for Probability, Concurrency, and Security | Companion Proceedings of the 2025 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity
You will be notified whenever a record that you have chosen has been cited.
dl.acm.org
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 5h
Formal verification of Graham’s scan algorithm. ~ Yingjun Lan, Yuxuan Sun. dl.acm.org/doi/abs/10.1... #ITP #Rocq
Formal Verification of Graham’s Scan Algorithm | Companion Proceedings of the 2025 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity
dl.acm.org
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 5h
How much is in a square? Calculating functional programs with squares. ~ Jose Nuno Oliveira. lmf.di.uminho.pt/Ibex/oliveir... #Haskell #FunctionalProgramming
1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 5h
Formalizando um teorema de classificação para álgebras de Lie solúveis de baixa dimensão em Lean. ~ Gustavo Infanti, Viviana del Barco, Exequiel Rivas, Paul Schwahn. prp.unicamp.br/inscricao-co... #ITP #LeanProver #Math
1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 5h
#MULCIA: PhD positions in Mathematical Foundations of Computation Group at Bath. tinyurl.com/287yg995 #PhD #CompSci
1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 5h
Mechanizing Olver's error arithmetic. ~ Max Fan, Ariel E. Kellison and Samuel D. Pollard. doi.org/10.4204/EPTC... #ITP #Rocq
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 5h
Formal verification of COO to CSR sparse matrix conversion. ~ Andrew W. Appel. cgi.cse.unsw.edu.au/~eptcs/paper... #ITP #CoqProver
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 6h
DRIFT: Decompose, retrieve, illustrate, then formalize theorems. ~ Meiru Zhang, Philipp Borchert, Milan Gritta, Gerasimos Lampouras. arxiv.org/abs/2510.10815 #AI #Math #LLMs #ITP #LeanProver
DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems
Automating the formalization of mathematical statements for theorem proving remains a major challenge for Large Language Models (LLMs). LLMs struggle to identify and utilize the prerequisite mathemati...
arxiv.org
1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 6h
Books to recommend to maths students. ~ Katie Steckles. aperiodical.com/2025/10/book... #Math
Books to Recommend to Maths Students
Image by Hermann Traub from Pixabay I was asked recently by a first-year maths undergrad student if I could recommend any books on problem-solving, as they were hoping to develop their problem-solv…
aperiodical.com
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 6h
McTT: A verified kernel for a proof assistant. ~ Junyoung Jang, Antoine Gaulin, Jason Z. S. Hu, Brigitte Pientka. dl.acm.org/doi/10.1145/... #ITP #Rocq #OCaml #FunctionalProgramming
McTT: A Verified Kernel for a Proof Assistant | Proceedings of the ACM on Programming Languages
Proof assistants based on type theories have been widely successful from verifying safety-critical software to establishing a new standard of rigour by formalizing mathematics. But these proof assistants and even their type-checking kernels are also ...
dl.acm.org
1 3
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 6h
"La pereza es la madre de la filosofía. Solo cuando el hombre se sienta a descansar empieza a pensar en el sentido de la vida." ~ Lin Yutang (1895-1975).
1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 6h
Readings shared October 14, 2025. jaalonso.github.io/vestigium/po... #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #Python #RustLang #SetTheory
Readings shared October 14, 2025
The readings shared in Bluesky on 14 October 2025 are: Formally verified certification of unsolvability of temporal planning problems. ~ David Wang, Mohammad Abdulaziz. #ITP #IsabelleHOL A formalizat
jaalonso.github.io
1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 1d
ZF style set theory in Knuckledragger I. ~ Philip Zucker. www.philipzucker.com/zf_knuckle1/ #Python #Logic #SetTheory
ZF style set theory in Knuckledragger I
Zermelo-Fraenkel set theory is a theory of sets.
www.philipzucker.com
2
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 1d
Formally verified certification of unsolvability of temporal planning problems. ~ David Wang, Mohammad Abdulaziz. arxiv.org/abs/2510.10189 #ITP #IsabelleHOL
Formally Verified Certification of Unsolvability of Temporal Planning Problems
We present an approach to unsolvability certification of temporal planning. Our approach is based on encoding the planning problem into a network of timed automata, and then using an efficient model c...
arxiv.org
1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 1d
A gentle introduction to the axiom of choice. ~ Andreas Blass, Dhruv Kulshreshtha. arxiv.org/abs/2509.01830 #Math #SetTheory
A Gentle Introduction to the Axiom of Choice
This article offers a gentle introduction to the axiom of choice. We introduce the axiom, discuss some common objections to it, and present three kinds of reasons to accept it. Although the exposition...
arxiv.org
2 4
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 1d
A formalization of the generalized quantum Stein's lemma in Lean. ~ Alex Meiburg, Leonardo A. Lessa, Rodolfo R. Soldati. arxiv.org/abs/2510.08672 #ITP #LeanProver
A Formalization of the Generalized Quantum Stein's Lemma in Lean
The Generalized Quantum Stein's Lemma is a theorem in quantum hypothesis testing that provides an operational meaning to the relative entropy within the context of quantum resource theories. Its origi...
arxiv.org
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 1d
Making change: Array-based dynamic programming. ~ James Bowen. mmhaskell.com/blog/2025/10... #Haskell #FunctionalProgramming #RustLang
1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 1d
"El arte de vivir consiste en saber sacar placer de las cosas más sencillas: una taza de té, un libro viejo, una conversación con un amigo." ~ Lin Yutang (1895-1975).
1
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 1d
Readings shared October 13, 2025. jaalonso.github.io/vestigium/po... #Agda #CoqProver #Erlang #FunctionalProgramming #Haskell #ITP #LeanProver #Math #OCaml #PVS #Programming #Python #Rocq
Readings shared October 13, 2025
The readings shared in Bluesky on 13 October 2025 are: PVS formalization of proofs of the infinitude of primes. ~ Bruno Berto de Oliveira Ribeiro. #ITP #PVS #Math Certified decision procedures for wi
jaalonso.github.io
3
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 2d
An empirical evaluation of property-based testing in Python. ~ Savitha Ravi, Michael Coblenz. dl.acm.org/doi/10.1145/... #Python #Programming
An Empirical Evaluation of Property-Based Testing in Python | Proceedings of the ACM on Programming Languages
Property-based testing (PBT) is a testing methodology with origins in the functional programming community. In recent years, PBT libraries have been developed for non-functional languages, including Python. However, to date, there is little evidence ...
dl.acm.org
2 2
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 2d
Proof repair across quotient type equivalences. ~ Cosmo Viola, Max Fan, Talia Ringer. dl.acm.org/doi/10.1145/... #ITP #Rocq
Proof Repair across Quotient Type Equivalences | Proceedings of the ACM on Programming Languages
Proofs in proof assistants like Rocq can be brittle, breaking easily in response to changes. To address this, recent work introduced an algorithm and tool in Rocq to automatically repair broken proofs in response to changes that correspond to type ...
dl.acm.org
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 2d
Incremental certified programming. ~ Tomás Díaz, Kenji Maillard, Nicolas Tabareau, Éric Tanter. dl.acm.org/doi/10.1145/... #ITP #Rocq
Incremental Certified Programming | Proceedings of the ACM on Programming Languages
Certified programming, as carried out in proof assistants and dependently-typed programming languages, ensures that a software meets its requirements by supporting the definition of both specifications and proofs. However, proofs easily break with ...
dl.acm.org
jalonso.bsky.social
José A. Alonso @jalonso.bsky.social · 2d
Pyrosome: Verified compilation for modular metatheory. ~ Dustin Jamner, Gabriel Kammer, Ritam Nag, Adam Chlipala. dl.acm.org/doi/10.1145/... #ITP #CoqProver
Pyrosome: Verified Compilation for Modular Metatheory | Proceedings of the ACM on Programming Languages
We present Pyrosome, a generic framework for modular language metatheory that embodies a novel approach to extensible semantics and compilation, implemented in Coq. Common techniques for semantic reasoning are often tied to the specific structures of the ...
dl.acm.org