José A. Alonso
Mathematician interested in the study and teaching of computational logic, functional programming and interactive theorem proving.
Homepage: https://jaalonso.github.io
Sevilla, Spain
- #MULCIA: Fully-funded PhD in explainable reasoning & argumentative AI, CRIL – Université d'Artois (France). tinyurl.com/23ttkywd #PhD #CompSci
- Verified purely functional catenable real-time deques. ~ Jules Viennot, Arthur Wendling, Armaël Guéneau, François Pottier. arxiv.org/abs/2505.07681 #ITP #Rocq #OCaml
- Formal P-category theory and normalization by evaluation in Rocq. ~ David G. Berry, Marcelo P. Fiore. arxiv.org/abs/2505.07780 #ITP #Rocq #CategoryTheory
- Theorem prover Arend. ~ Fedor Part, Valery Isaev, and Sergey Sinchuk. arend-lang.github.io/assets/lang-... #ITP #Arend
- "Confía en el tiempo, que suele dar dulces salidas a muchas amargas dificultades." ~ Miguel de Cervantes (1547-1616).
- Readings shared May 13, 2025. jaalonso.github.io/vestigium/po... #FunctionalProgramming #AI #ITP #LLMs #LeanProver #Math