The readings shared in Mastodon on August 22, 2024 are

• Readings shared August 21, 2024. #ITP #IsabelleHOL #Lean4 #Math #FunctionalProgramming
• Terminal coalgebras and non-wellfounded sets in Homotopy Type Theory. ~ Håkon Robbestad Gylterud, Elisabeth Stenholm & Niccolò Veltri. #ITP #Agda #HoTT
• Prettier. Happier. More Imperative. (Understanding "A prettier printer" by porting it). ~ Benjamin Hodgson. #Haskell #FunctionalProgramming

The readings shared in Mastodon on August 21, 2024 are

• Readings shared August 20, 2024. #ITP #Lean4 #Coq #ACL2 #AlphaProof #Math #Haskell #FunctionalProgramming #Logic #Math #CategoryTheory #TypeTheory
• Probabilistic reasoning and formal proof. ~ Lawrence Paulson (@LawrPaulson@mathstodon.xyz). #ITP #IsabelleHOL #Math
• Writing a small program with input and output in the Lean functional programming language. ~ Adolfo Neto (@adolfoneto@bertha.social). #Lean4 #FunctionalProgramming
• Worklist algorithms (in Isabelle/HOL). ~ Simon Wimmer & Peter Lammich. #ITP #IsabelleHOL
• Trustworthy verification of realtime systems. ~ Simon Wimmer. #ITP #IsabelleHOL
• Verified model checking of timed automata. ~ Simon Wimmer & Peter Lammich. #ITP #IsabelleHOL

The readings shared in Mastodon on August 20, 2024 are

• Readings shared August 18, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Math #Calculemus
• Improving on AlphaProof: IMO 2024 problem 2 in Lean 4. ~ David Renshaw. #ITP #Lean4 #Math #AlphaProof
• Verification and attack synthesis for network protocols. ~ Max von Hippel. #ITP #ACL2
• A two-phase infinite/finite low-level memory model (Reconciling integer–pointer casts, finite space, and undef at the LLVM IR level of abstraction). ~ Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski & Steve Zdancewic. #ITP #Coq
• Snapshoble stores. ~ Clément Allain, Basile Clément, Alexandre Moine & Gabriel Scherer. #ITP #Coq
• Refinement composition logic. ~ Youngju Song & Dongjae Lee. #ITP #Coq
• Beyond trees: Calculating graph-based compilers (Functional pearl). ~ Patrick Bahr & Graham Hutton. #Haskell #FunctionalProgramming
• An introduction to categorical proof theory. ~ Amirhossein Akbar Tabatabai. #Logic #Math #CategoryTheory #TypeTheory

The readings shared in Mastodon on August 18, 2024 are

• Readings shared August 18, 2024. #ITP #LeanProver #Lean4 #FunctionalProgramming #Math #Prolog #LogicProgramming
• Proofs of the equivalence of reverse definitions in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• A formalisation of the Mathieu-24 group. ~ Edward van de Meent. #ITP #LeanProver #Lean4 #Math

The readings shared in Mastodon on August 18, 2024 are

• Readings shared August 17, 2024. #ITP #LeanProver #Lean4 #Math #AI
• How the Lean language brings math to coding and coding to math. ~ Leo de Moura. #ITP #LeanProver #Math
• Lean again. ~ Adolfo Neto (@adolfoneto@bertha.social). #ITP #Lean4 #FunctionalProgramming
• The semantics of metapropramming in Prolog. ~ David S. Warren. #Prolog #LogicProgramming

The readings shared in Mastodon on August 18, 2024 are

• Readings shared August 15, 2024. #ITP #IsabelleHOL #Coq #SSReflect #Math #Haskell #Elm #FunctionalProgramming
• Machine-checked proofs and the rise of formal methods in mathematics. ~ Leonardo de Moura. #ITP #LeanProver #Math
• DeepSeek-Prover-V1.5: Harnessing proof assistant feedback for reinforcement learning and Monte-Carlo tree search. ~ Huajian Xin et als. #ITP #Lean4
• The AI scientist: Towards fully automated open-ended scientific discovery. ~ Chris Lu, Cong Lu, Robert Tjarko Lange, Jakob Foerster, Jeff Clune & David Ha. #AI

The readings shared in Mastodon on August 15, 2024 are

• Readings shared August 14, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Math #AI #MachineLearning
• Software verification with Isabelle/HOL. ~ Peter Höfner. #ITP #IsabelleHOL
• Functional algorithms verified in SSReflect. ~ Alex Gryzlov et als. #ITP #Coq #SSReflect
• Haskell for Elm developers: giving names to stuff (Part 5 - Semigroups and Monoids). ~ Flavio Corpa (@FlavioCorpa). #Haskell #Elm #FunctionalProgramming
• The Haskell Unfolder Episode 31: nothunks. ~ Edsko de Vries (@EdskoDeVries), Andres Löh (@kosmikus@functional.cafe). #Haskell #FunctionalProgramming
• Galois theory. ~ Tom Leinster. #Math

The readings shared in Mastodon on August 14, 2024 are

• Readings shared August 13, 2024. #ITP #Coq #Agda #Math #Python
• #Calculemus: Proofs with Lean4 and Isabelle/HOL of "take n xs ++ drop n xs = xs". #ITP #Lean4 #IsabelleHOL #Math
• Introduction to proofs with Lean proof assistant. ~ Sina Hazratpour (@sina_htpr). #ITP #LeanProver
• Taller de Lean 4. ~ Enric Cosme, Mario Vago. #ITP #LeanProver #Lean4
• A topological approach for semi-supervised learning. ~ Adrián Inés, César Domínguez, Jónathan Heras, Gadea Mata & Julio Rubio. #AI #MachineLearning #Math

The readings shared in Mastodon on August 13, 2024 are

• Readings Shared August 13, 2024. #Python #Haskell #FunctionalProgramming
• An elementary proof of the FMP for Kleene algebra. ~ Tobias Kappé. #ITP #Coq #Math
• Sharing proofs with predicative theories through universe-polymorphic elaboration. ~ Thiago Felicissimo & Frédéric Blanqui. #ITP #Agda #Coq
• Bounding Euler's constant. ~ Philip Zucker (@sandmouth@types.pl). #Math #Python
• Algebra. It's powerful. But it's not what it was. ~ Keith Devlin (@KeithDevlin@fediscience.org). #Math

Las lecturas compartidas en Mastodon el 10 de agosto de 2024 son

• Lecturas compartidas el 9 de agosto de 2024. #ITP #IsabelleHOL #LeanProver #HOL4 #Coq #Math #Haskell #FunctionalProgramming #IA
• Function composition and currying in Python (Python in the streets, Haskell in the sheets!). ~ Francisco Gutierrez. #Python #Haskell #FunctionalProgramming