Resumen de lecturas compartidas durante abril de 2018
Esta entrada es una recopilación de lecturas compartidas, durante abril 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.
- Francia invertirá 1.500 millones de euros en inteligencia artificial. #IA
- Parametricity for Bifunctor. ~ Brent Yorgey #Haskell
- Complexity problems in enumerative combinatorics. ~ Igor Pak #Math #CompSci
- L’algorithme quantique de Shor. ~ André Chailloux #CompSci
- IHaskell on mybinder.org ~ Vaibhav Sagar #Haskell #Jupyter #IHaskell
- Free lenses for higher-kinded data. ~ Sandy Maguire #Haskell
- Coq tactics index. ~ Joe Redmon (@pjreddie) #ITP #Coq
- Exercitium: “Múltiplos repitunos”. #Haskell #I1M2017 #Haskell #I1M2017
- Emacs #4: Automated emails to org-mode and org-mode syncing. ~ John Goerzen (@jgoerzen) #Emacs #OrgMode
- Ring theory, via coding theory and cryptography. ~ W. David Joyner #eBook #Math #Sagemath
- Calculus on graphs. ~ W. David Joyner #eBook #Math #Sagemath
- There’s more to mathematics than rigour and proofs. ~ Terence Tao #Math
- Exercitium: “Números tetranacci”. #Haskell #I1M2017 dígitos”]]. #Haskell #I1M2017
- Emacs for Data Science. ~ Robert Vesco (@robertvesco) #Emacs #DataScience
- Emacs for Data Science. ~ Ahsan Ijaz #Emacs #DataScience
- Examples using emacs org mode babel inline source code with different backend languages. ~ Derek Feichtinger #Emacs #OrgMode
- Exercitium: “Operaciones binarias con matrices”. #Haskell #I1M2017
- Exercitium: “Sucesiones de números consecutivos con suma dada”. #Haskell #I1M2017
- Applying computer algebra systems and SAT solvers to the Williamson conjecture. ~ C. Bright, I. Kotsireas, V. Ganesh #Logic #SAT #Math #CAS
- Emacs para ciencias del dato. #Emacs #OrgMode
- Why teaching FP to undergrads is important. ~ Evan Misshula (@emisshula) #FunctionalProgramming #Haskell
- The unreasonable relationship between mathematics and physics. ~ David Tong #Math #Physics
- RStartHere: A guide to some of the most useful R Packages that we know about, organized by their role in data science. #Rstat #DataScience
- OrgMode tutorial. ~ Rainer König #Emacs #OrgMode
- Exercitium: “Árbol de subconjuntos”. #Haskell #I1M2017
- What we talk about when we talk about monads. ~ T. Petricek #Haskell
- Seminario (I+A)A (Inteligencia Artificial + Aprendizaje Automático) #IA #AA
- OpenAI challenges you to beat 1990s classic Sonic the Hedgehog using machine learning. ~ #AI
- Comet.ml wants to do for machine learning what GitHub did for code. ~ F. Lardinois (@fredericl) #IA #ML
- Deriving Via (or, how to turn hand-written instances into an anti-pattern). ~ B. Blöndal, A. Löh, R. Scott #Haskell
- LMF2017: Deducción natural en lógica de primer orden. #Lógica
- LMF2017: Deducción natural de primer orden con Isabelle/HOL. #Lógica #IsabelleHOL
- I1M2017: El TAD de los conjuntos en Haskell. #Haskell #Algorítmica
- I1M2017: Las librerías de conjuntos y de diccionarios en Haskell. #Haskell
- I1M2017: El TAD de los polinomios en Haskell. #Haskell #Algorítmica #Matemáticas
- Learning to prove with tactics. ~ T. Gauthier, C. Kaliszyk, J. Urban, R. Kumar, M. Norrish #ITP #HOL4 #ML
- Org-mode and reproducible research. ~ Evan Misshula (@emisshula) #Emacs #OrgMode
- AI for humanity. #AI
- Here’s how the US needs to prepare for the age of artificial intelligence. ~ Will Knight #AI
- Quel langage pour le secondaire? ~ Laurent Bloch #Programming
- A unified approach to solving seven programming problems (functional pearl). ~ W.E. Byrd, M. Ballantyne, G. Rosenblatt, M. Might #FunctionalProgramming #Racket
- Jupyter notebook for beginners: a tutorial. ~ Benjamin Pryke (@BenjaminPryke) #Jupyter #Python
- Deep Learning: an introduction for applied mathematicians. ~ C.F. Higham, D.J. Higham #AI #ML #DeepLearning
- Plotting in Haskell. ~ James Church #FunctionalProgramming #Haskell
- The simple essence of automatic differentiation (Differentiable functional programming made easy). ~ Conal Elliott (@conal) #FunctionalProgramming #Haskell
- Tactics and certificates in Meta Dedukti. ~ R. Cauderlier #ITP #Dedukti
- Toward a tool to verify complex data structure invariants. ~ K.D. Roe #PhD_Thesis #ITP #Coq
- The boolean constraint solver of SWI-Prolog: system description. ~ M. Triska (@MarkusTriska) #Prolog #ConstraintProgramming
- Logic-Theorist: The sources of the first theorem prover. #ATP
- IHaskell on CoCalc! ~ Vaibhav Sagar (@vbhvsgr) #FunctionalProgramming #Haskell #CoCalc
- Welcome Haskell on CoCalc. #FunctionalProgramming #Haskell #CoCalc
- Deep learning: Why it’s time for AI to get philosophical. ~ Catherine Stinson (@cathnotcathy) #AI #Philosophy
- Exercitium: “Sucesión de antecesores y sucesores”. #Haskell #I1M2017 #I1M2017
- Dynamic programming in Haskell. ~ Laurence Emms (@wtfunctional) #FunctionalProgramming #Haskell
- Voronoi: A Haskell implementation of Fortune’s algorithm. #FunctionalProgramming #Haskell
- ‘Live coding’: desnudando a las máquinas a golpe de música. ~ Álvaro Lorite #Música #Programación vía @elsaltodiario
- Getting started with Emacs text editor. ~ Sachin Patil #Emacs #OrgMode #I1M2017
- How to create LaTeX documents with Emacs. ~ Sachin Patil #Emacs #OrgMode #LaTeX #I1M2017
- Exercitium: “Mayor número obtenido intercambiando dos dígitos”. #Haskell #I1M2017
- A footnote to “The crisis in contemporary mathematics”. ~ B. Katz, M.G. Katz, S. Sanders #Logic #Math
- Magit interface walkthrough. #Emacs #Magit
- Using Cloud Haskell to write a type-safe distributed chat. ~ Sebastian Pulido Gomez #Haskell
- Why does “=” mean assignment? ~ Hillel Wayne (@Hillelogram) #Programming
- Ten simple rules for responsible big data research. #BigData
- Exercitium: “La carrera de Collatz”. #Haskell #I1M2017 #Haskell #I1M2017
- LMF2017: Tableros semánticos. #Lógica
- Over 130 practical recipes for data analysis and machine learning. #Haskell #DataScience
- Introduction to Iltis: An interactive, Web-Based system for teaching logic. ~ G. Geck et als. #Teaching #Logic
- Modal logic playground (A graphical semantic calculator for modal propositional logic). ~ Ross Kirsling #Teaching #Logic
- Data engineers vs. data scientists. ~ Jesse Anderson #DataScience
- I1M2017: Emacs para ciencias del dato. #Emacs
- I1M2017: Haskell para ciencias del dato. #Haskell #DataScience
- I1M2017: Ejercicios con el tipo abstracto de dato de las pilas. #Haskell
- Exercitium: “Clases de equivalencia”. #Haskell #I1M2017
- Property based integration testing using Haskell! ~ Kristijan Šarić #Haskell
- Exercitium: “Diccionario de frecuencias”. #Haskell #I1M2017
- Twenty-four EU countries sign artificial intelligence pact in bid to compete with US & China. #AI
- Mike Gordon and hardware verification. ~ L. Paulson #ITP
- Evaluating winding numbers through Cauchy indices in Isabelle/HOL. ~ W. Li, L.C. Paulson #ITP #IsabelleHOL #Math
- What we talk about when we talk about monads. ~ T. Petricek (@tomaspetricek) #Haskell
- For mathematicians, = does not mean equality. ~ Jeremy Kun (@jeremyjkun) | Math ∩ Programming #Math #CompSci
- Math, music and imagination. ~ Marcus Miller #Math #Music
- Jupyter is where humans and data science intersect. ~ Paco Nathan (@pacoid) #Jupyter #DataScience
- Scientific Python in the browser. ~ M. Droettboom (@MDroettboom) #Python #DataScience
- Introduction to literate programming. ~ Howard Abrams (@howardabrams) #Emacs #OrgMode
- SLC2018: Soluciones lógicas de problemas lógicos. #Logic #Prolog #CLP
- LMF2017: Ejercicios de lógica de primer orden. #Lógica #IsabelleHOL
- Talk to Books (Browse passages from books using experimental AI). #AI
- Algorithms from AIMA (Artificial intelligence: a modern approach) in Haskell. ~ Chris Taylor #AI #Haskell
- Python implementation of algorithms from Russell And Norvig’s “Artificial Intelligence: A Modern Approach”. #AI #Python #Jupyter
- I1M2017: Relaciones binarias homogéneas con la librería de conjuntos de Haskell. #Haskell
- I1M2017: Ejercicios con el TAD de los polinomios en Haskell. #Haskell
- pycse – Python3 computations in science and engineering. ~ John Kitchin (@johnkitchin) #eBook #Python
- Scimax: an Emacs starterkit designed for people interested in reproducible research and publishing. ~ John Kitchin (@johnkitchin) #Emacs #OrgMode
- Gallery of named graphs (with tkz-berge.sty). ~ Alain Matthes #LaTeX #Math
- Using Cloud Haskell to write a type-safe distributed chat. ~ Sebastian Pulido Gomez #Haskell
- Why does “=” mean assignment? ~ Hillel Wayne #Programming
- A formal semantics of the core DOM in Isabelle/HOL. ~ A.D. Brucker, M. Herzberg #ITP #IsabelleHOL
- “Python computations in science and engineering” in Org mode ~ John Kitchin (@johnkitchin) #Emacs #OrgMode #Python
- I1M2018: Preguntas y respuestas sobre el modo Org. #Emacs #OrgMode
- I1M2018: Preguntas y respuestas sobre el modo Org: Portada, índice, cabeceras y símbolos matemáticos. #Emacs #OrgMode
- AITP 2018: The Third Conference on Artificial Intelligence and Theorem Proving (Abstracts of the talks). #AI #ATP #ITP
- Axiomatizing category theory in free logic. ~ C. Benzmüller, D.S. Scott #ITP #IsabelleHOL #CategoryTheory
- Safe reinforcement learning via formal methods (Toward safe control through proof and learning). ~ N. Fulton, A. Platzer #AI #ML #ATP
- Let’s make set theory great again! ~ John Harrison #ITP
- If mathematical proof is a game, what are the states and moves? ~ David McAllester #AI #ATP #ML #Math
- Exercitium: “Ampliación de árboles binarios”. #Haskell #I1M2017 #Haskell #I1M2017
- Interactive Theorem Proving in Higher-Order Logics. ~ J. Blanchette #ITP #IsabelleHOL
- Intelligence artificielle: les angles morts du rapport Villani. ~ Hervé Mariton (@HerveMariton) et Cyrille Dalmont (@CyrilleDalmont) #AI
- Exercitium: “Alturas primas”. #Haskell #I1M2017
- Very powerful data analysis environment – org mode with ob-ipython. ~ Robert Kozikowski #Emacs #OrgMode #Python #DataScience
- Some tips for learning Org Mode for Emacs. ~ Sacha Chua (@sachac) #Emacs #OrgMode
- Exercitium: “Cálculo de pi mediante la serie de Nilakantha”. #Haskell #I1M2017
- Efficient verification of imperative programs using auto2. ~ B. Zhan #IsabelleHOL
- The meaning of = for logic programmers. ~ Markus Triska (@MarkusTriska) #LogicProgramming #Prolog
- Boolos’ hardest logic puzzle ever in its purest form. ~ J.J. Colomina-Almiñana, P.R. Stinga #Logic
- Exercitium: “Números superpares”. #Haskell #I1M2017
- A better programming language for Data Science/Machine Learning. #Haskell #DataScience
- Working with lists. ~ Laurence Emms (@wtfunctional) #Haskell
- The best of Python: a collection of my favorite articles from 2017 and 2018 (so far). ~ Gergely Szerovay #Python
- What the history of Math can teach us about the future of AI. ~ Nathan Myhrvold #Math #AI
- Why Haskell is hot for cryptocurrencies. ~ Niklas Hambüchen #Haskell
- Exercitium: “Búsqueda en los dígitos de pi”. #Haskell #I1M2017 #Haskell #I1M2017
- Program reduction: a win for recursion schemes. ~ John Wiegley (@jwiegley) #Haskell
- Why you need Python environments and how to manage them with Conda. ~ Gergely Szerovay (@gergoszerovay) #Python
- Peligro: algoritmos al mando en la escuela. ~ Cathy O’Neill
- Armas de destrucción matemática: Cómo el big data aumenta la desigualdad y amenaza la democracia. ~ Cathy O’Neil #Libro #Matemáticas #BigData
- Linear algebra with applications. ~ W. Keith Nicholson #eBook #Math #OpenLibra
- Límites y paradojas de la evaluación científica. ~ Daniel Innerarity (@daniInnerarity)
- History of interactive theorem proving. ~ J. Schöpf, S. Widauer #ITP #DAO2018
- Course: Machine learning for theorem proving. ~ C. Kaliszyk #ATP #AI #ML
- Constructive analysis of S1S and Büchi automata. ~ M. Lichter, G. Smolka #ITP #Coq
- Evidence-providing problem solvers in Agda. ~ U. Zalakain #ITP #Agda
- Erlang: The power of functional programming. ~ S. Thompson #FunctionalProgramming #Erlang
- Functional reactive programming. ~ B. Siegel #FunctionalProgramming
- Semantic Web and Machine Learning. ~ F. Železný #ILP
- El resurgir de la programación funcional. #ProgramaciónFuncional #Haskell #Erlang #Elixir #Scala #Clojure #Fsharp vía @genbetadev
- Why monads? ~ Luca Belli (@__lucab) #Haskell
- JupyterLab is ready for users. #Jupyter
- Machine Learning is fun! (The world’s easiest introduction to Machine Learning). ~ Adam Geitgey (@ageitgey) #AI #MachineLearning
- Un futuro incierto ¿hacia donde marchamos? ~ Daniel Mery (@dmery)
- A quick guide to Emacs Lisp programming. ~ Chris Done (@christopherdone) #Emacs #Lisp
- Emacs is sexy! #Emacs
- Awesome Emacs: A community driven list of useful Emacs packages, libraries and others. #Emacs
- Here’s why so many data scientists are leaving their jobs. ~ Jonny Brooks-Bartlett (@Jonny_CBB) #DataScience
- Programming languages commonly used features in a side-by-side format. #Programming
- Exercitium: “Decidir si existe un subconjunto con suma dada”. #Haskell #I1M2017 #Haskell #I1M2017
- 10 libros de filosofía imprescindibles. ~ Filosofía&Co (@_filco) #Filosofía
- Org Babel recipes. #Emacs #OrgMode #Babel
- Higher-Kinded Data. ~ Sandy Maguire #Haskell
- Making a text adventure in Haskell (Part 4). ~ Laurence Emms (@wtfunctional) #Haskell #Game
- Verifying local definitions in Coq. ~ J. Breitner (@nomeata) #Haskell #Coq
- Exercitium: “Matrices de Hadamard”. #Haskell #I1M2017
- How to think like a programmer (lessons in problem solving). ~ Richard Reis (@richardreeze) #Programming
- Using functions for easier programming. ~ N. Savage #FunctionalProgramming #Haskell
- Formalising mathematics in simple type theory. ~ L.C. Paulson #ITP #Math #IsabelleHOL #HOL_Light
- Emacs #5: Documents and presentations with Org-Mode. ~ John Goerzen (@jgoerzen) #Emacs #OrgMode #LaTex #Beamer
- Exercitium: “Reducción de opuestos”. #Haskell #I1M2017
- Formal verification of platoon control strategies. ~ A. Rashid, U. Siddique, O. Hasan #ITP #HOL_Light
- Funflow: typed resumable workflows. ~ N. Clarke, A. Hermann, T. Nielsen #Haskell
- Exercitium: “Notas de evaluación acumulada”. #Haskell #I1M2017
- Bounded natural functors with covariance and contravariance in Isabelle/HOL. ~ A. Lochbihler, J. Schneider #ITP #IsabelleHOL
- Machine learning evolution (infographic). ~ A. Morrison (@AlanMorrison) and A. Rao (@AnandSRao) #AI #MachineLearnig #History
- Exercitium: “Números compuestos por un conjunto de primos”. #Haskell #I1M2017 #Haskell #I1M2017
- Best Haskell programming books for functional programming. #Haskell
- Kurt Gödel and the mechanization of mathematics. ~ J. Kennedy #Logic #Math
- Beauty and the beast (Eta Haskell on JVM). ~ Jarek Ratajski (@jarek000000) #Haskell
- DLV: Evolution and perspectives. ~ M. Alviano et als. #LogicProgramming #ASP #DLV
- New A.I. application can write its own code. ~ J. Boyd-Rice #AI
- The significance of Philosophy to Mathematics. ~ Richard Zach (@RrrichardZach) #Math #Philosophy
- Modelling bitcoin in Agda. ~ A. Setzer #ITP #Agda
- Quantifier elimination for reasoning in economics. ~ C.B. Mulligan et als. #Logic
- Asynchronous exception handling in Haskell. ~ M. Snoyman (@snoyberg) #Haskell
- Smarties: a general purpose behavior tree library written in Haskell. #Haskell #AI
- Iterating squared digit sum. ~ Brent Yorgey #Haskell #Math
- The Software Foundations book, in GHC. ~ Ryan Scott #Haskell
- Introduction to functional programming in Python. ~ Spiro Sideris #Python #FunctionalProgramming
- Proof and other dilemmas: Mathematics and Philosophy (Reviewed by Jeremy Avigad). #Math #Philosophy
- Formalization of a polymorphic subtyping algorithm. ~ J. Zhao, B.C.S. Oliveira, T. Schrijvers #ITP #Abella
- The Babel of languages and the substrate of nature. ~ Philip Thrift (@philipthrift) #Programming
- Applied category theory course: ordered sets. ~ John Carlos Baez (@johncarlosbaez) #Math #CategoryTheory
- Developing bug-free machine learning systems with formal mathematics. ~ D. Selsam, P. Liang, D.L. Dill #ITP #Lean #MachineLearnig
- Martin-Löf’s type theory (MLTT). ~ Larry Diehl (@larrytheliquid) #Logic
- Org mode syntax example. ~ Fabrice Niessen (@f_niessen) #Emacs #OrgMode
- Formas de incluir bibliografías en documentos Org. #Emacs #OrgMode #I1M2017
- Exercitium: “Subsucesiones crecientes de elementos consecutivos”. #Haskell #I1M2017
- A formally-proved algorithm to compute the correct average of decimal floating-point numbers. ~ S. Boldo, F. Faissole, V. Tourneur #ITP #Coq #Math
- Decades-old graph problem yields to amateur mathematician. ~ Evelyn Lamb #Math
- Un famoso «gurú» de la vida eterna resuelve un problema matemático de hace 60 años. #Matemáticas vía @jborrego
- SBV: SMT Based Verification in Haskell (Released: April 29th, 2018). #Haskell #SMT #SBV
- Communication Artificial Intelligence for Europe. #AI