Resumen de lecturas compartidas durante junio 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: “Caminos reducidos”. #Haskell #I1M2017
• Optimal binary search trees in Isabelle/HOL. ~ T. Nipkow and D. Somogyi #ITP #IsabelleHOL #Algorithms
• Functional programming and legacy software (Using PureScript to extend a legacy JavaScript system). ~ C. Fischer #PureScript
• Syntax and semantics for operations with scopes. ~ M. Piróg, T. Schrijvers, N. Wu, M. Jaskelioff #Haskell
• Mathematical essentials of quantum computing. ~ J. Rué, S. Xambó #Math #CompSci
• Learn You a Physics for Great Good! ~ B. Werner, E. Sjöström, J. Johansson, O. Lundström #eBook #Haskell #Physics
• Certified ordered completion in Isabelle/HOL. ~ C. Sternagel, S. Winkler #ITP #IsabelleHOL
• Modular verification of programs with effects and effect handlers in Coq. ~ T. Letan, Y. Régis-Gianas, P. Chifflier, G. Hiet #ITP #Coq
• A more precise, more correct stack and register model for CompCert. ~ G. Barany #ITP #Coq
• Handling recursion in generic programming using closed type families. ~ A. Bolotina, A. Pelenitsyn #FunctionalProgramming #Haskell
• Algorithms notes for professionals. #eBook #Algorithms
• Purely functional and declarative GTK+ programming in Haskell. ~ Oskar Wickström (@owickstrom) #Haskell
• Domain specific languages of mathematics: lecture notes. ~ Patrik Jansson (@patrikja), Cezar Ionescu. #Haskell #Math
• Semi-formal development: The Cardano wallet. ~ Edsko de Vries #Haskell
• Exercitium: “Números de Church”. #Haskell #I1M2017
• Programming by poking: why MIT stopped teaching SICP (The Structure and Interpretation of Computer Programs). ~ Yarden Katz #Programming
• Course CMU 15-150: Functional programming, summer 2018. #FunctionalProgramming #SML
• Introductory Computer Science Education at Carnegie Mellon University: A Deans’ Perspective. ~ R.E. Bryant, K. Sutner, M.J. Stehlik #Teaching #CompSci
• Some thoughts on teaching functional programming. ~ R. Harper #Teaching #FuncionalProgramming
• Galileo is the genesis of a symbolic and numerical math tool written in Scala; a Computer Algebra System (CAS). #Scala #Math #CAS
• Making an ecosystem simulation in Haskell (Part 3). ~ Laurence Emms (@wtfunctional) #Haskell
• Explaining explanations: an approach to evaluating interpretability of machine learning. ~ L.H. Gilpin et als. #XAI #AI #MachineLearning
• Exercitium: “Números taxicab”. #Haskell #I1M2017
• Haskell-based CoinMetrics.io tools. #Haskell
• Codeworld: Haskell as a first programming language. ~ James Bowen (@james_OWA) #Haskell #Codeworld #Teaching
• You should learn functional programming in 2018. ~ Allan MacGregor (@allanmacgregor) #FunctionalProgramming
• Linux notes for professionals. #eBook #Linux
• Bloque de GAP de la asignatura Software Matemáticas. ~ Pedro A. García-Sánchez #CAS #SageMath
• GAP (groups, algorithms, programming) a system for computational discrete algebra. #CAS
• Monad transformers for the easily confused. ~ @TheWizardTower #Haskell
• GitHub alternative top 7 sites to host your open source project. #GitHub
• Top GitHub alternatives to host your open source project. ~ Abhishek Prakash #GitHub
• Exercitium: “La regla de los signos de Descartes”. #Haskell #I1M2017
• GamePad: a learning environment for theorem proving. ~ D. Huang, P. Dhariwal, D. Song, I. Sutskever #ITP #Coq #MachineLearning
• A new style of mathematical proof. ~ W.M. Farmer #Logic #Math
• A decision procedure for univariate polynomial systems based on root counting and interval subdivision. ~ C. Munoz, A. Narkawicz, A. Dutle #ITP #PVS #Math
• Exercitium: “Subexpresiones aritméticas”. #Haskell #I1M2017
• Calculational verification of reactive programs with reactive relations and Kleene algebra. ~ S. Foster, K. Ye, A. Cavalcanti, J. Woodcock #ITP #IsabelleHOL
• Generating art with Haskell. #Haskell
• Breadth-first traversals in far too much detail. ~ Donnacha Oisín Kidney (@oisdk) #Haskell
• Exercitium: “Ancestro común más bajo”. #Haskell #I1M2017
• Haskell RIP tutorial. ~ @RipTutorial #Haskell
• Deriving via (or, how to turn hand-written instances into an anti-pattern). ~ B. Blöndal, A. Löh, R. Scott #Haskell
• This algorithm can tell which number sequences a human will find interesting. #AI #MachineLearning #Math
• Formalization of the undecidability of the halting problem for a functional language. ~ T. M. Ferreira Ramos et al. #ITP #PVS
• Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents. ~ M. Wenzel #ITP #IsabelleHOL
• Essential cheat sheets for machine learning and deep learning engineers. ~ Vivian Chong #MachineLearning #DeepLearning
• Suggesting valid hole fits for typed-holes. ~ Matthías Páll Gissurarson #Haskell
• Category theory proofs in Idris. ~ Jesse Hallett (@hallettj) #Idris #CategoryTheory
• How does Idris compare to other dependently-typed programming languages? ~ Edwin Brady #Idris
• Exercitium: “Valores de polinomios y de expresiones”. #Haskell #I1M2017
• Las matemáticas del fútbol y el nuevo ministro de cultura. ~ Juan Arias de Reyna #Matemáticas #Computación
• Formalization of Lerch’s theorem using HOL Light. ~ A. Rashid, O. Hasan #ITP #HOL_Light #Math
• Formal small-step verification of a call-by-value lambda calculus machine. ~ F. Kunze, G. Smolka, Y. Forster #ITP #Coq
• Exercitium: “El problema de las N torres”. #Haskell #I1M2017
• Lenses embody Products, Prisms embody Sums. ~ Justin Le (@mstk) #Haskell
• Formalizing constructive quantifier elimination in Agda. ~ J. Pope #ITP #Agda #Logic
• A dyadic deontic logic in HOL. ~ C. Benzmüller, A. Farjami, X. Parent #ITP #IsabelleHOL #Logic
• A formalization of the LLL basis reduction algorithm. ~ J. Divasón, S. Joosten, R. Thiemann, A. Yamada #ITP #IsabelleHOL
• Machine learning predicts World Cup winner. #MachineLearning
• Prediction of the FIFA World Cup 2018: A random forest approach with an emphasis on estimated team ability parameters. ~ A. Groll et als. #MachineLearning
• LISP: back to the future (a tribute to 60th anniversary). ~ Nikolay Mozgovoy #Programming #Lisp
• The surprising security benefits of end-to-end formal proofs. ~ Adam Chlipala
• Goal-oriented conjecturing for Isabelle/HOL. ~ Y. Nagashima, J. Parsert #ITP #IsabelleHOL
• Mining the Archive of Formal Proofs. ~ J. Blanchette, M. Haslbeck, D. Matichuk, T. Nipkow #ITP #IsabelleHOL
• Mettre l’éthique dans l’algorithme? ~ Catherine Tessier, Vincent Bonnemains, Claire Saurel
• Séquences d’algorithmique en mathématique en Python 3, de la seconde à la terminale. ~ Hubert Raymondaud #Python
• A complete computing environment. #Emacs
• Emacs as a complete computing environment. ~ Ryan Rix #Emacs
• Skolem’s paradox. ~ Timothy Bays #Logic
• 100 years of Zermelo’s axiom of choice: what was the problem with it? ~ Per Martin-Löf #Logic #Math
• Functional Pearl: Theorem Proving for all (Equational reasoning in Liquid Haskell). ~ N. Vazou, J. Breitner, W. Kunkel, D. van Horn, G. Hutton #Hakell #LiquidHaskell
• Foundations of Mathematics: a discussion of sets and types. ~ Dominik Kirst #Logic #Math
• Formal small-step verification of a call-by-value lambda calculus machine. ~ F. Kunze, G. Smolka, Y. Forster #ITP #Coq
• Substitutionless first-order logic: a formal soundness proof. ~ A.H. From, J.B Larsen, A. Schlichtkrull, J. Villadsen #ITP #IsabelleHOL #Logic
• Ghosts for lists: from axiomatic to executable specifications. ~ F. Loulergue, A. Blanchard, N. Kosmatov #ITP #Coq
• Engaging millennials into learning formal methods. ~ N. Cataño #Teaching #FormalMethods
• PaMpeR: a proof method recommendation system for Isabelle/HOL. ~ Y. Nagashima, Y. He #ITP #IsabelleHOL
• Projective geometry in Isabelle/HOL. ~ Anthony Bordg #ITP #IsabelleHOL #Math
• Smart constructors that cannot fail. ~ Mark Karpov (@mrkkrp) #Haskell
• The localization of a commutative ring in Isabelle/HOL. ~ Anthony Bordg #ITP #IsabelleHOL #Math
• International Olympiad in Isabelle? #IsabelleHOL
• Formalizing category theory and presheaf models of type theory in Nuprl. ~ Mark Bickford #ITP #Nuprl #CategoryTheory
• Source Plugins: Four ways to build a typechecked Haskell expression. ~ Matthew Pickering #Haskell
• A promise checked is a promise kept: inspection testing. ~ Joachim Breitner (@nomeata) #Haskell
• Python notes for professionals. #Python
• The inside story of how AI got good enough to dominate Silicon Valley. #AI
• Diálogos entre Arquitectura, Ciudad y Computación. ~ F. Sancho (@sanchocaparrini) #NetLogo
• #I1M2017: Soluciones del 6º examen de programación funcional con Haskell de los grupos 1, 2 y 3. #Haskell
• #I1M2017: Soluciones del 6º examen de programación funcional con Haskell de los grupos 4 y 5. #Haskell
• #I1M2017: Soluciones del 5º examen de programación funcional con Haskell del grupo 1. #Haskell
• #I1M2017: Soluciones del 5º examen de programación funcional con Haskell del grupo 2. #Haskell
• #I1M2017: Soluciones del 5º examen de programación funcional con Haskell del grupo 3. #Haskell
• #I1M2017: Soluciones del 5º examen de programación funcional con Haskell del grupo 5. #Haskell
• Hyper natural deduction for Gödel Logic: a natural deduction system for parallel reasoning. ~ A. Beckmann, N. Preinin #Logic
• R language for programmers. ~ John D. Cook #Rstats
• Web Prolog and the programmable Prolog Web (An attempt to revive and rebrand Prolog). ~ Torbjörn Lager #Prolog
• Proof theory. ~ Jeremy Avigad #Logic
• AutoBench: Comparing the time performance of Haskell programs. ~ M.A.T. Handley, G. Hutton #Haskell
• IBM Debater: la primera inteligencia artificial que gana un debate a un ser humano. ~ @Alvy #IA
• Una introducción visual al aprendizaje automático y otra a los sesgos que pueden sufrir sus algoritmos. ~ @Alvy #IA #AprendzajeAutomático
• A visual introduction to machine learning. ~ Stephanie Yee (@stephaniejyee), Tony Chu (@tonyhschu) #AI #MachineLearning
• Model tuning and the bias-variance tradeoff. ~ Stephanie Yee (@stephaniejyee), Tony Chu (@tonyhschu) #AI #MachineLearning
• The P vs NP problem. ~ Anthony Bonato #CompSci
• Seven dogmas of category theory. ~ John D. Cook #CategoryTheory
• Why you don’t need data scientists. ~ Kurt Cagle #DataScience
• Un algoritmo que ha aprendido a resolver el Cubo de Rubik «sin asistencia humana». ~ @Alvy #IA #AprendizajeAutomático
• Solving the Rubik’s cube without human knowledge. ~ S. McAleer et als. #AI #MachineLearning
• La programación funcional en Haskell. ~ R. Peña #ProgramaciónFuncional #Haskell
• Schematic polymorphism in the Abella proof assistant. ~ G. Nadathur, Y. Wang #ITP #Abella
• Fixing 17 space leaks in GHCi, and keeping them fixed. ~ Simon Marlow (@simonmar) #Haskell
• Computational algebra system in Haskell (Dependently-typed computational algebra system written in Haskell). ~ Hiromi Ishii #Haskell #CAS
• Functional data structures. ~ Prabhakar Ragde #FunctionalProgramming #Algorithms #OCaml
• Libro de exámenes de programación funcional con Haskell (versión del 22 de junio de 2018). #Haskell #I1M2017
• #I1M2017: Libro de ejercicios resueltos de programación funcional en Haskell del curso 2017-18. #Haskell
• Introduction to deep learning (What is deep learning and how can I study it?). ~ Tyler Bettilyon (@TebbaVonMaths) #AI #DeepLearning
• Deep neural networks as computational graphs (DNNs don’t need to be a black box). ~ Tyler Bettilyon (@TebbaVonMaths) #AI #DeepLearning
• Computer and human languages. ~ Diéssica Gurskas (@diessicode) #Programming
• BP: Formal proofs, the fine print and side effects. ~ T- Murray, P.C. van Oorschot #FormalVerification
• Rethinking static reference tables in GHC. ~ Simon Marlow (@simonmar) #Haskell
• What’s the difference? (A functional pearl on subtracting bijections). ~ B.A. Yorgey, K. Foner #Haskell
• Queryparser, an open source tool for parsing and analyzing SQL. ~ Matt Halverson #Haskell
• Lógica práctica y aprendizaje computacional. ~ Jacinto Dávila (@jacintodavila) #Lógica #IA #AprendizajeAutomático
• Computational logic and human thinking: How to be artificially intelligent. ~ Robert Kowalski #eBook #IA #Logic
• Pell’s equation in Isabelle/HOL. ~ Manuel Eberl #ITP #IsabelleHOL #Math
• Making the history of computing. The history of computing in the history of technology and the history of mathematics. ~ L. de Mol, M. Bullynck #History #CompSci #Math
• Notes on discrete mathematics. ~ James Aspnes #eBook #Math
• Fast Sudoku solver in Haskell #1: a simple solution. ~ Abhinav Sarkar (@abhin4v) #Haskell
• Paradigms of Artificial Intelligence programming: case studies in Common Lisp. ~ Peter Norvig #AI #CommonLisp
• Hasktorch: a library for tensors and neural networks in Haskell. #Haskell #AI #MachineLearning
• The automated-reasoning revolution: from theory to practice and back. ~ Moshe Y. Vardi (@vardi) #ATP
• Literate programming with Org-mode. ~ Gregory J Stein (@CachesToCaches) #Emacs #OrgMode
• Logic and proof (Release 0.1). ~ Jeremy Avigad, Robert Y. Lewis, and Floris van Doorn #Logic #LeanTheoremProver
• Coercions and roles for dummies. #Haskell
• Why laziness matters. ~ Ben Lynn #Haskell
• Instalación de “Lean theorem prover”. #ITP #LeanProver
• A web page with resources for teaching with formal methods and tools. ~ Jeremy Avigad #ITP #Logic #Math
• Formal methods in mathematics and the Lean theorem prover. ~ Jeremy Avigad #ITP #Logic #Math
• Machine learning for mathematical software. ~ M. England #MachineLearning #MathematicalSoftware
• Fast verifying proofs of propositional unsatisfiability via window shifting. ~ Jingchao Chen #SAT
• #I1M2017: Soluciones del 7º examen de programación funcional con Haskell. #Haskell
• Libro de exámenes de programación funcional con Haskell (versión 9.7 del 30 de junio de 2018). #Haskell #I1M2017
• The Emacs Commune. #Emacs #History
• forall x: Calgary Remix (An introduction to formal logic). ~ P.D. Magnus, T. Button, J. Robert Loftis, Aaron Thomas-Bolduc, R. Zach #eBook #Logic
• The Shamir secret sharing algorithm in Haskell. ~ Sina Habibian (@sinahab) #Haskell
• Keep your laziness in check. ~ K. Foner et als. #Haskell