Resumen de lecturas compartidas durante octubre de 2018

Esta entrada es una recopilación de lecturas compartidas, durante octubre de 2018, en Twitter fundamentalmente 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.

Una recopilación de todas las lecturas compartidas se encuentra en GitHub.

• From algebra to abstract machine: a verified generic construction. ~ C. Tomé Cortiñas, W. Swierstra. #FunctionalProgramming #ITP #Agda
• Refinement kinds (A theory of type-safe meta-programming). ~ L. Caires, B. Toninho. #FunctionalProgramming #Haskell
• Typing the wild in Erlang. ~ N. Valliappan, J. Hughes. #FunctionalProgramming #Erlang
• An introduction to probabilistic programming. ~ J.W. van de Meent, B. Paige, H. Yang, F. Wood. #FunctionalProgramming #Lisp #Clojure #FOPPL
• RMSbolt: A supercharged implementation of the godbolt compiler-explorer for Emacs. ~ Jay Kamat. #Programming #Emacs
• Resumen de lecturas compartidas durante septiembre de 2018.
• The transcendence of π in Isabelle/HOL. ~ M. Eberl. #ITP #isabelleHOL #Math
• Proving in the Isabelle proof assistant that the set of real numbers is not countable. ~ J. Villadsen. #ITP #isabelleHOL #Math
• Students’ Proof Assistant (SPA). ~ A. Schlichtkrull, J. Villadsen, A.H. From. #ITP #IsabelleHOL #Logic
• Introduction to Singletons (Part 3). ~ Justin Le. #Haskell
• Introducing Haskell to a company. ~ Brian Jones. #FunctionalProgramming #Haskell
• Formalization of logic in the Isabelle proof assistant. ~ A. Schlichtkrull. #PhD_Thesis #ITP #IsabelleHOL #Logic
• Representation matters: An unexpected property of polynomial rings and its consequences for formalizing abstract field theory. ~ C. Schwarzweller. #ITP #Mizar #Math
• AI benchmark: Running deep neural networks on Android smartphones. ~ A. Ignatov et als. #AI #DeepLearning
• Automatic diagnosis and correction of logical errors for functional programming assignments. ~ J. Lee et als. #FunctionalProgramming #OCaml via @scottfleischman
• Random testing for language design. ~ L. Lampropoulos. #PhD_Thesis #ITP #Coq #QuickChick
• Productive Haskell in enterprise. ~ Brian Jones. #FunctionalProgramming #Haskell
• Rewrite rules and a specific fold: use optimization techniques from GHC.Base. ~ Alexandre Moine. #FunctionalProgramming #Haskell
• Haskell study plan (an opinionated list of resources for learning Haskell). ~ Gil Mizrahi. #FunctionalProgramming #Haskell
• An application of ASP theories of intentions to understanding restaurant scenarios: insights and narrative corpus. ~ Q. Zhang, C. Benton, D. Inclezan. #LogicProgramming #ASP
• anthem: Transforming gringo programs into first-order theories (preliminary report). ~ V. Lifschitz, P. Lühne, T. Schaub. #LogicProgramming #ASP #ATP
• A review of the Lean theorem prover. ~ Thomas Hales. #ITP #LeanTheoremProver
• Formalizing 100 theorems in Coq. #ITP #Coq #Math
• capability: the ReaderT pattern without boilerplate. ~ A. Herrmann, A. Spiwack. #FunctionalProgramming #Haskell
• A gently curated list of companies using Haskell in industry. ~ Erik Mossberg #FunctionalProgramming #Haskell
• Ten things you should know about Haskell syntax. ~ Bartosz Milewski #FunctionalProgramming #Haskell
• 4 reasons why Python isn’t the programming language for you. ~ Ian Buckley #Programming #Python
• What is the Xena Project? ~ Kevin Buzzard #ITP #LeanTheoremProver #Math
• Counting inversions with monoidal sparks. ~ Brent Yorgey #FunctionalProgramming #Haskell #Math
• Keep your types small … and your bugs smaller. ~ Matt Parsons . #FunctionalProgramming #Haskell
• Monads for functional programming in Scala. ~ Daniel Berg #FunctionalProgramming #Scala
• A new algebraic approach to decision making in a railway interlocking system based on preprocess. ~ A. Hernando, R. Maestre, E. Roanes-Lozano. #Math #CompSci
• Companion webpage to the book “Mathematics for Machine Learning”. ~ Marc Peter Deisenroth, A Aldo Faisal, and Cheng Soon Ong. #eBook #MachineLearning #Math
• Detailed walkthrough for a beginner Haskell program. ~ G. Gonzalez . #FunctionalProgramming #Haskell
• Comprehending Monoids with Class. ~ Lionel Parreaux #FunctionalProgramming #Haskell
• Deeper Stack knowledge. ~ James Bowen . #FunctionalProgramming #Haskell
• Learn Haskell in one video. ~ Derek Banas. #FunctionalProgramming #Haskell
• Division of polynomials in Haskell. ~ Philip Zucker. #FunctionalProgramming #Haskell #Math
• Wikistat 2.0: Educational resources for Artificial Intelligence. ~ P. Besse, B. Guillouet, B. Laurent #AI
• Wikistat 2.0: Tutoriels (calepins jupyter) d’auto-apprentissage en Science des Données & Intelligence artificielle. #DataScience #AI
• Fractals and the Weierstrass-Mandelbrot function. ~ A. Zaleski #Math
• Formal verification of helicopter automatic landing control algorithm in theorem prover Coq. ~ X. Chen, G. Chen. #ITP #Coq
• Suggesting valid hole fits for typed-holes in Haskell. ~ Matthías Páll Gissurarson. #Msc_Thesis #FunctionalProgramming #Haskell
• Propositional logic with short-circuit evaluation: a non-commutative and a commutative variant. ~ J.A. Bergstra, A. Ponse, D.J.C. Staudt. #Logic #ATP #Prover9
• Making a Haskell interface for the Rosie Pattern Language. ~ Laurence Emms. #FunctionalProgramming #Haskell
• The fundamental theorem of algebra in ACL2. ~ R. Gamboa, J. Cowles. #ITP #ACL2 #Math
• Using ACL2 in the design of efficient, verifiable data structures for high-assurance systems. ~ D. Hardin, K. Slind. #ITP #ACL2
• An introduction to linear regression using Haskell. ~ Sam Gardner. #FunctionalProgramming #Haskell
• Why are functional programming languages so popular in the programming languages community? #FunctionalProgramming
• The art of Prolog, second edition (Advanced programming techniques). ~ L.S. Sterling, E.Y. Shapiro. #Open #eBook #LogicProgramming #Prolog
• Real vector spaces and the Cauchy-Schwarz inequality in ACL2(r). ~ C. Kwan, M.R. Greenstreet. #ITP #ACL2 #Math
• IsaK: a complete semantics of K. ~ L. Li, E.L. Gunter. #ITP #IsabelleHOL
• Hask Anything!: a website aimed at collecting and organizing the collective knowledge of the Haskell community. #FunctionalProgramming #Haskell
• Functional programming. #FunctionalProgramming #Haskell
• The US military wants to teach AI some basic common sense. ~ Will Knight. #AI
• An implementation of Homotopy Type Theory in Isabelle/Pure. ~ J. Chen . #Msc_Thesis #ITP #Isabelle #HoTT
• Isabelle/HoTT: An experimental implementation of HoTT in the interactive proof assistant Isabelle. J. Chen. #ITP #Isabelle #HoTT
• A tutorial introduction to CryptHOL. ~ A. Lochbihler, S.R. Sefidgar. #ITP #IsabelleHOL #CryptHOL
• Formalising filesystems in the ACL2 theorem prover: an Application to FAT32. ~ Mihir Parang Mehta. #ITP #ACL2
• Practical Haskell programs from scratch (a quick and easy guide). #FunctionalProgramming #Haskell
• Headfirst into Haskell. ~ Abby Sassel. #FunctionalProgramming #Haskell
• Towards verified, constant-time floating point operations. ~ M. Andrysco et als. #FunctionalProgramming #Haskell #SMT
• Dependent types in Haskell: Binomial heaps 101 (Who put binary numbers in my type system?). ~ Jasper Van der Jeugt. #FunctionalProgramming #Haskell
• Incremental SAT library integration in ACL2 using abstract stobjs. ~ Sol Swords. #ITP #ACL2 #SAT
• #HIW18: Let’s go mainstream with Eta!. ~ Rahul Muttineni . #FunctionalProgramming #Haskell #Eta
• CoreSpec: Verifying GHC with hs-to-coq. ~ Antal Spector-Zabusky et als. #FunctionalProgramming #Haskell #ITP #Coq
• Coercion quantification. ~ N. Xie, R.A. Eisenberg. #FunctionalProgramming #Haskell
• Aelve Guide: Wiki for the Haskell ecosystem. #Haskell
• Enlaces y recursos sobre redes neuronales y deep learning. ~ @ajlopez #AI #NeuralNetworks #DeepLearning
• Convex functions in ACL2(r). ~ C. Kwan, M.R. Greenstreet. #ITP #ACL2 #Math
• ESCRIPT: a human readable language for programming Bitcoin scripts. ~ Rick Klomp. #FunctionalProgramming #Haskell
• SCRIPT Analyser: Symbolic verification of Bitcoin’s output scripts. ~ Rick Klomp. #FunctionalProgramming #Haskell
• Fixpoints in Haskell. ~ Chris Smith. #FunctionalProgramming #Haskell
• A JavaScript WAT and monoidal folds. ~ Julie Moronuki and Chris Martin. #JavaScript #Haskell #FunctionalProgramming
• Orgstat: a statistics visualizer tool for org-mode. ~ Mikhail Volkhov. #Haskell #Emacs #OrgMode
• A Haskell Enigma machine simulator with rich display and machine state details. #FunctionalProgramming #Haskell
• Haskell in industry. #FunctionalProgramming #Haskell
• Learn programming. ~ A. Salonen. #eBook #Programming #OpenLibra
• Learning to reason (Theorem proving at first order via reinforcement learning). ~ Brian Groenke. #Logic #ATP #MachineLearning
• How Lisp became God’s own programming language. ~ Sinclair Target . #Programming #Lisp
• DefunT: A tool for automating termination proofs by using the community books. ~ Matt Kaufmann. #ITP #ACL2
• Cedille-Core: A minimal (600 LOC) programming language capable of proving theorems about its own terms. #ITP #Logic #FunctionalProgramming #Haskell
• Formality: An efficient programming language and proof assistant. #ITP #Cedille
• DBFunctor: Functional data management (type safe ETL/ELT in Haskell). ~ Nikos Karagiannidis. #FunctionalProgramming #Haskell
• Problem solving vs proving. ~ Anthony Bonato #Math
• Upper bounding diameters of state spaces of factored transition systems in Isabelle/HOL. F. Kurz and M. Abdulaziz. #ITP #IsabelleHOL
• Granule: a statically typed functional language with graded modal types for fine-grained program reasoning via types. ~ Dominic Orchard #FunctionalProgramming #Haskell
• Programming language foundations in Agda. ~ P. Wadler. #ITP #Agda #Coq
• Programming language foundations in Agda. ~ P. Wadler, W. Kokke. #eBook #ITP #Agda #Coq
• Temporal properties of smart contracts. ~ I. Sergey, A. Kumar, A. Hobor. #ITP #Coq
• Logics and symbolic Artificial Intelligence. ~ Isabelle Bloch, Natalia Díaz Rodríguez. #AI #Logic
• Randomised binary search trees in Isabelle/HOL. ~ M. Eberl #ITP #IsabelleHOL
• Haskell’s kind system (a primer). ~ D. Castro. #Haskell
• An applicative password list. ~ M. Seemann. #FunctionalProgramming #Haskell
• Sigma, Pi, Sum, Product. ~ Samuel Breese. #FunctionalProgramming #Haskell
• AI today and tomorrow is mostly about curve fitting, not intelligence. ~ Kurt Marko. #AI #DeepLearning
• Máquinas listas, pero sin sentido común. ~ Ramon López de Mántaras. #IA
• Building machines that learn and thinlike people. ~ B.M. Lake, T.D. Ullman, J.B. Tenenbaum, S.J. Gershman. #AI
• Algorithmes: à la recherche de l’universalité perdue. ~ Rachid Guerraoui #CompSci
• Proofs and side effects (Understanding the promise and the fine print of formal methods for security). ~ Toby Murray. #ITP
• BP: Formal proofs, the fine print and side effects. ~ T. Murray, P.C. van Oorscho. #ITP
• Running from the past. ~ Dan Piponi. #FunctionalProgramming #Haskell
• Mark Dominus: I struggle to understand Traversable. #FunctionalProgramming #Haskell
• The Haskell Cookbook. #FunctionalProgramming #Haskell
• Browsing the Web with Common Lisp. #Lisp #CommonLisp #Web #NextBrowser
• Next: a keyboard-oriented, extensible web-browser inspired by Emacs and designed for power users. #Lisp #CommonLisp #Web #NextBrowser
• Formalizing computability theory via partial recursive functions. ~ M. Carneiro. #ITP #Lean
• A denotational semantics for an imperative language. ~ G. Malecha . #ITP #Coq
• Formalization of the embedding path order for lambda-free higher-order terms. ~ A. Bentkamp. #ITP #IsabelleHOL
• REST-ish services in Haskell (Part 1). ~ @vadosware #FunctionalProgramming #Haskell
• Some computer algebra algorithms in Haskell. ~ J. Pellejero. #FunctionalProgramming #Haskell #Math
• An invitation to category theory. ~ Tai-Danae Bradley. #CategoryTheory
• Layer systems for confluence — formalized. ~ B. Felgenhauer, F. Rapp #ITP #IsabelleHOL
• The prime number theorem in Isabelle/HOL. ~ M. Eberl, L. Paulson. #ITP #IsabelleHOL #Math
• Elm: Functional frontend! ~ James Bowen. #FunctionalProgramming #Elm
• Introduction to Singletons (Part 4). ~ Justin Le. #Haskell #FunctionalProgramming
• Evolution of Emacs Lisp. ~ S. Monnier, M. Sperber. #Emacs #Lisp
• Principles of algorithmic problem solving. ~ J. Sannemo. #eBook #Algorithms #Programming #CompSci
• The student debt crisis: Could it slow the U.S. economy?
• Deriving proved equality tests in Coq-elpi (Stronger induction principles for containers in Coq). ~ E. Tassi. #ITP #Coq
• In computers we trust? (As math grows ever more complex, will computers reign?) #Math #CompSci #ITP
• Alchemy: A Language and Compiler for Homomorphic Encryption Made easY. ~ E. Crockett, C. Peikert, C. Sharp. #Haskell #FunctionalProgramming
• Typed functional programming and software correctness. ~ Marko Dimjašević. #FunctionalProgramming
• Algebraic Data Types in four languages (A comparison). ~ #Haskell #Scala #Rust #TypeScript
• Third wave AI: The coming revolution in Artificial Intelligence. ~ Scott Jones. #AI
• A DARPA perspective on Artificial Intelligence. ~ John Launchbury. #AI
• Can we trust AI if we don’t know how it works? ~ Marianne Lehnis. #AI
• Assuring AI. ~ John Launchbury. #AI
• CodeWorld guide. ~ Chris Smith. #Haskell #CodeWorld #FunctionalProgramming
• Solving russian calendar problems in Haskell (HaskellRank Ep.08). ~ Alexey Kutepov. #FunctionalProgramming #Haskell
• Los cuadrados y la factorización. ~ Juan Arias de Reyna. #Matematicas #Computacion
• A tale of two sieves. ~ C. Pomerance. #Math #CompSci
• AI, explain yourself. ~ Don Monroe. #AI #XAI
• US Department of Defense commits $2B to training AI to have “common sense”. #AI
• AI talent pipeline clogged by education programs slow or unable to change. #AI
• Para qué sirven las matemáticas. ~ Francisco R. Villatoro #Matemáticas
• The unplanned impact of mathematics. ~ P. Rowlett. #Math
• Build your own monads. ~ A. Serrano. #FunctionalProgramming #Haskell
• Wise man’s Haskell (Free book for learning Haskell). ~ Andre Popovitch. #eBook #FunctionalProgramming #Haskell
• Headfirst into Haskell. ~ Abby Sassel. #FunctionalProgramming #Haskell
• Testing in the World of Functional Programming. ~ Luka Jacobowitz . #FunctionalProgramming #Scala
• Statistics and data science degrees: Overhyped or the real deal? ~ P. Richard Hahn #DataScience
• A functional paradigm using the C language for teaching Programming for Engineers. ~ V. Theoktisto. #Teaching #Programming #FunctionalProgramming
• Legal representation and reasoning in practice: a critical comparison. ~ S. Batsakis et als. #KRR #ASP #Logic #AI
• The periodic table of data structures. ~ S. Idreos et als. #Algorithmic
• The internals of the data calculator. ~ S. Idreos et als. #Algorithmic
• Epistemic logic in Isabelle/HOL. ~ Andreas Halkjær From . #ITP #IsabelleHOL #Logic
• Creating a card game in Haskell (part 4). ~ Valentin Robert #FunctionalProgramming #Haskell
• Fourier, Cantor, las series trigonométricas y la teoría de conjuntos. ~ Pedro J. Paúl #Matemáticas
• Typed functional programming and software correctness. ~ Marko Dimjašević. #FunctionalProgramming #Haskell #Agda
• Introduction to state machine testing: part 1. ~ Andrew McMiddlin #FunctionalProgramming #Haskell
• Pragmatic development in Eta. ~ Nick Tchayka. #FunctionalProgramming #Haskell #Eta
• Course CIS 252: Introduction to Computer Science. ~ Susan Older #FunctionalProgramming #Haskell
• A trustworthy mechanized formalization of R. ~ M. Bodin, T. Diaz, É. Tanter. #ITP #Coq #RStat
• Attack trees in Isabelle. ~ F. Kammüller. #ITP #IsabelleHOL
• A generic Coq proof of typical worst-case analysis. ~ P. Fradet, M. Lesourd, J.F. Monin, S. Quinton. #ITP #Coq
• A simple implementation of affine spaces and vector spaces in Haskell. #FunctionalProgramming #Haskell #Math
• The laws of natural deduction in inference by DNA computer. ~ Ł. Rogowski, P. Sosík. #Logic #DNAcomputing