Las lecturas compartidas en Mastodon el 19 de mayo de 2024 son

• Lecturas compartidas el 18 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Agda #Physics #Math #Programming #Python
• Libro "Calculemus (Demostraciones con Lean4)" (versión 18-mayo-24). #ITP #Lean4 #Math
• #Exercitium: Diferencia simétrica. #Haskell #Python #Matemáticas
• Bridging syntax and semantics of Lean expressions in E-Graphs. ~ Marcus Rossel and Andrés Goens. #ITP #Lean4
• PSPSP: A tool for automated verification of stateful protocols in Isabelle/HOL. ~ Andreas Viktor Hess, Sebastian Alexander Mödersheim, Achim D. Brucker and Anders Schlichtkrull. #ITP #IsabelleHOL
• Metamathematics. ~ David Marker. #Logic #Math

Las lecturas compartidas en Mastodon el 18 de mayo de 2024 son

• Lecturas compartidas el 17 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Math
• La semana en Calculemus (Demostraciones con Lean4 e Isabelle/HOL) (18-mayo-24). #ITP #Lean4 #IsabelleHOL #Math
• Proofs and conversations. ~ Talia Ringer (@TaliaRinger@mathstodon.xyz). #ITP #Coq #Math
• Functional induction. ~ Joachim Breitner (@nomeata@mastodon.online). #ITP #Lean4
• HepLean: Digitalising high energy physics. ~ Joseph Tooby-Smith. #ITP #Lean4 #Physics
• Foundational verification of smart contracts through verified compilation. ~ Vilhelm Sjöberg, Kinnari Dave, Daniel Britten, Maria A Schett, Xinyuan Sun, Qinshi Wang, Sean Noble Anderson, Steve Reeves, Zhong Shao. #ITP #Coq
• Initial algebras unchained (A novel initial algebra construction formalized in Agda). ~ Thorsten Wißmann and Stefan Milius. #ITP #Agda #Math
• Programming as a mediator of mathematical thinking (Examples from upper secondary students exploring the definite integral). ~ Timo Tossavainen, Claes Johansson, Alf Juhlin and Anna Wedestig. #Math #Programming #Python
• Math databases. ~ Jeremy Kun (@j2kun@mathstodon.xyz). #Math
• code4math: Consortium of digital ecosystems for mathematics. #Math

Las lecturas compartidas en Mastodon el 17 de mayo de 2024 son

• Lecturas compartidas el 16 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Agda #Logic #Math #FunctionalProgramming #Haskell #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces a^(m·n) = (a^m)ⁿ". #ITP #Lean4 #IsabelleHOL #Math

Las lecturas compartidas en Mastodon el 16 de mayo de 2024 son

• Lecturas compartidas el 15 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #PVS #Coq #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si G es un grupo y a, b, c ∈ G tales que a·b = a·c, entonces b = c". #ITP #Lean4 #IsabelleHOL #Math
• Course: Logic in Software Engineering (Lean). ~ Alexander Kurz. #ITP #Lean4 #Logic
• Interactive theorem proving:Introduction to Agda. ~ Jeremy Siek. #ITP #Agda
• Implementing categorical notions of partiality and delay in Agda. ~ Leon Vatthauee. #ITP #Agda #FunctionalProgramming #Haskell
• Evaluating Large Language Model performance on Haskell. ~ Andrew Chen. #LLMs #Haskell #FunctionalProgramming
• The Haskell Unfolder Episode 25: from Java to Haskell. ~ Edsko de Vries (@EdskoDeVries), Andres Löh (@kosmikus@functional.cafe). #Haskell #FunctionalProgramming

Las lecturas compartidas en Mastodon el 15 de mayo de 2024 son

• Lecturas compartidas el 14 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Haskell #Python #Math #Emacs #OrgMode #Elisp #ChatGPT
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si G un grupo y a ∈ G, entonces (a⁻¹)⁻¹ = a". #ITP #Lean4 #IsabelleHOL #Math
• Towards nominal AC-unification. ~ Gabriel Ferreira Silva. #PhDThesis #ITP #PVS
• Multris: Functional verification of multiparty message passing in separation logic. ~ Jonas Kastberg Hinrichsen, Jules Jacobs, Robbert Krebbers. #ITP #Coq

Las lecturas compartidas en Mastodon el 14 de mayo de 2024 son

• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹". #ITP #Lean4 #IsabelleHOL #Math
• #Exercitium: Matrices de Toepliz. #Haskell #Python #Matemáticas
• Schönhage-Strassen multiplication (in Isabelle/HOL). ~ Jakob Schulz. #ITP #IsabelleHOL #Math
• An entry into the world of Org Mode for non Emacs users. ~ James Stoup. #Emacs #OrgMode
• Writing Lisp code with ChatGPT. #Elisp #ChatGPT

Las lecturas compartidas en Mastodon el 13 de mayo de 2024 son

• Lecturas compartidas el 12 de mayo de 2024. #ITP #Lean4 #Agda #Math #FunctionalProgramming #Haskell
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si G un grupo y a, b ∈ G tales que a⋅b = 1, entonces a⁻¹ = b". #ITP #Lean4 #IsabelleHOL #Math

Las lecturas compartidas en Mastodon el 12 de mayo de 2024 son

• Lecturas compartidas el 11 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Agda #Coq #HOL_Light #Metamath #Mizar #Math #Programming #CommonLisp
• Libro "Calculemus (Demostraciones con Lean4)" (versión 11-mayo-24). #ITP #LeanProver #Lean4 #Matemáticas
• A Lean proof of Fermat’s Last Theorem. ~ Kevin Buzzard, Richard Taylor. #ITP #Lean4 #Math
• Agda core: The dream and the reality. ~ Jesper Cockx (@jesper@agda.club) #ITP #Agda
• The ultimate guide to Haskell Strings. ~ Julian Ospald. #FunctionalProgramming #Haskell

Las lecturas compartidas en Mastodon el 11 de mayo de 2024 son

• Lecturas compartidas el 10 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #SAT_solver #FunctionalProgramming #Haskell #Python #Math
• La semana en Calculemus (Demostraciones con Lean4 e Isabelle/HOL) (11-mayo-24). #ITP #Lean4 #IsabelleHOL #Math
• Algorithm and abstraction in formal mathematics. ~ Heather Macbeth. #ITP #Agda #Coq #Lean4 #HOL_Light #IsabelleHOL #Metamath #Mizar #Math
• Course: Formalising Mathematics in Lean. ~ Adrián Doña Mateo, Monica Abu Omar, Patrick Kinnear and Simone Castellan. #ITP #Lean4 #Math
• Course: Formalized Mathematics in Lean (Winter 23/24). ~ Floris van Doorn. #ITP #Lean4 #Math
• Course: Theorem proving with Lean. ~ Damiano Testa. #ITP #Lean4 #Math
• Partial correctness of the top-down solver (in Isabelle/HOL). ~ Yannick Stade, Sarah Tilscher, Helmut Seidl. #ITP #IsabelleHOL
• LL(1) parser generator (in Isabelle/HOL). ~ Sarah Tilscher and Simon Wimmer. #ITP #IsabelleHOL
• How to explore Lisp metaprogramming techniques. #CommonLisp
• The way of Lisp or the right way. ~ Joe Marshall. #Lisp #Programming