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