José A. Alonso
LightNews LightNews
banner
jalonso.bsky.social
José A. Alonso
@jalonso.bsky.social
1.7K followers 670 following 5.2K posts
Mathematician interested in the study and teaching of computational logic, functional programming and interactive theorem proving.

Homepage: https://jaalonso.github.io

Sevilla, Spain
Posts Replies Media Videos
jalonso.bsky.social
#Exercitium: Repetición cíclica. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional
November 16, 2025 at 6:45 PM
jalonso.bsky.social
SITA: A framework for structure-to-instance theorem autoformalization. ~ Chenyi Li, Wanli Ma, Zichen Wang, Zaiwen Wen. arxiv.org/abs/2511.10356 #AI #Math #Autoformalization #LLMs #ITP #LeanProver
SITA: A Framework for Structure-to-Instance Theorem Autoformalization
While large language models (LLMs) have shown progress in mathematical reasoning, they still face challenges in formalizing theorems that arise from instantiating abstract structures in concrete setti...
arxiv.org
November 16, 2025 at 1:15 PM
jalonso.bsky.social
"La costumbre es una segunda naturaleza que destruye la primera. Pero ¿qué es naturaleza? ¿Por qué la costumbre no es natural? Tengo mucho miedo de que esta naturaleza no sea a su vez sino una primera costumbre, al igual que la costumbre es una segunda naturaleza." ~ B. Pascal. tinyurl.com/277hu84e
Pensamientos - Pascal : Pascal : Free Download, Borrow, and Streaming : Internet Archive
Pensamientos, por B. PascalPascal produce su obra en pleno triunfo del racionalismo cartesiano, y también en plena controversia teológica determinada por la...
tinyurl.com
November 16, 2025 at 12:45 PM
jalonso.bsky.social
#Exercitium: Elemento común en la menor posición. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas
November 15, 2025 at 6:39 PM
jalonso.bsky.social
"El hombre juicioso sólo piensa en sus males cuando ello conduce a algo práctico; todos los demás momentos los dedica a otras cosas." ~ Bertrand Russell (1872-1970).
November 15, 2025 at 10:07 AM
jalonso.bsky.social
Readings shared November 14, 2025. jaalonso.github.io/vestigium/po... #AI #Agda #AlphaProof #CoqProver #FunctionalProgramming #Haskell #ITP #LeanProver #Math #OCaml #Rocq
Readings shared November 14, 2025
The readings shared in Bluesky on 14 November 2025 are: An introduction to formal real analysis (Lecture 18: Rearrangements). ~ Alex Kontorovich. #ITP #LeanProver #Math Choice trees: Representing and
jaalonso.github.io
November 15, 2025 at 10:06 AM
jalonso.bsky.social
#Exercitium: Cuantificadores sobre listas. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional
November 14, 2025 at 7:26 PM
jalonso.bsky.social
An introduction to formal real analysis (Lecture 18: Rearrangements). ~ Alex Kontorovich. youtu.be/VI63OwWMxJM #ITP #LeanProver #Math
Lecture 18, Introduction to Formal Real Analysis, Rutgers University, Prof. Kontorovich, 11/11/2025
YouTube video by Alex Kontorovich
youtu.be
November 14, 2025 at 6:22 PM
jalonso.bsky.social
The Haskell Unfolder Episode 51: Typed servers using sop-core. ~ Edsko de Vries, Andres Löh. www.youtube.com/live/3XeIoA0... #Haskell #FunctionalProgramming
Typed servers using sop-core (Haskell Unfolder #51)
YouTube video by Well-Typed
www.youtube.com
November 14, 2025 at 6:17 PM
jalonso.bsky.social
The Haskell Unfolder Episode 50: Singletons. ~ Edsko de Vries, Andres Löh. www.youtube.com/live/-zxxl-W... #Haskell #FunctionalProgramming
Singletons (Haskell Unfolder #50)
YouTube video by Well-Typed
www.youtube.com
November 14, 2025 at 6:16 PM
jalonso.bsky.social
The Haskell Unfolder Episode 49: Shrinking. ~ Edsko de Vries, Andres Löh. www.youtube.com/live/EcV4rb-... #Haskell #FunctionalProgramming
Shrinking (Haskell Unfolder #49)
YouTube video by Well-Typed
www.youtube.com
November 14, 2025 at 6:16 PM
jalonso.bsky.social
#MULCIA: Postdoc positions in formal methods and programming languages (The Centre for Formal Methods and Future Computing (FORM) at the Department of Mathematics and Computer Science, University of Southern Denmark). tinyurl.com/25blteat #PostDoc #CompSci
Postdoc Positions in Formal Methods and Programming Languages
Application deadline: 11 January 2025 at 23:59 hours local Danish time
tinyurl.com
November 14, 2025 at 4:45 PM
jalonso.bsky.social
Patterns and paradoxes: The logic of pattern synonyms. ~ Koz Ross. www.mlabs.city/blog/pattern... #Haskell #FunctionalProgramming
Patterns and Paradoxes: The Logic of Pattern Synonyms — Mlabs.city
Learn how Haskell pattern synonyms and view patterns decouple interface from representation, deliver packed-data performance, preserve exhaustiveness, support bidirectional/read-only views, and more.
www.mlabs.city
November 14, 2025 at 4:35 PM
jalonso.bsky.social
How we achieved an IMO medal, one year before any other AI system. ~ Tom Zahavy. www.tomzahavy.com/post/how-we-... #AI #Math #ITP #LeanProver #AlphaProof
How we achieved an IMO medal, one year before any other AI system
It has been over a year since AlphaProof achieved silver-medal standard solving International Mathematical Olympiad (IMO) problems, by teaching itself mathematics in LEAN. This milestone was special t...
www.tomzahavy.com
November 14, 2025 at 1:14 PM
jalonso.bsky.social
A practical formalization of monadic equational reasoning in dependent-type theory. ~ Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. www.cambridge.org/core/journal... #ITP #CoqProver
A practical formalization of monadic equational reasoning in dependent-type theory | Journal of Functional Programming | Cambridge Core
A practical formalization of monadic equational reasoning in dependent-type theory - Volume 35
www.cambridge.org
November 14, 2025 at 12:52 PM
jalonso.bsky.social
You could have invented Fenwick trees. ~ Brent Yorgey. www.cambridge.org/core/journal... #Haskell #FunctionalProgramming
You could have invented Fenwick trees | Journal of Functional Programming | Cambridge Core
You could have invented Fenwick trees - Volume 35
www.cambridge.org
November 14, 2025 at 12:50 PM
jalonso.bsky.social
Experiences of early assessment to teach functional programming. ~ Peter Chapman. www.cambridge.org/core/journal... #Haskell #FunctionalProgramming
Experiences of early assessment to teach functional programming | Journal of Functional Programming | Cambridge Core
Experiences of early assessment to teach functional programming - Volume 35
www.cambridge.org
November 14, 2025 at 12:48 PM
jalonso.bsky.social
How much is in a square? Calculating functional programs with squares. ~ Jose Nuno Oliveira. www.cambridge.org/core/journal... #Haskell #FunctionalProgramming
How much is in a square? Calculating functional programs with squares | Journal of Functional Programming | Cambridge Core
How much is in a square? Calculating functional programs with squares - Volume 35
www.cambridge.org
November 14, 2025 at 12:45 PM
jalonso.bsky.social
Domain-specific tensor languages. ~ Jean-Philippe Bernardy, Patrik Jansson. www.cambridge.org/core/journal... #Haskell #FunctionalProgramming
Domain-specific tensor languages | Journal of Functional Programming | Cambridge Core
Domain-specific tensor languages - Volume 35
www.cambridge.org
November 14, 2025 at 12:41 PM
jalonso.bsky.social
Binary search—think positive. ~ Alexander Dinges, Ralf Hinze. www.cambridge.org/core/journal... #ITP #Agda
Binary search—think positive | Journal of Functional Programming | Cambridge Core
Binary search—think positive - Volume 35
www.cambridge.org
November 14, 2025 at 12:39 PM
jalonso.bsky.social
Parallel dual-numbers reverse AD. ~ Tom J. Smeding, Matthijs I.L. Vákár. www.cambridge.org/core/journal... #Haskell #FunctionalProgramming
Parallel dual-numbers reverse AD | Journal of Functional Programming | Cambridge Core
Parallel dual-numbers reverse AD - Volume 35
www.cambridge.org
November 14, 2025 at 12:32 PM
jalonso.bsky.social
Automatically testing console I/O behavior of student submissions in Haskell. ~ Oliver Westphal, Janis Voigtländer. www.cambridge.org/core/journal... #Haskell #FunctionalProgramming
Automatically testing console I/O behavior of student submissions in Haskell | Journal of Functional Programming | Cambridge Core
Automatically testing console I/O behavior of student submissions in Haskell - Volume 35
www.cambridge.org
November 14, 2025 at 12:28 PM
jalonso.bsky.social
Checking equivalence in a non-strict language. ~ John Charles Kolesar, Ruzica Piskac, William Triest Hallahan. www.cambridge.org/core/journal... #Haskell #FunctionalProgramming
Checking equivalence in a non-strict language | Journal of Functional Programming | Cambridge Core
Checking equivalence in a non-strict language - Volume 35
www.cambridge.org
November 14, 2025 at 12:25 PM
jalonso.bsky.social
Towards type-directed compiler calculation. ~ Wouter Swierstra. www.cambridge.org/core/journal... #ITP #Agda
Towards type-directed compiler calculation | Journal of Functional Programming | Cambridge Core
Towards type-directed compiler calculation - Volume 35
www.cambridge.org
November 14, 2025 at 12:21 PM
jalonso.bsky.social
Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq. ~ Nicolas Chappe et als. www.cambridge.org/core/journal... #ITP #Rocq
Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq | Journal of Functional Programming | Cambridge Core
Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq - Volume 35
www.cambridge.org
November 14, 2025 at 12:15 PM