Meses: junio 2014

Esta entrada es una recopilación de lecturas compartidas las dos últimas semanas (del 15 al 19 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.

• Gibbs sampling in Haskell. ~ D. Steinitz #Haskell
• A Simpl shortest path checker verification. ~ C. Rizkallah. #Isabelle_HOL
• Category theory applied to functional programming. ~ J.P. Villa #Haskell
• SmartCheck: Redux. ~ Lee Pike #Haskell
• Abstracting an operational semantics to finite automata. ~ N. Baklanova, W. Ricciotti & M. Strecker #Isabelle_HOL
• Initial experiments with TPTP-style automated theorem provers on ACL2 problems. ~ S. Joosten et als. #ACL2
• Equivalence of the traditional and non-standard definitions of concepts from real analysis. ~ J. Cowles & R. Gamboa #ACL2
• Formal verification of Medina’s sequence of polynomials for approximating arctangent. ~ R. Gamboa & J. Cowles #ACL2
• An ACL2 mechanization of an axiomatic framework for weak memory. ~ B. Selfridge #ACL2
• Teaching software architecture using Haskell. ~ A. Serrano #Haskell
• Monad transformers for backtracking search. ~ J. Hedges #Haskell #Logic #SAT
• Lagrange’s four-square theorem. ~ Y. Watase #Mizar
• Solving the 15-Puzzle with Haskell and diagrams. ~ J. Rosenbluth #Haskel #AI #Diagrams
• Barely functional: Writing a real program in Haskell. ~ B. Kirwin #Haskell
• Experience report: The next 1100 Haskell programmers. ~ J.C. Blanchette #Haskell
• Developments in formal proofs. ~ T.C. Hales #Math #CompSci #ITP
• A verified decision procedure for MSO on words based on derivatives of regular expressions. ~ D. Traytel & T. Nipkow #AFP #Isabelle_HOL
• Lem: reusable engineering of real-world semantics. ~ D.P. Mulligan et als. #ITP #Coq #HOL4 #Isabelle
• The mathematics of secret sharing. ~ Jeremy Kun #Math #Haskell
• The list monad. ~ Bartosz Milewski | FP School of Haskell. #Haskell
• On the correctness of transactional memory algorithms. ~ M. Lesani #PhD_Thesis #PVS
• US intelligence agency wants brain-like algorithms for complex information processing. ~ M. Cooney @NWWlayer8 #AI
• Adding parallel Haskell to the undergraduate programming language course. ~ D.P. Bunde et als. #Haskell
• Teenage Haskell. ~ Tim Docker #Teaching #Haskell #Gloss
• “Si me equivoco en un algoritmo, ¿puedo terminar en la cárcel?”. ~ Mónica G. Salomone
• A generic numbering system based on Catalan families of combinatorial objects. ~ P. Tarau #Haskell
• Logic and computation. ~ B. Pientka #eBook #Logic #CompSci

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