Lecturas compartidas el 16 de abril de 2024
#ITP #Lean4 #IsabelleHOL #Coq #HOL_Light #SMT #Haskell #Python #Logic #Math #CompSci
Buenos días
Las lecturas compartidas en Mastodon el 16 de abril de 2024 son
Lecturas compartidas el 15 de abril de 2024. #ITP #Lean4 #IsabelleHOL #Coq #PVS #FunctionalProgramming #Haskell #Math #AI #Education
#Calculemus: Demostraciones con Lean4 e Isabelle/HOL: "f[s] \ f[t] ⊆ f[s \ t]". #ITP #LeanProver #Lean4 #IsabelleHOL #Matemáticas
#Exercitium: Máxima suma de caminos en un triángulo. #Haskell #Python #Matemáticas
Logic in mathematics and computer science. ~ Richard Zach (@rrrichardzach@mathstodon.xyz). #Logic #Math #CompSci
IsaRare: Automatic verification of SMT rewrites in Isabelle/HOL. ~ Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark Barrett & Cesare Tinelli. #ITP #IsabelleHOL #SMT
Protein folding by recursive backtracking. ~ Bjørn Kjos-Hanssen. #ITP #Lean4
Live verification in an interactive proof assistant. ~ Samuel Gruetter, Viktor Fukala, Adam Chlipala. #ITP #Coq
A state-of-the-art Karp-Miller algorithm certified in Coq. ~ Thibault Hilaire, David Ilcinkas & Jérôme Leroux. #ITP #Coq
Foundational integration verification of a cryptographic server. ~ Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Clément Pit-Claudel & Adam Chlipala. #ITP #Coq
Asymptotics for the standard block size in primal lattice attacks: second order, formally verified. ~ Daniel J. Bernstein. #ITP #HOL_Light
También están en GitHub.
Saludos, José A.
"Se necesita muy poco para tener una vida feliz; todo está dentro de ti, en tu forma de pensar." ~ Marco Aurelio (121-180).