GLC

Esta entrada es una recopilación de lecturas compartidas esta semana (del 10 al 17 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.

• Verification of certifying computations through AutoCorres and Simpl. L. Noschinski, C. Rizkallah & K. Mehlhorn #Isabelle_HOL
• Formally verified computation of enclosures of solutions of ordinary differential equations. F. Immler #Isabelle_HOL
• Máximos locales. Exercitium #Haskell #I1M2013
• Formalization of function matrix theory in HOL. Zhiping Shi et als. #ITP #HOL4
• Lista cuadrada. Exercitium #Haskell #I1M2013
• From type theory to Haskell in 10 minutes. Matt Campbell #Logic #Haskell
• Dialogues for proof search. J. Alama #Kuno #Lisp
• Functional systems in Haskell. D. Mazières, B. O’Sullivan & D. Terei [Slides] #Haskell
• Segmentos maximales con elementos consecutivos.. Exercitium #Haskell #I1M2013
• Hipster: Integrating theory exploration in a proof assistant. M. Johansson et als. #Isabelle_HOL #Haskell
• Valores de polinomios representados mediante vectores. Exercitium #Haskell #I1M2013
• Programming with arrows. J. Hughes #Haskell
• Ramas de un árbol. Exercitium #Haskell #I1M2013
• Razonamiento sobre programas con Isabelle/HOL. LMF2014 #Isabelle_HOL
• Primitively (co)recursive definitions for Isabelle/HOL. L. Panny, J.C. Blanchette & D. Traytel #Isabelle_HOL
• Thinking in types. P. Brisbin #Haskell
• The algebra of algebraic data types. C. Taylor #Haskell
• Types, and two approaches to problem solving. Dan Piponi #Haskell