The readings shared in Mastodon on August 30, 2024 are

• Readings shared August 29, 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math #Calculemus
• Compactness theorem for propositional logic and combinatorial applications. ~ Fabián Fernando Serran Suárez, Thaynara Arielly de Lima & Mauricio Ayala-Rincón. #ITP #IsabelleHOL #Logic #Math
• Law and order for typestate with borrowing. ~ Hannes Saffrich, Yuki Nishida & Peter Thiemann.1# #ITP #Agda
• Getting started with Nix for Haskell. ~ Abhinav Sarkar. #Nix #Haskell #FunctionalProgramming
• Logic programming with extensible types. ~ Ivan Perez & Angel Herranz. #Haskell #FunctionalProgramming #LogicProgramming

The readings shared in Mastodon on August 29, 2024 are

• Readings shared August 28, 2024. #ITP #LeanProver #Lean4 #IsabelleHOL #Coq #Math #Calculemus #AI
• Proofs of the equivalence of two definitions of the Fibonacci function in Lean4 and Isabelle/HOL. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• A residual service curve computable in quadratic time for network calculus. ~ Marc Boyer & Pierre Roux. #ITP #Coq
• Modular verification of intrusive list and tree data structures in separation logic. ~ Marc Hermes & Robbert Krebbers. #ITP #Coq

The readings shared in Mastodon on August 28, 2024 are

• Readings shared August 27, 2024. #ITP #IsabelleHOL #Math
• Proofs of "flatten (mirror a) = reverse (flatten a)" in Lean4 and Isabelle/HOL. ~ José A. Alonso. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• Formalizing Mason-Stothers theorem and its corollaries in Lean 4. ~ Jineon Baek & Seewoo Lee. #ITP #LeanProver #Lean4 #Math
• On the maximum weighted irredundant set problem. ~ Ricardo D. Katz & Daniel Severín. #ITP #Coq #Math
• Compositional verification of composite byzantine protocols. ~ Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, Ilya Sergey. #ITP #Coq
• The top 100 gen AI consumer apps. ~ Olivia Moore. #AI
• Conocimientos de sentido común: el obstáculo de la IA en el camino hacia la inteligencia artificial general. ~ Ramón López de Mántaras. #IA
• Las herramientas de IA que están captando la atención de la gente. ~ @Alvy #IA
• L’intelligence artificielle : Hier, aujourd’hui … et demain. ~ Jean-Paul Haton. #AI

The readings shared in Mastodon on August 27, 2024 are

• Readings shared August 26, 2024. #ITP #Lean4 #IsabelleHOL #Math #Calculemus #Prolog #LogicProgramming
• Topological groups (in Isabelle/HOL). ~ Niklas Krofta. #ITP #IsabelleHOL #Math
• Difference bound matrices (in Isabelle/HOL). ~ Simon Wimmer & Peter Lammich. #ITP #IsabelleHOL

The readings shared in Mastodon on August 26, 2024 are

• Proofs that the mirror function of binary trees is involutive in Lean4 and Isabelle/HOL. ~ José A. Alonso. #ITP #Lean4 #IsabelleHOL #Math #Calculemus
• A formalized programming language with speculative execution. ~ Jamie Wright & Andrei Popescu. #ITP #IsabelleHOL
• Game programming in Prolog (Part 1). ~ Youngjin Kang. #Prolog #LogicProgramming

The readings shared in Mastodon on August 24, 2024 are

• Readings shared August 23, 2024. #ITP #IsabelleHOL #LeanProver #Lean4 #AI #DeepLearning #Haskell #FunctionalProgramming #LogicProgramming #Python
• Logic and computation intertwined. ~ Prabhakar Ragde. #Logic #Racket #ITP #Coq #Agda
• Tipos dependientes: λP. ~ Juan Pablo Yamamoto Zazueta. #TypeTheory #CurryHoward

The readings shared in Mastodon on August 23, 2024 are

• Readings shared August 22, 2024. #ITP #Agda #HoTT #Haskell #FunctionalProgramming
• Lean: First steps (06 - Intermediate results). ~ Tariq Rashid. #ITP #Lean4 #Math
• How to make mathematicians into programmers (and vice versa). ~ Will Crichton. #ITP #LeanProver #Math
• Michael John Caldwell Gordon (FRS 1994), 28 February 1948 - 22 August 2017. ~ Lawrence C Paulson. #ITP #HOL
• Coproduct measure (in Isabelle/HOL). ~ Michikazu Hirata. #ITP #IsabelleHOL #Math
• A survey on deep learning for theorem proving. ~ Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang & Xujie Si. #AI #DeepLearning #ITP
• Property-based testing for the people. ~ Harrison Goldstein. #PhDThesis #Haskell #FunctionalProgramming
• Boolean matrix logic programming. ~ Lun Ai & Stephen H. Muggleton. #LogicProgramming
• Ordinals aren't much worse than Quaternions. ~ Philip Zucker. #Python #Math

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. #ITP #IsabelleHOL #Math
• Writing a small program with input and output in the Lean functional programming language. ~ Adolfo Neto. #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