Resumen de lecturas compartidas (enero de 2018)

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

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

• Exercitium: “Posiciones de las mayúsculas”. #Haskell #I1M2017
• Exercitium: “Sucesión de raíces enteras de los números primos”. #Haskell #I1M2017
• Exercitium: “Recorrido por niveles de árboles binarios”. #Haskell #I1M2017
• Haskell notes for professionals book. #eBook #Haskell
• An extensible ad hoc interface between Lean and Mathematica. ~ R.Y. Lewis #ITP #Lean #Mathematica
• Template Haskell tutorial. ~ M. Karpov (@mrkkrp) #Haskell
• Exercitium: “Factorial módulo”. #Haskell #I1M2017
• Algoritmo de Monte Carlo aplicado a búsquedas en espacios de estados. ~ F. Sancho (@sanchocaparrini) #IA
• ProofSweeper: Play Minesweeper by formally proving your moves in Idris. ~ Andrew Miller #Idris #Haskell
• Haskell containers package. ~ Matt Renaud #Haskell
• The falling factorial of a sum. ~ L. Bulwahn #IsabelleHOL
• Exercitium: “Ordenación según una cadena”. #Haskell #I1M2017
• RA2017: Panorama de la demostración asistida por ordenador. #Prover9 #ACL2 #PVS #IsabelleHOL
• I1M2017: Manejo de ficheros en Haskell. #Haskell
• Functional programming for mathematical computing. ~ Matthias Endler (@matthiasendler) #Haskell
• Libro de exámenes de programación funcional con Haskell (versión del 6 de enero de 2018). #Haskell #I1M2017
• The foundations of mathematics. ~ K. Kunen #eBook #Logic #Math
• Is State a Comonad? ~ Edward Kmett (@kmett) #Haskell
• Finite of sense and infinite of thought: a history of computation, logic and algebra, part I. ~ Ron Pressler #Logic #Math #CompSci
• Formal verification: the gap between perfect code and reality. ~ Ray Wang #Formal_methods
• Exercitium: Números apocalípticos. #Haskell #I1M2017
• Coming soon: machine-checked mathematical proofs in everyday software and hardware development. ~ Adam Chlipala #ITP
• Snårkl: Somewhat practical, pretty much declarative verifiable computing in Haskell. ~ G. Stewart, S. Merten, L. Leland #Haskell
• TWAM: A certifying abstract machine for logic programs. ~ B. Bohrer, K. Crary #ITP #LF
• The Kuratowski closure-complement theorem in Isabelle/HOL. ~ P. Gammie, G. Gioiosa #ITP #IsabelleHOL #Math
• Exercitium: Enumeración de los números enteros. #Haskell #I1M2017
• The Shoelace formula for the area of a polygon. ~ Atabey Kaygun (@Atabey_Kaygun) #CommonLisp #Math
• Monads are just monoids in the category of endofunctors. ~ Axel Wagner (@TheMerovius) #Haskell #Math
• 10 awkward moments in math history. ~ Elena Nisioti (@elennisioti1) #Math #History
• Hezarfen: a theorem prover for intuitionistic propositional logic in Idris. ~ Joomy Korkut #Idris #Haskell #Logic
• Las universidades de EEUU al fin lo han reconocido: empezar a programar por Java es una mala idea. ~ Esther Miguel Trula
• Libro con las soluciones de las 16 primeras relaciones de ejercicios de programación con Haskell. #Haskell #I1M2017
• Exercitium: Números somirp. #Haskell #I1M2017
• Haskell et programmation fonctionnelle, ma conviction. ~ Frédéric Menou (@ptit_fred) #Haskell
• A formally verified implementation of multivariate Taylor models in Isabelle/HOL. ~ C. Traut, F. Immler #ITP #IsabelleHOL
• Exercitium: Ordenación por frecuencia. #Haskell #I1M2017
• Exercitium: Números malvados y odiosos. #Haskell #I1M2017
• An Isabelle/HOL formalisation of Green’s theorem. ~ M. Abdulaziz, L.C. Paulson #ITP #IsabelleHOL #Math
• Introduction to Singletons (Part 2). ~ Justin Le (@mstk) #Haskell
• A friendly introduction to mathematical logic. ~ Christopher C. Leary #eBook #Logic
• NP-hard does not mean hard. ~ Jeremy Kun (@jeremyjkun) | Math ∩ Programming #CompSci
• Œuf: Minimizing the Coq extraction TCB. ~ E. Mullen et als. #Coq
• The simple essence of automatic differentiation. ~ Conal Elliott (@conal) #Haskell
• linearmap-family: Purely-functional, coordinate-free linear algebra. ~ Justus Sagemüller #Haskell #Math
• From neural networks to the Category of composable supervised learning algorithms in Scala with compile-time matrix checking based on singleton-types. ~ Pascal Voitot (@mandubian) #Scala
• CodeWorld: The why, what, and how of teaching Haskell to children. ~ Chris Smith #Haskell
• How to teach computational thinking. ~ Stephen Wolfram #Teaching #CompSci
• Integrating computer science in math: the potential is great, but so are the risks. ~ Emmanuel Schanzer #Teaching #CompSci #Math
• Bootstrap: a research project at Brown University that offers a series of curricular modules built around purely mathematical programming. #Teaching #CompSci #Math
• Exercitium: Sumas parciales de Nicómaco. #Haskell #I1M2017
• “Let us calculate!”: Leibniz, Llull, and the computational imagination. ~ Jonathan Gray
• A tableaux calculus for reducing proof size. ~ M.P. Lettmann, N. Peltier #Logic #ATP
• Haskell in middle and high school mathematics. ~ F. Alegre, J. Moreno #Haskell #Math
• Mathematics for middle and high school in Haskell. #Haskell #Math
• Applicative functors and data validation, part II. ~ Carlos Morera de la Chica #Haskell
• Exercitium: “Enumeración de los números enteros”. #Haskell #I1M2017
• Extending higher-order logic with predicate subtyping: application to PVS. ~ Frédéric Gilbert #ITP #PVS
• Supermonads and superapplicatives. ~ J. Bracker, H. Nilsson #Haskell #Agda
• Lecture notes on rewriting theory. ~ F. Blanqui
• Towards verifying Ethereum smart contract bytecode in Isabelle/HOL. ~ S. Amani, M. Bégel, M. Bortin, M. Staples #ITP #IsabelleHOL
• Guía turística de Sevilla con Scratch. ~ @programamos #Scratch
• Exercitium: “Números somirp”. #Haskell #I1M2017 #I1M2017
• Formal microeconomic foundations and the First Welfare Theorem. ~ C. Kaliszyk, J. Parsert #ITP #IsabelleHOL
• A primer on boolean satisfiability. ~ Emina Torlak #Logic #SAT #Racket via @ozanerdem
• Course: Computer-aided reasoning for software. ~ E. Torlak #AutomatedReasoning #Logic
• Functional programming principles in Scala. ~ Martin Odersky #FunctionalProgramming #Scala
• Exercitium: “Ordenación por frecuencia”. #Haskell #I1M2017
• Formalizing data management systems: a case study of Syndicate protocol. ~ C.K. Wang, H. Xu #ITP #Coq
• Computational Quadrinitarianism (Curious Correspondences go Cubical). ~ Gershom Bazerman #CompSci
• A random walk through experimental mathematics. ~ E.Y.S. Chan, R.M. Corless #Math #Programming
• λ-calculus. ~ Christian Sternagel #Logic #Haskell #CompSci
• Exercitium: “Números malvados y odiosos”. #Haskell #I1M2017 #I1M2017
• Shrink fast correctly! ~ Olivier Savary Bélanger, Andrew W. Appel #ITP #Coq
• Hofstadter’s Q sequence. ~ Atabey Kaygun (@Atabey_Kaygun) #CommonLisp #Math
• Ten common myths about Computer Science. #CompSci
• Reasoning about functional programs. ~ Christian Sternagel #Logic #Haskell
• Resources for teaching with formal methods. ~ Jeremy Avigad #FormalMethods
• Computer understandable mathematics. ~ Josef Urban #ATP #ITP #Math
• The specification and analysis of use properties of a nuclear control system. ~ M.D. Harrison, P.M. Masci, J. Creissac Campos and P. Curzon #ITP #PVS
• Efficiency of functional programs. ~ Christian Sternagel and Harald Zankl #Haskell
• History of interactive theorem proving. ~ John Harrison, Josef Urban and Freek Wiedijk #ITP
• Computational thinking as an emergent learning trajectory of mathematics. ~ Tiina Partanen #Math #CompSci
• Verification of a concurrent garbage collector. ~ Yannick Zakowski #PhDThesis #ITP #Coq
• Typing of functional programs. ~ Christian Sternagel #Logic #FunctionalProgramming
• Creando un videojuego paso a paso con Scratch desde cero. ~ Jesús Moreno León (@J_MorenoL) #Scratch
• Domain modelling with Haskell: data structures. ~ Oskar Wickström #Haskell
• Liquid Haskell: refinement types for Haskell. ~ Niki Vazou (@nikivazou) #Haskell #LiquidHaskell
• Exercitium: “Sumas parciales de Nicómaco”. #Haskell #I1M2017
• Sequences, yet functions: the dual nature of data-stream processing. ~ S. Herbst, J. Tenschert, A.M. Wahl, K. Meyer-Wegener #ITP #Coq
• Course: Functional programming. ~ Christian Sternagel et als. #Haskell
• How to prove a compiler correct. ~ Daniel Patterson #Haskell
• Explaining type errors. ~ B. Yorgey, R. Eisenberg, H. Eades #Haskell
• Exercitium: “Fractal hexagonal”. #Haskell #I1M2017
• Relational characterisations of paths. ~ R. Berghammer, H. Furusawa, W. Guttmann, P. Höfner #ITP #IsabelleHOL
• Functors done quick! ~ James Bowen (@james_OWA) #Haskell
• Programando un laberinto con Scratch, ¡para principiantes! ~ Alejandra Sánchez Acosta #Scratch vía @programamos
• Dafny overview. ~ K. Rustan M. Leino #Dafny
• “Interpreters a la Carte” in Advent of Code 2017 Duet. ~ Justin Le (@mstk) #Haskell
• Exercitium: “Números como diferencias de potencias”. #Haskell #I1M2017 #I1M2017
• Formalization of Bachmair and Ganzinger’s ordered resolution prover. ~ A. Schlichtkrull, J.C. Blanchette, D. Traytel and U. Waldmann (Code) #ITP #IsabelleHOL
• Haskell functions as functors, applicatives and monads. ~ Eli Bendersky (@elibendersky) #Haskell
• The nesting instinct. ~ Julie Moronuki (@argumatronic) #Haskell
• Model theory and machine learning. ~ H. Chase, J. Freitag #Logic #AI
• Exercitium: “Escalada hasta un primo”. #Haskell #I1M2017
• Computer-assisted proving of combinatorial conjectures over finite domains: a case study of a chess conjecture. ~ P. Janičić, F. Marić, M. Maliković #ITP #IsabelleHOL
• Pointwise Kan extensions. ~ Bartosz Milewski (@BartoszMilewski) #CategoryTheory #Haskell
• Cracking codes with Python: An introduction to building and breaking ciphers. ~ Al Sweigart #eBook #Programming #Python
• RedPRL: a proof assistant for Computational Higher-Dimensional Type Theory. #ITP #RedPRL #SML
• Computational (higher) type theory. ~ R. Harper and C. Angiuli #RedPRL #SML
• Context Free/cfdg: a simple language for generating stunning images. With only a few lines you can describe abstract art, beautiful organic scenery, and many kinds of fractals.
• Elsa: a lambda calculus evaluator. ~ R. Jhala @RanjitJhala #Haskell #Logic #LambdaCalculus
• Exercitium: “Terna pitagórica a partir de un lado”. #Haskell #I1M2017
• China enters the battle for AI talent. #AI
• Toward scalable verification for safety-critical deep networks. ~ L. Kuper et als. #NeuralNetworks #SMT
• El curioso caso de la secuencia de Goodstein. ~ M.A. Morales (@gaussianos) | El Aleph #Matemáticas
• A conversation with Stephen Cook. #CompSci
• Collatz sequence (yet again). ~ Atabey Kaygun (@Atabey_Kaygun) #CommonLisp #Math
• Introduction to functional programming in Python. ~ Spiro Sideris #FunctionalProgramming #Python
• Finitary-based domain theory in Coq: An early report. ~ M.A. AbdelGawad #ITP #Coq
• Domain modelling with Haskell: Generalizing with Foldable and Traversable. ~ Oskar Wickström #Haskell
• LambdaCase in the wild. ~ Matt Noonan (@BanjoTragedy) #Haskell
• Recursion schemes, Part 4½: Better living through base functors. ~ Patrick Thomson (@importantshock) #Haskell
• Lambda calculus in Clojure (Part 2). ~ Sergio Rodrigo Royo #LambdaCalculus #Clojure
• Free: You can now read classic books by MIT Press on archive.org #eBooks
• When is Haskell more useful than R or Python in Data Science? ~ Tikhon Jelvis (@tikhonjelvis) #Haskell #Rstats #Python #DataScience
• Programming R at native speed using Haskell. ~ M. Boespflug, F. Domínguez, A. Vershilov #Haskell #Rstats
• A hashing-based graph implementation in Haskell. ~ Patrick Dougherty #Haskell
• Selling laziness. ~ Alex Beal (@beala) #Programming
• Why functional programming matters. ~ John Hughes #FunctionalProgramming #Miranda
• A toy Wolfram Language interpreter in Haskell. ~ Yonghao Jin #Haskell
• Org-mode: An integrated language and editor. ~ Alex Beal (@beala) #Emacs #Haskell
• Why sum types matter in Haskell. ~ Will Kurt (@willkurt) #Haskell
• Exercitium: “Complemento potencial”. #Haskell #I1M2017
• Intrinsically-typed definitional interpreters for imperative languages. ~ C. Bach Poulsen, A. Rouvoet, A. Tolmach, R. Krebbers #ITP #Agda
• Monads are not what they seem (Uncovering the hidden nature of programming concepts). ~ T. Petricek #Math #CompSci
• Securing complex software systems using formal verification and specification. ~ X. Qi #FormalVerification
• Programación funcional: la programación del futuro. ~ Moises Vázquez #ProgramacionFuncional #Haskell
• Exercitium: “Sumas parciales de Juzuk”. #Haskell #I1M2017
• A verified ODE solver and the Lorenz attractor. ~ F. Immler #ITP #IsabelleHOL
• Un vistazo al futuro: revisando demostraciones matemáticas con la computadora. ~ Moisés Vázquez #DAO
• Exercitium: “Sucesión de dígitos 0 y 1 alternados”. #Haskell #I1M2017
• Formalizing the meta-theory of first-order predicate logic. ~ H. Herberlin, S.Y. Kim, G. Lee #ITP #Coq #Logic
• Category theory: a gentle introduction. ~ Peter Smith (@PeterSmith) #CategoryTheory
• Investigations in computer-aided mathematics: experimentation, computation, and certification. ~ Thomas Sibut Pinote #PhDThesis #ITP #Coq
• Formal methods for probabilistic programming. ~ D. Selsam, P. Liang, D.L. Dill #ITP #Lean
• Certigrad: Bug-free machine learning on stochastic computation graphs. ~ D. Selsam #ITP #Lean