Resumen de lecturas compartidas durante noviembre de 2019

Esta entrada es una recopilación de lecturas compartidas, durante noviembre de 2019, 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.

• Neural Networks with Weighty Lenses (DiOptics?) ~ Philip Zucker (@SandMouth). #Haskell #NeuralNetworks #FunctionalProgramming
• The future of work: How new technologies are transforming tasks. ~ M. Fleming et als. #AI #ML
• Compile your comments in ghcid. ~ Jake Keuhlen. #Haskell #FunctionalProgramming
• Scraping Goodreads Sitemaps with Haskell. ~ Marcus Buffett. #Haskell #FunctionalProgramming
• How does the continuation monad work? ~ Max Hallinan. #PureScript #FunctionalProgramming
• Copilot: A stream DSL for writing embedded C programs. ~ Lee Pike (@pike7464). #Haskell #FunctionalProgramming
• Esta IA resuelve un antiguo problema matemático mucho más rápido. #IA
• A basic Haskell solution to the robot journeys coding exercise. ~ Mark Seemann (@ploeh). #Haskell #FunctionalProgramming
• The natural number game (version 1.06). ~ K. Buzzard, M. Pedramfar. #ITP #LeanProver #Math
• Learn Coq in Y minutes tutorial. ~ Philip Zucker (@SandMouth). #ITP #Coq
• No Garden of Eden: Adventures in Teaching Haskell to Kids. ~ Peter Berger (@peterb). #Haskell #FunctionalProgramming
• The story of Logic. ~ Robert L. Constable. #Logic #Math #ITP
• Computational foundations of Mathematics. ~ Robert L. Constable. #Logic Math #CompSci #ITP #Nuprl
• Approximate normalization for gradual dependent types. ~ J. Eremondi, É. Tanter, R. Garcia. #GDTL
• A review of the Lean theorem prover. ~ Thomas Hales. #ITP #LeanProver
• La inteligencia artificial capaz de puntuar con notas sobresalientes en los exámenes de ciencias. ~ @Alvy. #IA
• From ‘F’ to ‘A’ on the N.Y. Regents Science Exams: An Overview of the Aristo Project. ~ P. Clark et als. #AI
• An implementation of Homotopy Type Theory in Isabelle/Pure. ~ J. Chen. #MSc_Thesis #ITP #IsabellePure #HoTT
• A formal proof of PAC learnability for decision stumps. ~ J. Tassarotti, J.B. Tristan, K. Vajjha. #ITP #LeanProver
• How to do binary random-access lists simply. ~ Donnacha Oisín Kidney (@oisdk). #Agda #FunctionalProgramming #ITP
• Unrolling data with Backpack. ~ Oleg Grenrus. #Haskell #FunctionalProgramming
• Category Theory. ~ Jean-Pierre Marquis. #CategoryTheory.
• A brief tour of logic and optimization. ~ J. Hooker. #Logic #Optimization
• Zermelo Fraenkel Set Theory in Higher-Order Logic. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Logic #Math
• Differential Hoare logics and refinement calculi for hybrid systems with Isabelle/HOL. ~ S. Foster, G. Struth. #ITP #IsabelleHOL
• CoqTL: A Coq DSL for rule-based model transformation. ~ Z. Cheng, M. Tisi, R. Douence. #ITP #Coq
• Recent trends in STM Haskell. ~ P. Tiwari, S. Meenu. #Haskell #FunctionalProgramming
• Introduction to univalent foundations of mathematics with Agda. ~ Martín Hötzel Escardó. #ITP #Agda HoTT
• Coq à la carte (A practical approach to modular syntax with binders). ~ Y. Forster, K. Stark. #ITP #Coq
• Fixed points and diagonal arguments. ~ Bartosz Milewski (@BartoszMilewski). #Haskell #Math
• Python VS Common Lisp, workflow and ecosystem. #Python #CommonLisp
• The four simple ways to encode sum-types. ~ Yair Chuchem (@yairchu). #Haskell #FunctionalProgramming
• Proving groups with Idris. ~ Boro Sitnikovski## (@BSitnikovski). #Idris #FunctionalProgramming #ITP
• Predicates vs functions. ~ Paul Brown. #Prolog #LogicProgramming
• Qué es la teoría de categorías y cómo se ha convertido en tendencia. ~ John Baez (@johncarlosbaez). #Teoría_de_categorías #Lógica #Matemáticas #Computación
• El problema de Collatz. ~ Juan Arias de Reyna. #Matemáticas
• Probabilistic programming with Monad‑Bayes, Part 2: Linear regression. ~ S. Bhat, M. Meschede. #Haskell #FunctionalProgramming
• Verified programming of Turing machines in Coq. ~ Y. Forster, F. Kunze, M. Wuttke. #ITP #Coq
• Intuitionistic logic: a view of its evolution. ~ A.K. Peters. #Logic #CompSci
• Minimal logic and automated proof verification. ~ L. Warren. #PhD_Thesis #ITP #Agda #Logic
• Figurate numbers: a historical survey of an ancient mathematics. ~ D. Shane. #Math #History
• Propositions as types: some missing links. ~ Kostiantyn Rybnikov (@ko_bx). #Agda #ITP #Math
• Formalizing expressiveness of line editors. ~ Boro Sitnikovski. #ITP #Coq
• Commanding Emacs from Coq. #ITP #Coq #Emacs
• Goldbach: a curious conjecture. ~ R.J. Lipton, K.W. Regan. #Math
• GHC exercises (A little course to learn about some of the more obscure GHC extensions). ~ Tom Harding (@am_i_tom). #Haskell #FunctionalProgramming
• Linear relation algebra of circuits with HMatrix. ~ Philip Zucker (@SandMouth). #Haskell #FunctionalProgramming
• Smart constructors that cannot fail. ~ Mark Karpov (@mrkkrp). #Haskell #FunctionalProgramming
• Named typeclasses in Haskell. ~ Marco Perone (@marcoshuttle). #Haskell #FunctionalProgramming
• Source-free machine-checked validation of native code in Coq. ~ K.W. Hamlen, D.Fisher, G.R. Lundquist. #ITP #Coq
• Embracing a mechanized formalization gap. ~ A. Spector-Zabusky, J. Breitner, Y. Li, S. Weirich #ITP #Coq #Haskell via @scottfleischman
• A probability theory library for the Coq theorem prover. ~ J. Tassarotti. #ITP #Coq #Math
• Formalizing the dependency pair criterion for innermost termination. ~ A. Alves Almeida, M. Ayala-Rincón. #ITP #PVS
• Computational logic: its origins and applications. ~ L.C. Paulson. #Logic #ITP #IsabelleHOL
• Formalising mathematics in simple type theory. ~ L.C. Paulson. #Logic #Math #ITP #IsabelleHOL
• A small proof that fin is injective. ~ Donnacha Oisín Kidney (@oisdk). #ITP #Agda
• Variational autoencoders in Haskell, or: how I learned to stop worrying and turn my friends into dogs. ~ @heyitdeclan #Haskell #FunctionalProgramming via @SandMouth
• The “many worlds” design pattern. ~ Paulo Moura. #LogicProgramming
• Facts and fluents vs constants and variables. ~ Paul Brown. #Prolog #LogicProgramming
• Abstracting user interaction. ~ Paulo Moura. #LogicProgramming
• Monads in Haskell and category theory. ~ Samuel Grahn. #Haskell #FunctionalProgramming #CategoryTheory
• Cofree traversable functors. ~ L. Waern. #Haskell #FunctionalProgramming #CategoryTheory
• AXolotl: A self-study tool for first-order logic. ~ David M. Cerna. #Logic
• Mathematical knowledge management across formal libraries. ~ D. Müller. #PhD_Thesis #MKM #ITP #PVS
• 2019 state of Haskell survey results. ~ Taylor Fausak (@taylorfausak). #Haskell #FunctionalProgramming
• Forgetting to learn logic programs. ~ Andrew Cropper. #ILP #LogicProgramming
• Swap the DB based on a config file. ~ Grégoire Charvet. #Haskell #FunctionalProgramming
• Encoding problems in boolean satisfiability. ~ Ozan Erdem (@ozanerdem). #Logic #SAT_solving
• Finite field polynomial arithmetic based on fast Fourier transforms. ~ Stephen Diehl (@smdiehl). #Haskell #FunctionalProgramming #Math
• Mi entorno de trabajo en Emacs. ~ Ondiz. #Emacs
• Category theory as a methodology for computational sciences. ~ Xinyuan Sun. #CategoryTheory #Haskell
• Deeply integrating C11 code support into Isabelle/PIDE. ~ F. Tuong, B. Wolff. #ITP #IsabelleHOL
• Deriving magic and parsing CSV. ~ Grégoire Charvet. #Haskell #FunctionalProgramming
• Verified quantum computing. ~ Robert Rand. #ITP #Coq #QuantumComputing
• Formally verified quantum programming. ~ Robert Rand. #PhD_Thesis #ITP #Coq #QuantumComputing
• A quick reference for mapping Coq tactics to Lean tactics. ~ Joey Dodds. #ITP #Coq #LeanProver
• Boring Haskell manifesto (how to get Haskell into your organization, and how to make your organization more productive and profitable with better engineering). ~ M. Snoyman (@snoyberg). #Haskell #FunctionalProgramming
• Barbara Liskov: The architect of modern algorithms. ~ Susan D’Agostino (@susan_dagostino). #CompSci #Algorithms
• Links to recourses for the Lean Theorem Prover. ~ Floris van Doorn. #ITP #LeanProver
• A bare-bones Twitter clone implemented with Haskell + Nix. ~ Gabriel Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming
• CodeWorld import by Hash. ~ Chris Smith (@cdsmithus). #CodeWorld #Haskell
• Certification of breadth-first algorithms by extraction~ D. Larchey-Wendling, R. Matthes. #Coq
• Verified self-explaining computation. ~ J. Stolarek, J. Cheney. #ITP #Coq
• The 2019/2020 edition of Strathclyde’s CS316 Functional Programming course. ~ Bob Atkey. #Haskell #FunctionalProgramming
• Tools for tutoring theoretical computer science topics. ~ Mark McCartin-Lim. #PhD_Thesis #CompSci #Logic #ATP
• Formally verified insertion of reference counting instructions. ~ Marc Huisinga. #ITP #LeanProver
• A collection of resources for learning type theory and type theory adjacent fields. ~ Daniel Gratzer. #TypeTheory #CategoryTheory #ITP #Coq #LeanProver #HoTT
• Constructing infinitary quotient-inductive types. ~ M. Fiore, A.M. Pitts, S.C. Steenkamp. #ITP #Agda
• ConCert: A smart contract certification framework in Coq. ~ D. Annenkov, J.B. Nielsen, B. Spitters. #ITP #Coq #Blockchain
• ConCert: A framework for smart contract verification in Coq. ~ J.B. Nielsen, D. Annenkov. #ITP #Coq #Blockchain
• The sequent calculus calculator. ~ Matteo Kamm, Mike Marti. #BsC_Thesis #Logic #ITP #Elm #FunctionalProgramming
• Sequent calculus calculator. #Logic #ITP
• Kairos: a Haskell library for live coding Csound performances. ~ L. Foletto. #Haskell #FunctionalProgramming #Music
• Supporting the Algebra I curriculum with an introduction to computational thinking course. ~ M.M. Laskowski. #MsC_Thesis #CodeWorld #Haskell #Teaching
• Libro de exámenes de programación funcional con Haskell (versión del 25 de noviembre de 2019). #ProgramaciónFuncional #Haskell #I1M2019
• Abstractions and constructions from math, implementations in FP languages and formalizations in proof assistants. ~ P. Paradziński. #CategoryTheory
• PLT: A path to enlightenment in Programming Language Theory. ~ Steven Shaw (@steshaw). #Programming #TypeTheory #FunctionalProgramming #CategoryTheory via @pparadzinski
• RustBelt: Securing the foundations of the Rust programming language. ~ Ralf Jung et als. #ITP #Coq #Rust
• From math to machine: translating a function to machine code. ~ Brian Steffens (@brian_steffens). #Haskell #Math
• Digging into Rust’s syntax. ~ James Bowen (@james_OWA). #Programming #Rust #Haskell
• Conway’s game of life using Haskell and Gloss. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming #Gloss
• Categorical LQR control with linear relations. ~ Philip Zucker (@SandMouth). #Haskell #FunctionalProgramming
• Supercharged imperative programming with Haskell and FP. ~ Anupam Jain (@ajnsit). #Haskell #FunctionalProgramming
• The enormous theorem. ~ Sarah Spoenemann. #Math
• Introducción a la “Introducción de Emacs”. #Emacs
• Development of group theory in the language of internal set theory. ~ Zoltan Kocsis #PhD_Thesis #ITP #Agda #Logic #Math
• Structured induction proofs in Isabelle/Isar. ~ M. Wenzel. #ITP #IsabelleHOL
• Property invariant embedding for automated reasoning. ~ M. Olšák, C. Kaliszyk, J. Urban. #ATP #MachineLearnig
• How to learn Haskell in 10 minutes a day. ~ Yulia Gavrilova. #Haskell #FunctionalProgramming
• The Makam metalanguage: a tool for rapid language prototyping. ~ Antonis Stampoulis. #Programming #Makam #OCaml
• How to make your papers run: Executable formal semantics for your language. ~ Teodoro Freund. #Programming #Makam
• The Mind at Work: Guido van Rossum on how Python makes thinking in code easier. ~ Anthony Wing Kosner. #Programming #Python
• The revolution in computing education at school: opportunity and challenge. ~ Simon Peyton Jones. #CompSci #Teaching