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