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