Resumen de lecturas compartidas (octubre de 2017)

Esta entrada es una recopilación de lecturas compartidas, durante octubre de 2017, en Twitter sobre lógica computacional y programación funcional.

Las lecturas están ordenadas según su fecha de publicación en Twitter.

Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.

• Profunctors for encoding and decoding. ~ Kari Pahula #Haskell
• Making your brain tingle: Functions as functors. ~ Sascha Wilde #Haskell
• Codex: a web application for setting programming exercises in a learning environment. ~ Pedro Vasconcelos #Haskell
• Codex-QuickcCheck: QuickCheck customizations for the Codex learning environment. ~ Pedro Vasconcelos #Haskell
• Ofertas de trabajos del mes de septiembre. #MULCIA
• Lista de lecturas compartidas en septiembre de 2017. #GLC
• Métodos elementales de definición de funciones en Haskell. #I1M2017 #Haskell
• Ejercicios de definiciones por composición sobre números y listas. #I1M2017 #Haskell
• Trouble with databases? Persevere with Persistent! ~ James Bowen #Haskell
• Proof-checking Euclid. ~ M. Beeson, J. Narboux & F. Wiedijk #ITP #Coq #HOL_Light #Math
• Org mode as an Exocortex. ~ Irreal #Emacs
• What does explainable AI really mean? A new conceptualization of perspectives. ~ D. Doran, S. Schulz & T.R. Besold #XAI
• CMSC-16100 Lecture 1: Introduction to Haskell. ~ R. Chugh & S.A. Kurtz #Haskell #I1M2017
• A Quarter of Haskell (Supplementary notes for UChicago CMSC 16100). ~ R. Chugh & S.A. Kurtz #Haskell #I1M2017
• A Quarter of Haskell: Introduction to Haskell. ~ R. Chugh & S.A. Kurtz #Haskell #I1M2017
• A verified messaging system. ~ W. Mansky, A.W. Appel & A. Nogin #Coq
• Domain Specific Languages of Mathematics: Lecture Notes. ~ P. Jansson & C. Ionescu #Haskell #Math #I1M2017
• Metamorphisms. ~ Jeremy Gibbons #Haskell
• Les méthodes formelles: l’autre arme de la cybersécurité. ~ Jean Goubault-Larrecq #Formal_verification
• Which languages are bug prone. ~ Janet Swift #Programming
• Ten things you should know about Haskell syntax. ~ Bartosz Milewski #Haskell
• Definiciones por comprensión. #I1M2017 #Haskell
• Deduzione automatica. ~ M.P. Bonacina #ATP #Logic
• Formalizing and proving a typing result for security protocols in Isabelle/HOL. ~ A.V. Hess & S. Mödersheim #ITP #IsabelleHOL
• How to compose streaming programs. ~F. Domínguez #Haskell
• Natural deduction on Liquid Haskell. ~ Niki Vazou #Haskell #LiquidHaskell #Logic
• From design patterns to category theory. ~ Mark Seemann #Programming #Math
• Lists as context: A deeper look at the Applicative Type Class. ~ Will Kurt #Haskell
• Why do our programs need to read input and write output? ~ G. Gonzalez #Haskell
• Exponential sums make pretty pictures. ~ J.D. Cook #Math #Programming
• Haskell Weekly 75: News from the Haskell community (October 5 2017). #Haskell
• scalendar: Haskell Library to deal with resource availability in a Calendar. ~ Sebastián Pulido #Haskell
• A large-scale study of programming languages and code quality in GitHub. ~ B. Ray et als. #Programming
• Definiciones por comprensión (2). #Haskell #I1M2017
• Ejercicios de definiciones por composición sobre números y listas (2). #Haskell #I1M2017
• Semantic versioning checking in a declarative package manager. ~ M. Hanus #Curry
• Functional Pearl: Compiling a fifty year journey. ~ G. Hutton & P. Bahr #Haskell
• News in Isabelle2017 (October 2017). #IsabelleHOL
• A verified compiler from Isabelle/HOL to CakeML. ~ L. Hupel & T. Nipkow #IsabelleHOL
• Matemáticas conceptuales: Una primera introducción a categorı́as. ~ W. Lawvere & S. Schanuel #Matemáticas
• Category theory and functional programming. ~ Mikael Vejdemo Johansson #Math #CompSci #FunctionalProgramming
• Definiciones por recursión. #Haskell #I1M2017
• Ejercicios de definiciones con condicionales, guardas o patrones. #Haskell #I1M2017
• Isabelle functions: Always total, sometimes undefined. ~ Joachim Breitner #IsabelleHOL
• Computational geometry: set operations on polytopes. ~ Maksymilian Owsianny #Haskell #Math
• A Monoid for all seasons. ~ Julie Moronuki #Haskell #Logic #Math
• Making Kalman filtering correct with types. ~ Dominic Steinitz #Haskell #DataScience
• Array fusion with vector. ~ Manuel M T Chakravarty #Haskell
• Scrap your bounds checks with Liquid Haskell. ~ Gabriel Gonzalez #Haskell #LiquidHaskell
• Recursion schemes, part IV: Time is of the essence. ~ Patrick Thomson #Haskell
• A mechanized proof of Higman’s lemma by open induction. ~ Christian Sternagel #IsabelleHOL #Math
• What are some scientific applications of Haskell? ~ Edward Kmett #Haskell
• A tail we don’t need to wag. ~ Dan Piponi #Haskell
• Composing declarations in Template Haskell. #Haskell
• The CEO of GitHub, which caters to coders, thinks automation will bring an end to traditional software programming. ~ Becky Peterson #Programming
• hs-to-coq: Convert Haskell source code to Coq source code. ~ Antal Spector-Zabusky #Haskell #Coq
• MagicHaskeller based agent makes finalist in 1st round of general AI challenge! #Haskell #AI
• Contando números primos: Análisis contra Combinatoria. ~ Juan Arias de Reyna #Matemáticas #Computación
• The combinatorial algorithm for computing π(x). ~ Douglas B. Staple #Math #CompSci
• Homogeneous linear diophantine equations in Isabelle/HOL. ~ Florian Meßner et als. #ITP #IsabelleHOL #Math
• Machine-checked proof. ~ Jacob Gross #ITP #Math
• Computer-assisted reconstruction and assessment of E. J. Lowe’s modal ontological argument. ~ D. Fuenmayor & C. Benzmüller #IsabelleHOL
• hs-init: Tool for creating completely configured production Haskell projects. ~ Veronika Romashkina #Haskell
• Advice for Haskell beginners. ~ G. Gonzalez #Haskell
• The Hurwitz and Riemann ζ functions in Isabelle/HOL. ~ M. Eberl #IsabelleHOL #ITP #Math
• Hotswapping Haskell. ~ Jon Coens #Haskell
• I1M2017: Ejercicios de definiciones por comprensión. #Haskell
• RA2017: Comienzo del curso de “Razonamiento automático” del Máster en Lógica, Computación e Inteligencia Artificial
• RA2017: Presentación del curso de “Razonamiento automático”.
• A verified solver for linear recurrences in Isabelle/HOL. ~ M. Eberl #IsabelleHOL #ITP #Math
• Dirichlet series in Isabelle/HOL. ~ M. Eberl #IsabelleHOL #ITP #Math
• AI algorithms are starting to teach AI algorithms. #AI #Programming
• I1M2017: Ejercicios de definiciones por comprensión (2). #Haskell
• I1M2017: Ejercicios de definiciones por recursión (1). #Haskell
• Homogeneous linear diophantine equations in Isabelle/HOL. ~ F. Messner et als. #IsabelleHOL #ITP #Math
• Formal methods for Answer Set Programming. ~ Amelia J. Harrison #PhD_Thesis #ASP
• Formalization of quantum protocols using Coq. ~ J. Boender, F. Kammüller & R. Nagarajan #ITP #Coq
• forall x: Calgary Remix (An introduction to formal logic). ~ P.D. Magnus et als. #eBook #Logic
• Count the number of complex roots in Isabelle/HOL. ~ Wenda Li #IsabelleHOL #ITP #Math
• Empirically testing the Chowla conjecture. ~ J.D. Cook #Math #Programming
• ELFE: An interactive theorem prover for undergraduate students. ~ Maximilian Doré #ITP #Logic #Haskell
• ELFE: Interactive theorem proving for students (code). ~ Maximilian Doré #ITP #Logic #Haskell
• Good proofs are proofs that make us wiser. ~ Yu.I.Manin #Math
• Formal methods during the programming phase. ~ R.F. Paige et als. #Formal_methods
• Towards complete specification and verification with SMT. ~ N. Vazou et als. #Haskell #LiquidHaskell #Logic #SMT
• Handout on basics behind answer sets. ~ Yuliya Lierler #ASP #Logic #Programming
• Evaluate winding numbers through Cauchy indices in Isabelle/HOL. ~ Wenda Li #IsabelleHOL #ITP #Math
• Formalization of Pell’s equation in the Mizar system. ~ M. Acewicz & K. Pak #ITP #Mizar #Math
• Tangled Webs: Testing an integrated system. ~ James Bowen #Haskell
• Didáctica con R, menos cuentas y más pensamiento crítico. ~ A. Galindo #Matemáticas #Enseñanza
• Progress in the independent certification of Mizar Mathematical Library in Isabelle. ~ C. Kaliszyk & K. Pak #ITP #IsabelleHOL #Mizar #Math
• System Description: Russell (A logical framework for deductive systems). ~ Dmitry Vlasov #ITP #Logic
• I1M2017: El cifrado César en Haskell. #Haskell
• I1M2017: Ejercicios de definiciones por recursión (2). #Haskell
• RA2017: Programación funcional con Isabelle/HOL. #IsabelleHOL
• Transition systems and automata in Isabelle/HOL. ~ J. Brunner #IsabelleHOL
• Motor: Finite-state machines in Haskell. ~ Oskar Wickström #Haskell
• Linear Haskell: practical linearity in a higher-order polymorphic language. ~ Jean-Philippe Bernardy et als. #Haskell
• Using Stackage for GHC regression testing. ~ Manuel Chakravarty #Haskell
• The Kuratowski closure-complement theorem in Isabelle/HOL. ~ P. Gammie & G. Gioiosa. #ITP #IsabelleHOL #Math
• What’s the future of programming? The answer lies in functional languages. ~ Nick Heath #Programming #Haskell
• The refinement calculus of reactive systems toolset. ~ I. Dragomir, V. Preoteasa & S. Tripakis #IsabelleHOL
• Comonads for optionality. ~ Phil Freeman #Haskell #PureScript
• The game of pattern matching. ~ Phil Freeman #Haskell #PureScript
• Constructive pedagogy. ~ Julie Moronuki #Haskell #Pedagogy
• Modern library for working with URIs. ~ Mark Karpov #Haskell
• Why Computer Science is a science. Emanuele D’Osualdo #CompSi
• Cuatro décadas de Informática en España. ~ Ángel G. Perianes #Historia
• Temporal Answer Set Programming. ~ M. Diéguez #ASP
• Réminiscences d’un chercheur en informatique 1967-2000. ~ Gérard Huet #OCaml #Coq
• Formal proof of Banach-Tarski paradox. ~ Daniel de Rauglaudre #ITP #Coq #Math
• A pragmatic introduction to category theory. ~ Daniela Sfregola #Scala #Category_theory
• Answer Set Programming in Proofdoku. ~ Adam M. Smith #ASP #Game
• proofdoku: Game with ASP-backed mechanics. ~ By Nick Warren, Mason Reed & Adam Smith #ASP #Game
• Answer Set Programming tutorial (AIIDE2017). ~ Adam M. Smith #ASP #AI #Game
• Jean D’Alembert: cómo pasar de matemático a figura pública. ~ J. Ferreirós #Historia #Matemática
• Poisson distribution and prime numbers. ~ J.D. Cook #Math #Programming #Python
• View and annotate PDFs in Emacs with PDF-tools. #Emacs
• Mathematics and computation. ~ Avi Wigderson #eBook #Math #CompSci
• Büchi complementation in Isabelle/HOL. ~ J. Brunner #IsabelleHOL
• Functional programming with bananas, lenses, envelopes and barbed wire. ~ E. Meijer, M. Fokkinga & R. Paterson #FunctionalProgramming
• Generalized bananas, lenses and barbed wire. ~ Edward Kmett #Haskell
• An Idris library for recursion schemes, with liberal examples. ~ Vanessa McHale #Idris
• Peeling the banana: Recursion schemes from first principles. ~ Zainab Ali #Scala
• Near future of programming languages. ~ Stephen Diehl #Programming
• Mechanizing exploratory game design. ~ Adam M. Smith #eBook #ASP #Game #AI
• Command Line Interface Tweeter in Haskell. ~ Vanessa McHale #Haskell
• Temporal type theory (A topos-theoretic approach to systems and behavior). ~ P. Schultz, D.I. Spivak
• Solving a crossword in answer set programming. ~ Alessandro Bruni #ASP