Resumen de lecturas compartidas (diciembre de 2017)

Esta entrada es una recopilación de lecturas compartidas, durante diciembre de 2017, en Twitter sobre programación funcional y demostración asistida por ordenador.

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: “Sumas de dos cuadrados”. #Haskell #I1M2017 #Haskell #I1M2017
• Teaching the formalization of mathematical theories and algorithms via the automatic checking of finite models. ~ W. Schreiner, A. Brunhuemer, C. Fürst #ITP #Math #RISCAL
• Números piramidales de cuatro dimensiones. ~ Antonio Roldán (@Connumeros) #Matemáticas #Programación
• November 2017 1HaskellADay problems and solutions. ~ Douglas M. Auclair (@geophf) | Typed Logic #Haskell #1HaskellADay
• From logic programming to machine ethics. ~ A. Saptawijaya, L.M. Pereira #LogicProgramming #KRR #AI
• Tierless Web programming in ML. ~ G. Radanne #PhD_Thesis #FunctionalProgramming #OCaml
• A domain specific language for drum beat programming. ~ A.R. Du Bois, R. Ribeiro #Haskell #DSL #Music
• RA2017: Ejercicios de razonamiento detallado sobre programas en Isabelle/HOL. #IsabelleHOL
• RA2017: Razonamiento por casos y por inducción en Isabelle/HOL. #IsabelleHOL
• I1M2017: 2º examen de programación funcional con Haskell. #Haskell
• I1M2017: Evaluación perezosa en Haskell. #Haskell
• A formal proof in Coq of a control function for the inverted pendulum. ~ D. Rouhling #ITP #Coq #Math #Physics
• Writing code like a mathematical proof. ~ Spiro Sideris #Math #Programming
• Haskell for dummies. ~ M. Snoyman (@snoyberg) #Haskell
• CompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler. ~ D. Kästner et als. #ITP #Coq #CompCert
• Reflecting on Haskell in 2017. ~ Stephen Diehl (@smdiehl) #Haskell
• Exercitium: “Conjunto de relaciones binarias entre dos conjuntos”. #Haskell #I1M2017 #I1M2017
• Slides and other materials for functional programming lectures ITMO university. ~ D. Kovanikov, A. Seroka #Haskell
• Point-free or die: tacit programming in Haskell and beyond. ~ Amar Shah #Haskell
• Voting with ties: Strong impossibilities via SAT solving. ~ F. Brandt, C. Saile, C. Stricker #SAT_solving
• Exercitium: “Menor x tal que los x múltiplos de n contienen todos los dígitos”. #Haskell #I1M2017 elementos”]]. #Haskell #I1M2017
• A constructive formalisation of semi-algebraic sets and functions. ~ B. Djalal #ITP #Coq #Math
• Arithmetic coding. ~ Jeremy Gibbons (@jer_gib) #Haskell #Math
• Exercitium: “Reconocimiento de relaciones funcionales entre dos conjuntos”. #Haskell #I1M2017 #I1M2017
• Finding bugs in Haskell code by proving it. ~ J. Breitner (@nomeata) #Haskell
• Using Haskell on the frontend. ~ Vanessa McHale #Haskell
• La inteligencia artificial que caza noticias para Reuters en Twitter. ~ David Sarabia (@DSRELD) #IA
• Reuters Tracer: toward automated news production using large scale social media data. ~ X. Liu et als. #AI #BigData
• learn elm: discover why people are switching to Elm and how you can get started today! #elm
• Un bestiario fractal de curvas para rellenar el espacio (y el cerebro). ~ @Alvy #Fractales
• Brainfilling curves: a fractal bestiary. ~ Jeffrey Ventrella
• A complete taxonomy of plane-filling curves. ~ Jeffrey Ventrella #Fractal
• Analyzing individual proofs as the basis of interoperability between proof systems. ~ G. Dowek #ITP #Coq #IsabelleHOL
• Functional pearl: integer partitions and QuickCheck. ~ Vanessa McHale #Haskell
• Exercitium: “Expresiones equilibradas”. #Haskell #I1M2017 #I1M2017
• Secret link uncovered between pure math and physics. ~ Kevin Hartnett #Math #Physics
• Cómo compartir un secreto usando sistemas de ecuaciones lineales. ~ A. Cano, J.M. LunA, A. Rojas #Matemáticas
• The mind as a computational system. ~ Christoph Adami #AI
• Geometría axiomática. ~ Gerard Romo Garrido #Matemáticas
• Variations on a theme: A set of curated examples meant to show Haskell’s expressiveness. ~ Vanessa McHale #Haskell
• Exercitium: “Conjunto de funciones entre dos conjuntos”. #Haskell #I1M2017
• P = NP: Perhaps I change my mind. (An old result put a new way). ~ R.J. Lipton, K.W. Regan #Math #CompSci
• Mathematicians crack the cursed curve. ~ Kevin Hartnett #Math
• Notes on mathematical writing. ~ Clark Barwick #Math
• Rings: an efficient Java/Scala library for polynomial rings. ~ S. Poslavsky #Scala #Math
• Towards automatic resource bound analysis for OCaml. ~ J. Hoffmann, A. Das, S.C. Weng #OCaml
• The role of theory in Deep Learning. ~ David McAllester #AI #DeepLearning
• Computation in Logic and Logic in Computation. ~ S. Salehi #Logic #CompSci
• Exercitium: “Mayúsculas y minúsculas alternadas”. #Haskell #I1M2017 #I1M2017
• All about strictness analysis (part 1). ~ Sebastian Graf (@sgraf1337) #Haskell
• Introduction to logic programming with Prolog. ~ Mathias Schilling (@MatChilling) #Prolog
• Co finds a pairing. ~ Phil Freeman (@paf31) #Haskell
• Streaming arithmetic coding. ~ Jeremy Gibbons (@jer_gib) #Haskell #Math
• A framework for certified self-stabilization. ~ S. Devismes, P. Corbineau, K. Altisen #ITP #Coq
• Getting things done in Haskell. ~ Jasper Van der Jeugt (@jaspervdj) #Haskell
• Exercitium: “Aplicación de lista de funciones a lista de elementos”. #Haskell #I1M2017 #I1M2017
• Dismal arithmetic. ~ D. Applegate, M. LeBrun, N.J.A. Sloane #Math
• The Haskell pyramid. ~ Patrick Nielsen (@pmylund) #Haskell
• fugacious: An example Haskell Web application. ~ Jasper Van der Jeugt (@jaspervdj) #Haskell
• swMATH: An information service for mathematical software. #Math #CompSci
• Exercitium: “Máximo de las rotaciones restringidas”. #Haskell #I1M2017
• Computational Logic: its origins and applications. ~ L.C Paulson #Logic #ITP #IsabelleHOL
• Monadification of functional programs. ~ M. Erwig, D. Ren #Haskell
• Exercitium: “Caminos minimales en un árbol numérico”. #Haskell #I1M2017
• An interactive introduction to quantum computing (or what do you mean they can be both zero and one at the same time!) ~ D. Kemp #CompSci
• Efficiency is not associative for matrix multiplication. ~ J.D. Cook @JohnDCook #Math #CompSci
• A brief introduction to category theory. ~ D. Hofmann #CategoryTheory
• I1M2017: Ejercicios de evaluación perezosa y listas infinitas en Haskell (1). #Haskell
• Applications of automated reasoning. ~ J. Harrison #AutomatedReasoning
• El Tao de la programación. #Programación
• The Tao of programming. #Programming
• Verified iptables firewall analysis & verification. ~ C. Diekmann, L. Hupel, J. Michaelis, M. Haslbeck, G. Carle #ITP #IsabelleHOL
• A tour of Go in Haskell. ~ Osanai Kazuyoshi #Haskell
• Exercitium: “Ordenación valle”. #Haskell #I1M2017
• Reading simple Haskell. ~ Gil Mizrahi #Haskell
• Continuation passing style Free Monads and direct style Free Monads. ~ Quentin Duval @quduval #Idris
• Folding Christmas fractals. ~ Clarissa Grandi (@c0mplexnumber) #Math
• Online Turing machine simulator. ~ Martín Ugarte #CompSci #Turing
• RA2017: Ejercicios dec uantificadores sobre listas en Isabelle/HOL. #IsabelleHOL
• RA2017: Razonamiento sobre árboles y bosques en Isabelle/HOL. #IsabelleHOL
• I1M2017: Programas interactivos en Haskell. #Haskell
• I1M2017: Definiciones de la lista infinita de factoriales en Haskell. #Haskell #Matemáticas
• A logical relation for monadic encapsulation of state (proving contextual equivalences in the presence of runST). ~ A. Timany et als. #ITP #Coq #Haskell
• What makes Haskell unique. ~ M. Snoyman (@snoyberg) #Haskell
• safe-money: Money in the type system where it belongs. ~ Renzo Carbonara #Haskell
• Emacs: Org mode, programing language code markup. ~ Xah Lee (@xah_lee) #Emacs #Programming #OrgMode
• taskell: A command line task manager written in Haskell. ~ Mark Wales #Haskell
• Logic books of the year? ~ Peter Smith #Logic
• SLS: Songbird + Lemma Synthesis (a separation logic prover which can automatically synthesize inductive lemmas on-the-fly). #ATP #OCaml
• An axiomatic basis for bidirectional programming. ~ H.S. Ko, Z. Hu #ITP #Agda
• Bonsai: synthesis-based reasoning for type systems. ~ K. Chandra, R. Bodik #Racket
• Exercitium: “Número de viajeros en el autobús”. #Haskell #I1M2017
• Collapsing towers of interpreters. ~ N. Amin, T. Rompf #Lisp #Scala
• Debug: Haskell library for debugging. ~ Neil Mitchell #Haskell
• Fast and fearless evolution of server-side Web applications. ~ Oskar Wickström (@owickstrom) #Haskell
• A water-based solution of polynomial equations. ~ Mark Levi #Math
• Safety and conservativity of definitions in HOL and Isabelle/HOL. ~ O. Kunčar, A. Popescu #ITP #IsabelleHOL
• The string search algorithm by Knuth, Morris and Pratt in Isabelle/HOL. ~ F. Hellauer, P. Lammich #IsabelleHOL
• Monadic “do” block, yet again (What should get into your “do” block?) ~ Arvind Devarajan #Haskell
• Exercitium: “Reconocimiento de recorridos correctos”. #Haskell #I1M2017
• Lambda calculus in Clojure (part 1). ~ Sergio Rodrigo Royo #LambdaCalculus #Clojure
• Haskell in production in a startup in 2017? Yup. ~ Frédéric Menou (@ptit_fred), Clément Delafargue (@clementd) #Haskell
• Functional programming with graphs. ~ @futtetennista #Haskell
• Solving satisfiability using inclusion-exclusion. ~ A. Zaleski #Logic #Sat #Maple
• The Haskell performance checklist. ~ Chris Done (@christopherdone) #Haskell
• Exercitium: “Bosque de recorridos del autobús”. #Haskell #I1M2017 #I1M2017
• Benchmarks for numbers: ints, doubles, bignums, rationals, etc. ~ Chris Done (@christopherdone) #Haskell
• Splitting and splicing intervals (part 1). ~ R. Jhala (@RanjitJhala) #Haskell #LiquidHaskell
• De Lutero a Voevodsky, pasando por Brouwer: Reformas en matemáticas. ~ J. Ferreirós #Matemáticas
• Exercitium: “Aplicaciones biyectivas”. #Haskell #I1M2017
• I1M2017: Representación gráfica de funciones en Haskell con GNUplot. #Haskell
• I1M2017: Programación de dibujos por comprensión en CodeWorld/Haskell. #Haskell #CodeWorld
• I1M2017: Programación de dibujos por recursión en CodeWorld/Haskell. #Haskell #CodeWorld
• A library for algorithmic game theory in Ssreflect/Coq. ~ A. Bagnall, S. Merten, G. Stewart #ITP #Coq
• Building Haskell apps with Docker. ~ D. Bertovic #Haskell via @FPComplete
• Exercitium: “Menor con suma de dígitos dada”. #Haskell #I1M2017
• All about reflection: a tutorial. ~ A. Spiwack #Haskell
• A Lisp REPL in your pocket. ~ Kvardek Du #Lisp #Android
• Reasoning about program behavior algebraically. ~ Stephen Diehl (@smdiehl) #Haskell
• Understanding simplicity: implementing a smart contract language in 30 lines of Haskell. ~ Dan Robinson #Haskell
• Evolutionary programming converts darwinism into algorithms. ~ R. Colin Johnson #Programming #AI
• The Mason–Stother’s theorem. ~ Manuel Eberl #ITP #IsabelleHOL
• Some notes about how I write Haskell. ~ Getty Ritter (@aisamanra) #Haskell
• Exercitium: “Cadenas opuestas”. #Haskell #I1M2017
• Zipperposition: An automatic theorem prover in OCaml for typed logic with equality, datatypes and arithmetic. ~ Simon Cruanes #OCaml #ATP #Logic
• Extending superposition with integer arithmetic, structural induction, and beyond. ~ Simon Cruanes #PhD_Thesis #OCaml #ATP #Logic
• Programas artístico-matemáticos en menos de 280 caracteres. ~ @Alvy #Programación #Matemáticas
• Introduction to singletons (Part 1). ~ Justin Le (@mstk) #Haskell
• On possible use of quantifier elimination software in upper secondary mathematics education. ~ Y. Sato, R. Fukasaku #Math #Logic
• The median-of-medians selection algorithm. ~ Manuel Eberl #ITP #IsabelleHOL
• Exercitium: “Vecino en lista circular”. #Haskell #I1M2017 primos”]]. #Haskell #I1M2017
• Integrated simulation and formal verification of a simple autonomous vehicle. ~ A_ Domenici, A. Fagiolini, M. Palmieri #Formal_verification #ITP #PVS
• importify: manage Haskell imports quickly. ~ Dmitry Kovanikov et als. #Haskell
• Exercitium: “Suma de las hojas de mínimo nivel”. #Haskell #I1M2017 #Haskell #I1M2017
• Beginning Computer Science with R. ~ H. White #CompSci #Rstats
• Protolude: A sensible starting Prelude for building custom Preludes. ~ Stephen Diehl (@smdiehl) #Haskell
• Scaling Isabelle proof document processing. ~ M. Wenzel #IsabelleHOL
• Exercitium: “Sumable sin vecinos”. #Haskell #I1M2017.
• Getting used to R, RStudio, and R Markdown. ~ C. Ismay #Rstats
• Tiny art in less than 280 characters. ~ Antonio S. Chinchón (@aschinchon) #Rstats
• Programar (en R) te da alas. ~ Antonio S. Chinchón (@aschinchon) #Rstats
• Formal proof of polynomial-time complexity with quasi-interpretations. ~ H. Férée et als. #ITP #Coq
• Exercitium: “Rotaciones divisibles por 8”. #Haskell #I1M2017
• A library for algorithmic game theory in Ssreflect/Coq. ~ A- Bagnall, S. Merten, G. Stewart #ITP #Coq
• Annotated multisemantics to prove Non-Interference analyses. ~ G. Cabon, A. Schmitt #ITP #Coq