Readings shared January 3, 2025
The readings shared in Bluesky on 3 January 2025 are
- Readings shared January 2, 2025. #Haskell #Python #Math
- #Exercitium: Mayor órbita de la sucesión de Collatz. #Haskell #Python #Matemáticas
- Proofs of the Nicomachus’s theorem in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
- Décomposition algébrique cylindrique en Coq/Rocq. ~ Quentin Vermande. #ITP #Coq #Rocq #Math
- Formalizing adhesive category theory in Rocq. ~ Samuel Arsac, Russell Harmer, Damien Pous. #ITP #Rocq
- Vérification de bout en bout d’une fonction de bibliothèque mathématique. ~ Paul Geneau de Lamarlière. #ITP #Coq #Rocq #Math
- Safe external calls from formally verified functional code: exiting the monad, and a BDD case study. ~ David Monniaux, Sylvain Boulmé. #ITP #Coq #Rocq
- Modular probabilistic programming with algebraic effects. ~ Oliver Goldstein, Ohad Kammar. #Haskell #FunctionalProgramming
- Parallel QuickHull algorithm in Haskell. ~ George Morgulis, Henry Lin. #Haskell #FunctionalProgramming
- Parallel SAT solver. ~ Yixuan Li, Jiaqian Li, Phoebe Wang. #Haskell #FunctionalProgramming
- Storable types: free, absorbing, custom. ~ Basile Clément, Camille Noûs, Gabriel Scherer. #OCaml #FunctionalProgramming
- Typechecking of overloading in programming languages and mechanized mathematics. ~ Arthur Charguéraud, Martin Bodin, Louis Riboulet. #OCaml #FunctionalProgramming
- Applying machine learning to number-theoretical data (A focus on class groups of imaginary quadratic fields). ~ Hugo Sträng. #AI #MachineLearning #Math