Esta entrada es una recopilación de lecturas compartidas esta semana (del 24 de mayo al 8 de junio) en la lista de correo del grupo de lógica computacional

La recopilación está ordenada por la fecha de su publicación en Twitter. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.

• Generalized arrows. ~ A. Megacz #Haskell #Coq
• Transitive closure according to Roy-Floyd-Warshall. ~ M. Wenzel #AFP #Isabelle_HOL
• Composing and decomposing data types (A closed type families implementation of data types à la carte). ~ P. Bahr #Haskell
• Formalization of complex vectors in higher-order logic. ~ S. Khan-Afshar et als. #HOL_Light
• Experience report: Type-checking polymorphic units for astrophysics research in Haskell. ~ T. Muranushi & R.A. Eisenberg #Haskell
• Noninterference security in communicating sequential processes. ~ P. Noce #AFP #Isabelle_HOL
• Logic programming as scripting language for bots in computer games: Research overview. ~ G. Jaśkiewicz #Prolog
• The pitfalls of protocol design (Attempting to write a formally verified PDF parser). ~ A. Bogk & M. Schöpl #Coq
• A fully verified executable LTL model checker. ~ J. Esparza et als. #AFP #Isabelle_HOL
• My life with an automatic theorem prover. ~ J.C. Blanchette #Sledgehammer #Isabelle_HOL
• Programming is social. ~ E. Wallingford #Programming
• Don’t learn to code. Learn to think. ~ Y. Brikman
• Some constructions on ω-groupoids. ~ T. Altenkirch, N. Li & O. Rypácek #Agda
• Graphs: a balancing act. ~ mazzo.li #Tutorial #Haskell #Gloss
• Beautiful code, compelling evidence (Functional programming for information visualization and visual analytics). ~ J.R. Heard #Haskell
• Using small scale automation to improve both accessibility and readability of formal proofs in geometry. ~ P. Boutry et als. #Coq
• Computer-aided proof of Erdös discrepancy properties. ~ B. Konev & A. Lisitsa #SAT
• A short note about case distinctions in Tarski’s geometry. ~ P. Boutry et als. #Coq
• Comonads in Haskell. ~ D. Overton [Slides] #Haskell
• Proofs about programs, proofs as programs, and programs as proofs! ~ Katherine Ye #Coq
• Lazy dynamic programming. ~ T. Jelvis #Haskell
• A major upgrade to attoparsec: more speed, more power. ~ B. O’Sullivan #Haskell
• Generating mazes with inductive graphs. ~ T. Jelvis #Haskell
• Monadic parsers: Implementing a micro Parsec. ~ O. Iqbal #Haskell
• Installing GHC and working with Cabal. ~ @ReichertBros [Slides] #Haskell
• Formal verification of control systems’ properties with theorem proving. ~ D. Araiza-Illan et als. #Why3
• Learn physics by programming in Haskell. ~ S.N. Walck #Haskell
• Formalized, effective domain theory in Coq. ~ R. Dockins #Coq
• Course on a mathematical presentation of functional programming. ~ A. Tasistro, J. Michelini & N. Szasz #Haskell
• Hardware design using Haskell and CλaSH. ~ R. Wester, J. Kuper & C. Baaij #Haskell
• System description: Isabelle/jEdit in 2014. ~ M. Wenzel #Isabelle_HOL
• Comonads, life and Klein bottles. ~ Idontgetoutmuch’s Weblog #Haskell

Esta entrada es una recopilación de lecturas compartidas esta semana (del 18 al 24 de mayo) en la lista de correo del grupo de lógica computacional

La recopilación está ordenada por la fecha de su publicación en Twitter. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.

• Formalizing Strand Spaces in Coq: Proving “Proving security protocols correct” correct A. Kent & J. McCarty #Coq
• Do creative-telescoping algorithms provide complete proofs? A formal study of Apéry’s theorem F. Chyzak et als. #Coq
• Formal proofs for nonlinear optimization X. Allamigeon et als. #Coq
• Exact combinational circuit synthesis in Haskell P. Tarau #Haskell
• Generating learning algorithms: Hidden Markov models as a case study D. Szymczak #Haskell
• A generic view of primality (with Haskell type classes) Paul Tarau #Haskell
• Model checking and deduction N. Shankar #PVS