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

• Lecturas compartidas el 9 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Relación entre los índices de las subsucesiones y de la sucesión". #ITP #Lean4 #IsabelleHOL #Math
• On non-triviality of the hierarchy of decreasing Church-Rosser abstract rewriting systems. ~ Ievgen Ivanov. #ITP #IsabelleHOL
• Formalization of the filter extension principle (FEP) in Coq. ~ Guowei Dou, Wensheng Yu. #ITP #Coq
• Binding contexts as partitionable multisets in Abella. ~ Terrance Gray, Gopalan Nadathur. #ITP #Abella
• A Beluga formalization of the Harmony Lemma in the π-calculus. ~ Gabriele Cecilia, Alberto Momigliano. #ITP #Beluga
• Confluence by the Z-property for De Bruijn’s λ-calculus with nameless dummies, based on PLFA∗. ~ Vincent van Oostrom. #ITP #Agda
• Verifying peephole rewriting in SSA compiler IRs. ~ Siddharth Bhat, Alex Keizer, Chris Hughes, Andrés Goens, Tobias Grosser. #ITP #Lean4
• Moca 0.3: A first-order theorem prover for Horn clauses. ~ Yusuke Oi, Nao Hirokawa, Teppei Saito. #Haskell #ATP #Logic