Resumen de lecturas compartidas durante mayo de 2018
Esta entrada es una recopilación de lecturas compartidas, durante mayo 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: “Sumas de subconjuntos”. #Haskell #I1M2017
- Mechanising and verifying the WebAssembly specification. ~ C. Watt #IsabelleHOL #WebAssembly
- WebAssembly in Isabelle/HOL. ~ C. Watt #IsabelleHOL #WebAssembly
- Dockerizing our Haskell app. ~ James Bowen (@james_OWA) #Haskell #Docker
- Indian Supreme Court rules that CS degrees cannot be provided on-line. ~ Mark Guzdial (@guzdial) #Education #CompSci
- Using machine learning to improve cylindrical algebraic decomposition. ~ Z. Huang, M. England, D. Wilson, J.H. Davenport, L.C. Paulson #MachineLearning #Logic
- Courses on mathematical thinking now underway. ~ Sue Gee #Math #Logic #CompSci
- The Metamorphosis of Escher through tours.
- Exercitium: “Subconjuntos con suma dada”. #Haskell #I1M2017 #Haskell #I1M2017
- Gröbner bases of modules and Faugère’s F4 algorithm in Isabelle/HOL. ~ A. Maletzky, F. Immler #ITP #IsabelleHOL #Math
- Abe-Ohkubo-Suzuki linkable ring signatures. ~ A. Centelles, S. Diehl #Haskell
- Las matemáticas que descifraron la máquina «Enigma» de los nazis. ~ Paz Jiménez Seral y Manuel Vázquez Lapuente #Matemáticas
- Exploiting Answer Set Programming with external sources for meta-interpretive learning. ~ T. Kaminski, T. Eiter, K. Inoue #ASP #ILP
- Using SWISH to realise interactive web based tutorials for logic based languages. ~ J. Wielemaker, F. Riguzzi, R. Kowalski, T. Lager, F. Sadri, M. Calejo. #LogicProgramming #Prolog #SWISH
- Edit-time tactics in Idris. ~ Joomy Korkut (@cattheory). #Idris
- Rosetta Haskell (how abstractions are used by sequentially rewriting a program to do exactly the same thing using different techniques). ~ Chas Leichner #Haskell
- Advanced techniques for reducing Emacs startup time. ~ Joe Schafer #Emacs
- Exercitium: “Diccionario inverso”. #Haskell #I1M2017 #Haskell #I1M2017
- Variations on inductive-recursive definitions. ~ N. Ghani et als. #Agda
- VerifyThis 2018 – Polished Isabelle solutions. ~ P. Lammich and S. Wimmer #IsabelleHOL
- Exercitium: “Operaciones con series de potencias”. #Haskell #I1M2017
- Parametrised unit tests in Haskell. ~ Mark Seemann #Haskell
- Formal process virtual machine for smart contracts verification. ~ Z. Yang, H. Lei #Coq
- Learning logic and proof with an interactive theorem prover. ~ J. Avigad #Logic #ITP #Lean
- Logic and proof (Release 0.1). ~ J. Avigad, R.Y. Lewis, F. van Doorn #Logic #ITP #Lean
- Writing LaTeX with Org Mode. #Emacs #OrgMode #LaTeX
- Sistema de Deep Learning para el reconocimiento de palabras manuscritas implementado en TensorFlow y entrenado con IAM Handwriting Database. ~ Hugo Rubio #DeepLearning
- De resolver ecuaciones a aprendizaje profundo: Un tutorial de TensorFlow Python. ~ Oliver Holloway #DeepLearning
- From solving equations to Deep Learning: A TensorFlow Python tutorial. ~ Oliver Holloway #DeepLearning
- Type-level induction in Haskell. ~ Donnacha Oisín Kidney (@oisdk) #Haskell
- The lambda calculus. ~ J. Alama, J. Korbmacher #Logic
- Deep learning comes full circle. ~ N. Collins #DeepLearning
- Formal specification for a Cardano wallet. ~ D. Coutts, E. de Vries #Cardano
- AI researchers allege that machine learning is alchemy. ~ M. Hutson #MachineLearnig
- Exercitium: “Las sucesiones de Loomis”. #Haskell #I1M2017 #Haskell #I1M2017
- Making an ecosystem simulation in Haskell (Part 1). ~ Laurence Emms (@wtfunctional) #Haskell
- Dynamic programming in Haskell is just recursion. ~ Travis Athougies #Haskell
- Machine learning tutorial:
- Procedural generation of polyrhythmic beats. ~ Luke Palmer (@luqui) #Haskell
- Conversations with a six-year-old on functional programming. ~ Brent Yorgey #FunctionalProgramming
- Exercitium: “Polinomio digital”. #Haskell #I1M2017 conjunto dado”]]. #Haskell #I1M2017
- A brief introduction to literate analytics with Org-Babel. ~ Nick Barnwell #Emacs #OrgMode
- Introducción a la programación con Python 3. ~ José Luis Chiquete Valdivieso #Python
- C is not a low-level language (Your computer is not a fast PDP-11). ~ David Chisnall #Programming
- Exercitium: “Clausura respecto de una operación binaria”. #Haskell #I1M2017 #Haskell #I1M2017
- The Humanities of Maths/Computer Science. ~ L.P. Cruz #Math #CompSci
- MagicHaskeller: An inductive functional programming system for casual/beginner Haskell programmers. ~ Susumu Katayama #Haskell
- The Const Applicative and Monoids. ~ Justin Le (@mstk) #Haskell
- Exercitium: “Máximos de expresiones aritméticas”. #Haskell #I1M2017
- From math to machine: translating a function to machine code. ~ Brian Steffens #Programming #Math #Haskell #Imperative_language #Assembly_language #Machine_code #I1M2017
- An Isabelle/HOL formalization of the modular assembly kit for security properties. ~ O. Bračevac et als. #IsabelleHOL
- Vectorization in Haskell. ~ Abhiroop Sarkar #Haskell
- A curated collection of free eBooks about Haskell. #Haskell
- 8 time complexities that every programmer should know. ~ Adrián Mejía (@amejiarosario) #Algorithmic
- Revisiting decision diagrams for SAT. ~ T. van Dijk, R. Ehlers, A. Biere #Logic #ATP #SAT
- Machine learning guidance and proof certification for connection tableau. ~ M. Färber, C. Kaliszyk, J. Urban #MachineLearning #ATP #Prolog
- Explicit memoization can be elegant; a response to “Dynamic programming in Haskell is just recursion”. ~ Dan Burton #Haskell
- Exercitium: “Sucesiones suaves”. #Haskell #I1M2017
- Type-level induction in Haskell. ~ Donnacha Oisín Kidney (@oisdk) #Haskell
- Follow the denotation. ~ Sandy Maguire #Haskell
- Proof mining with dependent types. ~ E. Komendantskaya, J. Heras #ITP #Coq #MachineLearning
- The HKD pattern and type-level SKI. ~ Tom Ellis #Haskell
- Machine learning: A quick and simple definition. ~ James Furbush (@JamesFurbush) #AI #MachineLearning
- La hipótesis de Riemann y el problema P = NP. ~ Juan Arias de Reyna #Matemáticas #Computación
- Functional baby talk: Analysis of code fragments from novice Haskell programmers. ~ J. Singer (@jsinger_compsci), B. Archibald #Haskell
- Los puentes de Königsberg: Estudio y resolución con Haskell. ~ Miguel Ibáñez #Hakell #Matemáticas
- Proceedings of the 25th Automated Reasoning Workshop (Bridging the Gap between Theory and Practice). #ATP
- Qué hacer ante la “tecnupidez”. ~ Mario Bunge #Ciencia #Tecnología
- ¿Qué es la tecnología? ~ Dominique Raynaud #Ciencia #Tecnología
- ASP in industrial contexts: applications and toolchain. ~ Francesco Ricca #Logic #Programming #ASP
- Writing bug-free code using theorem provers. ~ Aaron Stump #ITP
- Proof assistants: from symbolic logic to real mathematics? ~ Lawrence C Paulson #ITP #Logic #Math
- Math can’t solve everything: questions we need to be asking before deciding an algorithm is the answer. ~ J. Williams, L. Gunn #Algorithms
- Exercitium: “Número de triangulaciones de un polígono”. #Haskell #I1M2017
- Automatic differentiation in machine learning: a survey. ~ Atılım Güneş Baydin et als. #AD #AutomaticDifferentiation #ML #MachineLearning
- Automatic differentiation. ~ Edward Kmett (@kmett) #Haskell #AD #AutomaticDifferentiation
- La Inteligencia Artificial no es como en las películas. ¿Qué es? #IA
- My Lisp experiences and the development of GNU Emacs. ~ Richard Stallman #Lisp #Emacs
- Intelligence artificielle et pensée humaine. ~ Margarida Romero (@margaridaromero) #IA
- Exercícios resolvidos em Prolog sobre sistemas baseados em conhecimento. ~ Paulo Cortez #Prolog
- Exercitium: “Números construidos con los dígitos de un conjunto dado”. #Haskell #I1M2017 #I1M2017
- A purely functional typed approach to trainable models (Part 1). ~ Justin Le (@mstk) #Haskell #MachineLearning
- The RedPRL proof assistant. ~ C. Angiuli, E. Cavallo, K.B. Hou, R. Harper, J. Sterling. #ITP
- Carnegie Mellon University starts first AI degree program in U.S. ~ K. Johnson @kharijohnson #AI
- Bachelor of Science in Artificial Intelligence (CMU): Curriculum. #AI
- Deductive mathematics (an introduction to proof and discovery for mathematics education). ~ A. Wohlgemuth #eBook #Math
- Pensée informatique et géométrie. ~ A. Busser, P. Debrabant, S. Gonifei #Math #Programming
- Dimiten varios empleados de Google por la aplicación de su inteligencia artificial a un proyecto militar. #AI vía @eldiariotec
- Inside Google, a debate rages: should it sell Artificial Intelligence to the military?. ~ Mark Berge #AI
- Exercitium: “Mayor número de atracciones visitables”. #Haskell #I1M2017
- Haskell communities and activities report (May 2018). #Haskell
- Verifying code toward trustworthy software. ~ Hyong-Soon Kim and Eunyoung Lee #FormalVerification
- I-MAKS (A framework for information-flow security in Isabelle/HOL). ~ S Grewe, H Mantel, M Tasch, R Gay, H Sudbrock #ITP #IsabelleHOL
- High-level signatures and initial semantics. ~ B. Ahrens, A. Hirschowitz, A. Lafont, M. Maggesi #ITP #Coq
- Emacs tools for writers. #Emacs
- 5 Emacs modes for writers. ~ Scott Nesbit (@ScottWNesbitt) #Emacs
- Exercitium: “Problema de las jarras”. #Haskell #I1M2017 #Haskell #I1M2017
- To build truly intelligent machines, teach them cause and effect. #AI
- The book of why (The new science of cause and effect). ~ Judea Pearl, Dana Mackenzie #Science #AI
- Catamorphisms and F-algebras. ~ Alexey Avramenko (@vvviiimmm) #Haskell
- Create Blockchain in Haskell. ~ Gaurav Agrawal (@gaurav_zen) #Haskell #Blockchain
- Proof pearl: Magic wand as frame. ~ Qinxiang Cao, Shengyi Wang, Aquinas Hobor, and Andrew W. Appel #ITP #Coq
- Advanced Github: Webhooks and automation. ~ James Bowen (@james_OWA) #Haskell
- Exercitium: “Sucesión de Recamán”. #Haskell #I1M2017
- Proof reuse in Coq using existential variables. ~ J. Breitner (@nomeata) #ITP #Coq
- A Coq formalization of digital filters. ~ Diane Gallois-Wong, Sylvie Boldo, and Thibault Hilaire #ITP #Coq
- Formalization of the arithmetization of euclidean plane geometry and applications. ~ Pierre Boutry, Gabriel Braun, Julien Narboux #ITP #Coq #Math
- A general formal memory framework in Coq for verifying the properties of programs based on higher-order logic theorem proving with increased automation, consistency, and reusability. ~ Zheng Yang, Hang Lei #ITP #Coq
- Performance and feature case studies in ecstasy. ~ Sandy Maguire #Haskell
- Artificial Intelligence’s ethical challenges. ~ L. Zacharias #AI #Ethics
- Cartography in Haskell. ~ Dominic Steinitz (@idontgetoutmuch) #Haskell
- Revisiting the tree edit distance and its backtracing: A tutorial. ~ B. Paaßen #Algorithms
- First experiments with neural translation of informal to formal mathematics. ~ Q. Wang, C. Kaliszyk, J. Urban #MachineLearning #Math
- Free monoidal functors, categorically! ~ Bartosz Milewski (@BartoszMilewski) #haskell #CategoryTheory
- Exercitium: “Grafo de divisibilidad”. #Haskell #I1M2017
- Direct interpretation of functional programs for debugging. ~ J. Whitington, T. Ridge #FunctionalProgramming
- Vector Programming using structural recursion (An introduction to vectors for beginners). ~ M.T. Morazán #Racket
- Using Elm to introduce algebraic thinking to K-8 students. ~ C. d’Alves et als. #Elm
- Teaching Erlang through the Internet: an experience report. ~ S. Adams #Erlang
- Exercitium: “El problema de las celebridades”. #Haskell #I1M2017 #I1M2017
- How I evaluate Haskell packages. ~ G. Gonzalez (@GabrielG439) #Haskell
- Making an ecosystem simulation in Haskell (Part 2). ~ Laurence Emms (@wtfunctional) #Haskell
- DeepLogic: end-to-end logical reasoning. ~ N. Cingillioglu, A. Russo #Logic #MachineLearnig
- Reinforcement learning of theorem proving. ~ C. Kaliszyk, J. Urban, H. Michalewski, M. Olšák #Logic #ATP #MachineLearnig
- Can machine learning identify interesting mathematics? An exploration using empirically observed laws. ~ Chai Wah Wu #MachineLearning #Math
- Formalizing (Web) standards: an application of test and proof. ~ A.D. Brucker, M. Herzberg #ITP #IsabelleHOL
- Exercitium: “Problema del dominó”. #Haskell #I1M2017
- Number sequence prediction problems and computational powers of neural network models. ~ H. Nam, S. Kim, K. Jung #MachineLearning #Math
- Teaching two programming languages in the first CS course. ~ M. Guzdial #Teaching #Programming
- Exercitium: “Sustitución de pares de elementos consecutivos iguales”. #Haskell #I1M2017 #Haskell #I1M2017
- Exercitium: “Caminos en un grafo”. #Haskell #I1M2017
- A classical math problem gets pulled into the modern world. ~ K. Hartnett #Math
- Probabilistic timed automata in Isabelle/HOL. ~ S. Wimmer, J. Hölzl #IsabelleHOL
- Hidden Markov models. ~ S. Wimmer #IsabelleHOL
- QuickCheck vs SmallCheck. ~ R. Cheplyaka (@shebang) #Haskell
- Polinomios contra ordenadores cuánticos. ~ I. Luengo #Matemáticas #Computación
- Technical writing: Learning from Kernighan. ~ Two Wrongs #Programming
- Microsoft is creating an oracle for catching biased AI algorithms. ~ W. Knight #AI
- The US military is funding an effort to catch deepfakes and other AI trickery. ~ W. Knight #AI
- Proving program correctness using the AG semantics: an example with n-Queens. ~ A. Harrison #ASP
- Free AI course from Finland. ~ S. Gee #AI
- Haskell/GHC symbol search cheatsheet. ~ Takenobu Tani #Haskell
- Combinatorics of permutations. ~ M. Bona #Math
- Combinatorics of permutations in Haskell: Introduction. ~ Vinay Madhusudanan #Haskell #Math
- Haskell: an introduction. ~ Sylvain Henry #Haskell
- Extensible ADT (EADT). ~ Sylvain Henry #Haskell
- Fast Haskell coding with cushions. ~ Roman Gonzalez #Haskell
- Exercitium: “Polinomios de Fibonacci”. #Haskell #I1M2017
- Irrational rapidly convergent series in Isabelle/HOL. ~ A. Koutsoukou Argyraki, W. Li #ITP #IsabelleHOL #Math
- Haskell Lens Operator Onboarding. ~ Russell Matney (@RussMatney) #Haskell
- Definitions of mathematics. #Math
- One Monad to prove them all (Functional pearl). ~ J- Christiansen, S. Dylus, F. Teegen #ITP #Coq #Haskell
- One formalization of virtue ethics via learning. ~ N.S. Govindarajulu, S. Bringjsord, R. Ghosh #AI
- A toolchain to produce correct-by-construction OCaml programs. ~ J.C. Filliâtre et als. #FunctionalProgramming #OCaml #Why3
- Exercitium: “Representaciones de grafos”. #Haskell #I1M2017
- Axiom systems for category theory in free logic. ~ C. Benzmüller and D. Scott #ITP #IsabelleHOL #Math #Logic
- Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems. ~ A Semenov et als. #SAT
- Functional pearl: La tour d’Hanoï. ~ R. Hinze #FuncionalProgramming #Haskell
- Simulation of mathematical games using functional programming. ~ D. Murphy #FuncionalProgramming #Haskell #Math #Games
- LaTeX notes for professionals book. #LaTeX
- Visualizing Cantor’s zig zag. ~ Patrick Honner (@MrHonner) #Math
- Lisp, Jazz, Aikido (three expressions of a single essence). ~ Didier Verna #FunctionalProgramming #Lisp
- f-strings in emacs-lisp. ~ John Kitchin (@johnkitchin) #Emacs #Elisp
- Automated verification of neural networks: Advances, challenges and perspectives. ~ F. Leofante et als. #AutomatedReasoning #MachineLearning
- Exercitium: “Problema de las 3 jarras”. #Haskell #I1M2017
- Monadification, memoization and dynamic programming in Isabelle/HOL. ~ S. Wimmer, S. Hu and T. Nipkow #ITP #IsabelleHOL #Algorithms
- Block puzzle in Haskell. ~ @__seroron #Haskell
- Exercitium: “Descomposiciones de N como sumas de 1, 3 ó 4”. #Haskell #I1M2017
- Computation-as-deduction in Abella: work in progress. ~ K. Chaudhuri, U. Gérard, D. Miller #ITP #Abella
- Announcing the Facebook Testing and Verification request for research proposals.
- ¿Realidad o ficción? Inteligencia artificial que nos engaña como por arte de magia. ~ Cristina Sánchez (@CristinaSanzM) #IA
- Nix: Haskell concepts for package managment. ~ James Bowen (@james_OWA) #Haskell #Nix
- Automated proof synthesis for propositional logic with deep neural networks. ~ T. Sekiyama, K. Suenaga #Logic #ATP #DeepLearning
- Purely functional AVL trees in Common Lisp. #CommonLisp
- DeepProbLog: Neural probabilistic logic programming. ~ R. Manhaeve et als. #LogicProgramming #DeepLearning
- How close are we—really—to building a quantum computer? ~ Larry Greenemeier #CompSci
- Constructive Mathematics. ~ D. Bridges #Logic #Math
- Un mainframe IBM 1401 de 1959 compilando Fortran. ~ @Alvy #Programación #Computación
- History of programming languages. #Programming #CompSci
- Timeline of programming languages. #Programming #CompSci