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

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

• Lecturas compartidas el 9 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #FunctionalProgramming #Haskell #Python #Math #CategoryTheory
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de la unicidad del elemento neutro en los grupos. #ITP #Lean4 #IsabelleHOL #Math
• #Exercitium: Diagonales principales de una matriz. #Haskell #Python #Matemáticas
• Verifying a SAT solver from ground up. ~ Mathias Fleury. #ITP #IsabelleHOL #SAT_solver
• Solving recurrence relations. ~ John Mount. #Python #Math

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

• Lecturas compartidas el 8 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #HOL_Light #Coq #HOL4 #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si M es un monoide cancelativo por la izquierda y a, b ∈ M, entonces a⋅b = a ↔ b = 1". #ITP #Lean4 #IsabelleHOL #Math
• #Exercitium: Posiciones de las diagonales principales. #Haskell #Python #Matemáticas
• Compiling higher order functions with GADTs. ~ Srijan (@_injuly). #FunctionalProgramming #Haskell
• When are functions lazy enough for lists. ~ Daniel Beskin. #FunctionalProgramming #Haskell
• Notes on Category Theory (with examples from basic mathematics). ~ Paolo Perrone. #CategoryTheory

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

• Lecturas compartidas el 7 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Agda #SMT #Logic #Math #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si M es un monoide conmutativo y x, y, z ∈ M tales que x⋅y = 1 y x⋅z = 1, entonces y = z.". #ITP #Lean4 #IsabelleHOL #Math
• Translating HOL-Light proofs to Coq. ~ Frédéric Blanqui. #ITP #HOL_Light #Coq
• HOL4P4: Mechanized small-step semantics for P4. ~ Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam. #ITP #HOL4