Lecturas del Grupo de Lógica Computacional (del 24 de mayo al 8 de junio)
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