Readings shared May 9, 2025
The readings shared in Bluesky on 9 May 2025 are
- Proof assistants for teaching: A survey. ~ Frédéric Tran Minh, Laure Gonnord and Julien Narboux. #ATP #ITP #IsabelleHOL #LeanProver #Coq #Rocq #Education
- Maths with Coq in L1, a pedagogical experiment. ~ Marie Kerjean, Micaela Mayero and Pierre Rousselin. #ITP #Coq #Rocq #Logic #Math #Teaching
- Teaching divisibility and binomials with Coq. ~ Sylvie Boldo, François Clément, David Hamelin, Micaela Mayero and Pierre Rousselin. #ITP #Coq #Rocq #Math #Teaching
- A graphical interface for category theory proofs in Coq. ~ Luc Chabassier. #ITP #Coq #Rocq #CategoryTheory
- OnlineProver: Experience with a visualisation tool for teaching formal proofs. ~ Ján Perháč et als. #ITP #Logic #Teaching
- Minimal sequent calculus for teaching first-order logic: Lessons learned. ~ Jørgen Villadsen. #ITP #IsabelleHOL #Logic #Teaching
- ProofBuddy (How it started, how it's going). ~ Nadine Karsten, Kim Jana Eiken, Uwe Nestmann. #ITP #IsabelleHOL #Logic #Teaching
- Lean4 machine assisted proof framework for chip firing game & graphical Riemann-Roch. ~ Dhyey Dharmendrakumar Mavani. #ITP #LeanProver
- Modelling and verifying neuronal archetypes in Coq. ~ Abdorrahim Bahrami, Rébecca Zucchini, Elisabetta De Maria, Amy Felty. #ITP #Coq #Rocq
- Analyzing API design via algebraic laws. ~ Sandy Maguire. #Haskell #FunctionalProgramming
- Beginnings of a Haskell game engine. ~ Mitchell Vitez. #Haskell #FunctionalProgramming
- Scrap your iteration combinators. ~ Tom Ellis. #Haskell #FunctionalProgramming
- From Haskell to a new structured combinator processor. ~ Yukang Xie et als. #Haskell #FunctionalProgramming
- Lógicas de orden superior y verificación formal. ~ Lourdes del Carmen González Huesca. #Logic #Math #Haskell #FunctionalProgramming #ITP #Coq #Rocq
- Lógicas de orden superior y verificación formal (Slides). ~ Lourdes del Carmen González Huesca. #Logic #Math #Haskell #FunctionalProgramming #ITP #Coq #Rocq