Resumen de lecturas compartidas durante marzo de 2018
Esta entrada es una recopilación de lecturas compartidas, durante marzo de 2018, en Twitter sobre programación funcional y demostración asistida por ordenador fundamentalmente.
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: “Menor potencia de 2 que comienza por n”. #Haskell #I1M2017
- Fast machine words in Isabelle/HOL. ~ A. Lochbihler #ITP #IsabelleHOL
- Teaching quantum physics to a computer. ~ Oliver Morsch #MachineLearning
- Artificial intelligence and its applications in healthcare and pharmacy. ~ Atul Adhikari #AI
- A reproducible research toolkit. #Emacs #OrgMode #Rstats
- Using Emacs, Org-mode and R for Research Writing in Social Sciences. ~ Vikas Rawal #Emacs #OrgMode #Rstats
- Matemática discreta en Haskell. ~ María Dolores Valverde Rodríguez #Haskell #Matemáticas #OpenLibra
- Exercitium: “Ceros con los n primeros números”. #Haskell #I1M2017
- A theory of architectural design patterns in Isabelle/HOL. ~ Diego Marmsoler #ITP #IsabelleHOL
- From math to machine: translating a function to machine code. ~ Brian Steffens #Programming #Math #Haskell #Imperative_language #Assembly_language #Machine_code #I1M2017
- A Game in Haskell: Dino Rush. ~ Joe Vargas (@jxv_io) #Haskell #Game
- Comonad Transformers in the Wild. ~ Isaac Elliott #Haskell
- Haskell with Reactive Banana and GTK3. ~ Paul Johnson #Haskell
- CLI program for pretty-printing Haskell datatypes. ~ Dennis Gosnell (@cdepillabout) #Haskell
- A gentle introduction to monad transformers. #Haskell
- Curso intensivo de Google sobre aprendizaje automático e inteligencia artificial (en español). #IA
- Org mode pour LaTeXiens. ~ Fabrice Niessen #Emacs #OrgMode #LaTeX
- Haskell for the imperative. ~ Laurence Emms (@wtfunctional) #Haskell
- Getting started with Haskell. ~ Laurence Emms (@wtfunctional) #Haskell
- The type language. ~ Laurence Emms (@wtfunctional) #Haskell
- Mandelbrot fractal in Haskell. ~ Laurence Emms (@wtfunctional) #Haskell
- Quick specifications for the busy programmer. ~ N. Smallbone, M. Johansson, K. Claessen, M. Algehed #Haskell
- Quick-Sort: a pet peeve. ~ A. Nunes-Harwitt, M. Gambogi, T. Whitaker #Haskell
- Data Science predicts Oscar winner. ~ Lucy Black #AI #DataScience
- Successful companies use Erlang and Elixir. #FunctionalProgramming #Erlang #Elixir
- Natural deduction and the Isabelle proof assistant. ~ J. Villadsen, A. Halkjær, A. Schlichtkrull #ITP #IsabelleHOL #Logic
- NaDeA: A Natural Deduction Assistant with a formalization in Isabelle. #IsabelleHOL #Logic #NaDeA
- The Sequent Calculus Trainer: a tool that aims at supporting students in learning how to correctly construct proofs in the sequent calculus for propositional logic and first-order logic with equality. #Logic
- Proof search in the sequent calculus for first-order logic with equality. ~ Arno Ehle #ATP #Logic
- Image processing with Juicy Pixels and Repa. ~ Mark Karpov (@mrkkrp) #Haskell
- History of Mathematics. ~ Doron Zeilberger #Math #History
- Learning how to prove: From the Coq proof assistant to textbook style. ~ S. Böhne, C. Kreitz #ITP #Coq #Logic
- Concise history of Mathematics. ~ Dirk J. Struik #eBook #Math #History
- Hypothesis: Annotate the web, with anyone, anywhere. ~ @hypothes_is #Annotation
- Haskell without the theory. ~ Saurabh Nanda #Haskell
- Trying out GHC compact regions for improved latency (Pusher case study). ~ Mateusz Kowalczyk #Haskell
- Exercitium: “Generación de progresiones geométricas”. #Haskell #I1M2017
- The Sequent Calculus Trainer with automated reasoning (Helping students to find proofs). ~ A. Ehle, N. Hundeshagen, M. Lange #Logic
- In Mathematics, mistakes aren’t what they used to be (Computers can’t invent, but they’re changing the field anyway). ~ Siobhan Roberts #Math #CompSci
- Implicit Runge Kutta and GNU scientific library. ~ Dominic Steinitz (@idontgetoutmuch) #Haskell #Math
- ¿Qué demonios es la programación funcional? ~ Rodrigo de Frutos #ProgramacionFuncional
- Funtores, Aplicativos y Mónadas en imágenes. ~ Miguel Á. Moreno #Haskell
- Exercitium: “La función de Smarandache”. #Haskell #I1M2017 #Haskell #I1M2017
- QWIRE practice: Formal verification of quantum circuits in Coq. ~ R. Rand, J. Paykin, S. Zdancewic #ITP #Coq
- Measuring functions in Criterion. ~ Patrick Dougherty #Haskell
- Simple fractals in Haskell. ~ @Mike_K_Houghton #Haskell
- Exercitium: “Números cuyos factoriales son divisibles por x pero no por y”. #Haskell #I1M2017 divisores”]]. #Haskell #I1M2017
- Hammer for Coq: automation for dependent type theory. ~ Ł. Czajka, C. Kaliszyk #ITP #Coq
- Symbolic execution: intuition and implementation. ~ Alex Beal(@beala) #Haskell
- Making a text adventure in Haskell (Part 1). ~ Laurence Emms (@wtfunctional) #Haskell
- Exercitium: “Nodos con máxima suma de hijos”. #Haskell #I1M2017 #I1M2017
- A Coq formalisation of SQL’s execution engines. ~ V. Benzaken et als. #ITP #Coq
- Applied functional programming course. #Haskell
- Simple puzzle with rotating circles. ~ Ilya V. Portnov #Haskell #Gloss
- Object oriented programming in Haskell. ~ Edsko de Vries #Haskell
- Exercitium: “Matrices centro simétricas”. #Haskell #I1M2017
- Proof Pearl: Constructive extraction of cycle finding algorithms. ~ D. Larchey-Wendling #ITP #Coq #SLC2018
- MonadFix and the lazy and strict state monad. ~ Moritz Kiefer (@cocreature) #Haskell
- Haskell design patterns: The handle pattern. ~ Jasper Van der Jeugt (@jaspervdj) #Haskell
- Implementing a safer sort with linear types. ~ Alexander Vershilov, Arnaud Spiwack #Haskell
- Constructive decision via redundancy-free proof-search. ~ D. Larchey-Wendling #ITP #Coq #SLC2018
- Who needs category theory? ~ A. Blass, Y. Gurevich #CategoryTheory #CompSci
- Generating artwork with Haskell. ~ Benjamin Kovach (@BendotK) #Haskell
- Proposal recommends AI training in China’s primary, secondary schools. #AI
- Using Org Mode, LaTeX, Beamer, and Medibang Paint to make a children’s book. ~ Sacha Chua #Emacs #OrgMode #LaTeX #Beamer
- Emacs #1: Ditching a bunch of stuff and moving to Emacs and org-mode. ~ John Goerzen (@jgoerzen) #Emacs #OrgMode
- Emacs #2: Introducing org-mode. ~ John Goerzen (@jgoerzen) #Emacs #OrgMode
- Emacs #3: More on org-mode. ~ John Goerzen (@jgoerzen) #Emacs #OrgMode
- MDP+TA = PTA: Probabilistic timed automata, formalized (short paper). ~ S. Wimmer, J. Hölzl #ITP #IsabelleHOL
- Writing simple Haskell. ~ Gil Mizrahi (@_gilmi) #Haskell
- Making a text adventure in Haskell (Part 2). ~ Laurence Emms (@wtfunctional) #Haskell
- Clara-rules: Forward-chaining rules in Clojure. #Clojure
- Clojure and AI. ~ Michael Pershyn #Clojure #AI
- I1M2017: Introducción a la programación con Maxima. #Maxima
- I1M2017: De la matemática a la máquina. #Matemática #Programación
- I1M2017: Análisis de la complejidad de los algoritmos. #Haskell #Algorítmica
- I1M2017: Cálculo numérico en Haskell (2º parte). #Haskell #Matemáticas
- I1M2017: Ejercicios de programación de cálculo numérico en Maxima. #Maxima #Matematicas
- I1M2017: Programación dinámica en Haskell. #Haskell #Algorítmica
- LMF2017: Deducción natural proposicional (2). #Lógica
- LMF2017: Ejercicios de deducción natural proposicional. #Lógica
- LMF2017: Deducción natural proposicional con Isabelle/HOL. #IsabelleHOL #Lógica
- Exercitium: “Cruce de listas”. #Haskell #I1M2017
- Correct-by-construction finite field arithmetic in Coq. ~ J. Philipoom #ITP #Coq #Math
- Data visualization with Haskell: NYC public urination. ~ David Lettier #Haskell #DataScience
- A compendium of clean graphs in R (version 2.0). ~ E.J.Wagenmakers, Q.F. Gronau #Rstats
- Exercitium: “Suma de los dígitos de las repeticiones de un número”. #Haskell #I1M2017 árbol”]]. #Haskell #I1M2017
- Foundations of Mathematics. ~ Ken Kubota (@KenKubota_de) #Math #Logic #LamdaCalculus #ITP #IsabelleHOL #Coq #PVS #Agda
- Formalization techniques for asymptotic reasoning in classical analysis. ~ R. Affeldt, C. Cohen, D. Rouhling #ITP #Coq #Math
- Breadth-first search in Haskell. ~ David Lettier #Haskell
- LMF2017: Representación del conocimiento mediante lógica de primer orden. #Lógica
- LMF2017: Sintaxis y semántica de la lógica de primer orden. #Lógica
- Intelligible Artificial Intelligence. ~ D.S. Weld, G. Bansal #AI #XAI
- How to design programs (2nd edition, 2018). ~ M. Felleisen, R.B. Findler, M. Flatt, S. Krishnamurthi #eBook #Programming #DrRacket
- Exercitium: “Suma de las sumas de los cuadrados de los divisores”. #Haskell #I1M2017
- Weight-balanced trees in Isabelle/HOL. ~ T. Nipkow, S. Dirix #IsabelleHOL
- Max subarray in Haskell. ~ David Lettier #Haskell
- Text Reflow in Haskell. ~ Laurence Emms (@wtfunctional) #Haskell
- I1M2017: 4º examen de programación funcional con Haskell. #Haskell
- Discrete structures. ~ M.G. Knepley #eBook #Math #ITP #Coq
- The OEIS now contains 300,000 integer sequences. ~ C. Lawson-Perfect #Math
- Exercitium: “La conjetura de Gilbreath”. #Haskell #I1M2017 matriz”]]. #Haskell #I1M2017
- On cryptographic attacks using backdoors for SAT. ~ A. Semenov et als. #SAT
- LMF2017: Ejercicios de deducción natural proposicional en Isabelle/HOL. #Lógica #IsabelleHOL
- Verlet integration (Physics simulation in Clojure). ~ M. Metz (@MMz_) #Clojure #Physics
- Exercitium: “Matrices de Pascal”. #Haskell #I1M2017
- Domain modeling with Haskell data structures. ~ Oskar Wickström (@owickstrom) #Haskell
- I1M2017: El tipo abstracto de datos de las pilas en Haskell. #Haskell #Algorítmica
- I1M2017: El tipo abstracto de datos de las colas en Haskell. #Haskell #Algorítmica
- Multiplicar es mas fácil de lo que piensas. ~ Juan Arias de Reyna #Matemáticas #Algorítmica
- Formalized first-order logic. ~ A.H. From #ITP #IsabelleHOL #Logic
- I1M2017: 4º examen de programación funcional con Haskell. #Haskell
- I1M2017: Soluciones del 4º examen de programación funcional con Haskell del grupo 1. #Haskell
- I1M2017: Soluciones del 4º examen de programación funcional con Haskell del grupo 2. #Haskell
- I1M2017: Soluciones del 4º examen de programación funcional con Haskell del grupo 3. #Haskell
- Course: Functional programming and intelligent algorithms. ~ Hans Georg Schaathun #Haskell #AI
- Narcissus: Deriving correct-by-construction decoders and encoders from binary formats. S. Suriyakarn, C. Pit-Claudel, B. Delaware, A. Chlipala #ITP #Coq
- Formalized unification algorithms. ~ K. Hvidtfeldt #ITP #IsabelleHOL #Logic
- Explanation in Mathematics (in “The Stanford Encyclopedia of Philosophy”). ~ Paolo Mancosu #Math #Philosophy
- Rose trees, breadth-first. ~ Donnacha Oisín Kidney (@oisdk) #Haskell
- Lessons learned. ~ Laurence Emms (@wtfunctional) #Haskell
- Haskell’s triangle: or, more fun with recursion. ~ Thomas Cothran (@thomas_cothran) #Math #Haskell #JavaScript
- Máquinas listas, pero sin sentido común. ~ Ramon López de Mántaras #IA
- Exercitium: “La conjetura de Levy”. #Haskell #I1M2017
- Formalization of a near-linear time algorithm for solving the unification problem. ~ K.F. Brandt #ITP #IsabelleHOL #Logic
- Making a text adventure in Haskell (Part 3). ~ Laurence Emms (@wtfunctional) #Haskell
- Seven sketches in compositionality: An invitation to applied category theory. ~ B. Fong, D.I Spivak #CategoryTheory
- Fundamental tools for Math in 2018. ~ Robert L. Read #Math
- CoCalc: Collaborative Calculation in the Cloud. ~ @cocalc_com #Math #SageMath via @paul_snively
- Exercitium: “Suma de las alturas de los nodos de un árbol”. #Haskell #I1M2017
- Well-founded unions. ~ J. Dawson, N. Dershowitz, R. Goré #ITP #IsabelleHOL
- Build systems à la carte. ~ A. Mokhov, N. Mitchell, Simon Peyton Jones #Haskell
- LMF2017: Semántica de la lógica de primer orden. #Lógica
- Exercitium: “Caminos en una matriz”. #Haskell #I1M2017
- Attack trees in Isabelle: CTL semantics, correctness and completeness. ~ F. Kammüller #ITP #IsabelleHOL #Logic
- ‘Grand unified theory of maths’ nets Abel Prize ~ D. Castelvecchi #Math
- From logic and math to code. For dummies. Part III. Dependent types. ~ R. Krivtsov #Logic #FunctionalProgramming
- Exercitium: “Máximo de las sumas de los caminos en una matriz”. #Haskell #I1M2017
- Argumentation theory for mathematical argument. ~ J. Corneli et als. #Math #Logic
- Two tools for formalizing mathematical proofs. ~ R.Y. Lewis #PhD_Thesis #Math #ITP #Lean #Mathematica
- Eleven simple algorithms to compute Fibonacci numbers. ~ A. Dasdan #Math #Programming #Python
- Exercitium: “Camino de máxima suma en una matriz”. #Haskell #I1M2017 #Haskell #I1M2017
- Ready, set, verify! Applying hs-to-coq to real-world Haskell code. ~ J. Breitner et als. #Coq #Haskell
- containers-verified: Formally verified drop-in replacement of containers. ~ J. Breitner (@nomeata) #Haskell #Coq
- La historia del error de división de los primeros Pentium. ~ M.A. Morales (@gaussianos) | El Aleph #Matemáticas
- (Haskell) modules for the masses. ~ E. Torreborre (@etorreborre) #Haskell
- In search of God’s perfect proofs. ~ E. Klarreich (@EricaKlarreich) #Math
- I1M2017: El tipo abstracto de datos de las colas de prioridad en Haskell. #Haskell #Algorítmica
- I1M2017: Programación dinámica: Caminos en una retícula. #Haskell #Algorítmica
- I1M2017: Programación dinámica: Apilamiento de barriles. #Haskell #Algorítmica
- I1M2017: Escritura de documentos, LaTeX, PDF y HTML con el modo Org de Emacs. #Emacs
- The incompatibility of Fishburn-Strategyproofness and Pareto-efficiency. ~ F. Brandt, M. Eberl, C. Saile and C. Stricker #ITP #IsabelleHOL
- Efficiently improving test coverage with algebraic data types. #Haskell
- Three layer Haskell cake. ~ Matt Parsons (@mattoflambda) #Haskell
- Replacing type classes with records affects optimisation. #Haskell
- LMF2017: Ejercicios de deducción natural proposicional en Isabelle/HOL (2). #Lógica #IsabelleHOL
- LMF2017: Ejercicios de sintaxis y semántica de la lógica de primer orden. #Lógica
- SLC2018: Programación funcional en Coq. #ITP #Coq
- SLC2018: Demostraciones por inducción en Coq. #ITP #Coq
- Techie Delight (Coding made easy): 500+ data structure and algorithms problems. ~ @techie_delight #Programming
- SLC2018: Datos estructurados en Coq. #ITP #Coq
- Exercitium: “La sucesión de Sylvester”. #Haskell #I1M2017
- Everyday Haskell (Haskell for the working programmer). ~ Laurence Emms (@wtfunctional) #Haskell
- Simple comparative benchmarks for CSV parsing libraries. #Haskell
- Exercitium: “Particiones primas”. #Haskell #I1M2017
- Automatic refinement to efficient data structures: a comparison of two approaches. ~ P Lammich, A Lochbihler #IsabelleHOL
- Exercitium: “Conjetura de Goldbach”. #Haskell #I1M2017 #I1M2017
- Thinking recursively in Python. ~ A. Awasthi #Python
- Computations in number theory using Python: A brief introduction. ~ J. Carlson #Python #Math
- A history of interactions between Logic and Number Theory. ~ A. Macintyre #Logic #NumberTheory
- Philosophy of mathematics and computer science. ~ K. Trzęsicki #Math #Logic #CompSci
- Mathematics for computer scientists (Lecture notes). ~ T. Altenkirch #Math #Haskell
- Exercitium: “Mayores sublistas crecientes”. #Haskell #I1M2017 dada”]]. #Haskell #I1M2017
- Goldbach’s function approximation using deep learning. ~ A. Stekel, M. Chkroun, A. Azaria #DeepLearning #Math
- Language-integrated provenance in Haskell. ~ J. Stolarek, J. Cheney #Haskell
- Demystifying functional programming (And what that means for learning & teaching). ~ Manuel M T Chakravarty (@TacticalGrace) and Gabriele Keller #Haskell
- L’intelligence artificielle, mythes et réalités. ~ Nicolas Rougier #IA via @interstices_eu
- Mathematical writing. ~ D,E. Knuth, T. Larrabee, and P.M. Roberts #Math
- Making L-Systems with Haskell and Logo. ~ Laurence Emms (@wtfunctional) #Haskell
- Encyclopedia of Combinatorial Structures (ECS). #Math
- Exercitium: “Máxima longitud de sublistas crecientes”. #Haskell #I1M2017
- An old and a new library for generic deriving. #Haskell
- Building blocks (a more visual approach to the topic of purely-typed functional programming). ~ Steven Vandevelde (@icidasset) #FuncionalProgramming #Haskell
- Scott Aaronson: 30 of my favorite books.
- Understanding contravariance. ~ Julie Moronuki and Chris Martin #Haskell
- Welcome to Type Classes! ~ Julie Moronuki (@argumatronic) and Chris Martin (@chris__martin) #Haskell