Resumen de lecturas compartidas durante marzo de 2019

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

• Monoidal and applicative functors. ~ Marcin Szamotulski. #Haskell #FunctionalProgramming
• Property-based testing in a screencast editor: Introduction. ~ Oskar Wickström. #Haskell
• Beeraffe: A silly game in PureScript. ~ Jasper Van der Jeugt. #PureScript
• Recursion schemes, part VI: Comonads, composition, and generality. ~ Patrick Thomson. #Haskell
• Beautiful Racket (an introduction to language oriented programming using Racket). ~ Matthew Butterick. #Racket #Programming
• Functional programming in OCaml. ~ Michael R. Clarkson. #eBook #OCaml #FunctionalProgramming
• Lazy validation. ~ Roman Cheplyaka. #Haskell
• The basics of game programming in Common Lisp. ~ Mauricio Fernandez. #CommonLisp
• Using Julia for Data Science (Part 02). ~ Cleyton Farias. #JuliaLang #DataScience
• Pourquoi créer des nouveaux langages de programmation? ~ Ludovic Henrio. #Programmation
• Matplotlib guide for people in a hurry. ~ Julia Kho. #Python #Matplotlib
• Selective applicative functors: declare your effects statically, select which to execute dynamically. ~ A. Mokhov. #Haskell
• Isomorphic web apps in Haskell. ~ Julien Dehos. #Haskell
• Programmation fonctionnelle pour le web. ~ Julien Dehos. #Haskell
• Neural network in 42 lines of Haskell. ~ Julien Dehos. #Haskell
• Shareable Haskell with Jupyter! ~ James Bowen. #Haskell #Jupyter
• Infinite types, infinite data, infinite interaction. ~ P. Hyvernat. #ITP #Agda
• Means compatible with semigroup laws. ~ R. Padmanabhan, A. Shukla. #ATP #Prover9 #Math
• Introduction to theoretical computer science. ~ Boaz Barak. #eBook #CompSci
• DimDraw: A novel tool for drawing concept lattices. ~ D. Dürrschnabel, T. Hanika, G. Stumme. #AFC
• Type classes for mathematics in type theory. ~ B. Spitters, E. van der Weegen. #ITP #Coq #Math
• A library of formalised undecidable problems in Coq. ~ Dominique Larchey-Wendling et als. #ITP #Coq
• GRUNGE: A grand unified ATP challenge. ~ C.E. Brown, T. Gauthier, C. Kaliszyk, G. Sutcliffe, J. Urban. #ATP
• The state of Haskell in Ethereum. ~ Martin Allen. #Haskell
• Why I use Julia. (Come for the speed. Stay for the productivity). ~ Josh Day #LuliaLang
• What exactly makes the Haskell type system so revered (vs say, Java)? #Haskell #FunctionalProgramming
• Computer-assisted proving of combinatorial conjectures over finite domains: A case study of a chess conjecture. ~ P. Janičić, F. Marić, M. Maliković. #ITP #IsabelleHOL #ATP #SAT #SMT
• Dijkstra monads for all. ~ K. Maillard et als. #ITP #Coq
• Stack cookbook. #Haskell #Stack
• Rust for linear algebra and neural networks. ~ J.P. Moresmau. #RustLang #AI #MachineLearnig #Math
• On Lamport’s critique of compositional reasoning. ~ Ilya Sergey. #Programming
• Why Jupyter is not my ideal notebook. ~ Clément Walter. #Jupyter
• From free algebras to free monads. ~ Marcin Szamotulski. #Haskell #CategoryTheory
• Category theory for computing science. ~ M. Barr, C. Wells. #eBook #CategoryTheory
• What are the advantages/disadvantages of uLisp vs C/C++? #Programming #Lisp #Cpp
• An example of state-based testing in Haskell. ~ Mark Seemann. #Haskell
• 33 can be written as the sum of three cubes. ~ Peter Rowlett. #Math #CompSci
• Gödel without (too many) tears. ~ Peter Smith. #Logic
• AI efforts at large companies may be hindered by poor quality data. #AI
• Learning a SAT solver from single-bit supervision. ~ D. Selsam et als. #SAT #Logic #MachineLearnig
• On constructive-deductive method for plane euclidean geometry. ~ E.V. Ivashkevich. #ITP #Coq #Math
• Typeable and Data in Haskell. ~ Chris Done. #Haskell #FunctionalProgramming
• From math to machine: translating a function to machine code. ~ Brian Steffens #Haskell #Math
• Writing a simple evaluator and type-checker in Haskell. ~ Boro Sitnikovski. #Haskell
• These years in Common Lisp: 2018. ~ Vince Zd #CommonLisp
• Visible dependent quantification in Haskell. ~ Ryan Scott. #Haskell
• Cooking a Haskell curry with applicative functors. ~ G. Érdi. #Haskell
• Logipedia: a multi-system encyclopedia of formal proofs. ~ G. Dowek, F. Thiré. #ITP #Logic #Math #Dedukti #Coq #Matita #HOL_Light #PVS #LeanProver
• A framework for defining computational higher-order logics. ~ A. Assaf. #PhD_Thesis #ITP #Logic #Math #Dedukti
• Nine chapters of analytic number theory in Isabelle/HOL. ~ M. Eberl. #ITP #IsabelleHOL #Math
• Liquidate your assets (Reasoning about resource usage in Liquid Haskell). ~ M. Handley, N. Vazou, G. Hutton. #Haskell
• Machine learning and the Continuum Hypothesis. ~ K.P. Hart. #MachineLearnig #SetTheory
• Extending Haskell’s syntax! ~ James Bowen. #Haskell #FunctionalProgramming
• Compdata trees and catamorphisms. ~ Ben Blaxill. #Haskell #FunctionalProgramming
• Pure maths in crisis? ~ M. Freiberger. #Math #ITP #IsabelleHOL #LeanProver
• Writing a lambda calculus evaluator in Haskell. ~ B. Sitnikovski. #Haskell #FunctionalProgramming #LambdaCalculus
• Map/Reduce operations for scientific computing in Julia. ~ X. Vasseur. #JuliaLang
• Introduction to Univalent Foundations of Mathematics with Agda. ~ Martín Hötzel Escardó. #ITP #Agda #math #HoTT
• What is a proof? What should it be? ~ C. Benzmüller. #Logic #Math #ITP #ATP
• FMS: Functional programming as a modelling language. ~ I. Dasseville, G. Janssens. #FunctionalProgramming #ASP
• FMS (Functional Modelling System) tutorial. ~ I. Dasseville. #FunctionalProgramming #ASP
• Lazy binary numbers. ~ Donnacha Oisín Kidney. #Haskell #Agda
• Fractals and monads (Part 3). ~ Derek Wise. #Haskell #Math
• A small use case for Deriving Via. ~ Sam Tay. #Haskell
• Okay, maybe proofs aren’t dying after all. ~ J. Horgan. #Math
• An introduction to existential types. ~ S. Bly. #FunctionalProgramming
• A constructive proof of dependent choice in classical arithmetic via memoization. ~ É. Miquey. #ITP #Coq
• Algorithms for verifying deep neural networks. ~ C. Liu, T. Arnon, C. Lazarus, C. Barrett, M.J. Kochenderfer. #JuliaLang #NeuralNetworks
• Introduction to Python for science and engineering. ~ D.J. Pine. #eBook #Programming #Python
• Computer science and metaphysics: a cross-fertilization. ~ D. Kirchner, C. Benzmüller, E.N. Zalta. #ITP #IsabelleHOL
• Permutations by sorting. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming
• Tagless final encoding in Haskell. ~ J.P. Royo. #Haskell #FunctionalProgramming
• Quantum Hoare logic in Isabelle/HOL. ~ J. Liu et als. #ITP #IsabelleHOL
• Using SMT solvers to validate models for AI problems. ~ A. Arusoaie, I. Pistol. #ATP #SMT #AI
• Universal (meta-) logical reasoning: The wise men puzzle (Isabelle/HOL dataset). ~ C. Benzmüller. #ITP #IsabelleHOL #Logic
• A verifiable search for projective planes of order ten. ~ C. Bright. #ATP #SAT #Math
• The SAT+CAS method for combinatorial search with applications to best matrices. ~ C. Bright et als. #ATP #SAT #CAS #Math
• Comonadic builders. ~ Dmitrii Kovanikov. #Haskell #FunctionalProgramming
• The minimalist Prelude … or why can’t Haskell be more like Purescript? #Haskell #FunctionalProgramming
• Finger trees in Agda. ~ Donnacha Oisín Kidney. #Agda
• Promonads, arrows, and Einstein notation for profunctors. ~ Bartosz Milewski. #Haskel #CategoryTheory
• The transcendence of certain infinite series in Isabelle/HOL. ~ A, Koutsoukou-Argyraki, W. Li. #ITP #IsabelleHOL #Math
• A formal, classical proof of the Hahn-Banach theorem. ~ M. Kerjean, A. Mahboubi. #ITP #Coq #Math
• Partial type constructors (extended version). ~ M.P. Jones et als. #Haskell #FunctionalProgramming
• Towards a constructive formalization of Perfect Graph Theorems (Slides)]. ~ A.K. Singh. R. Natarajan. #ITP #Coq #Math
• Towards a constructive formalization of Perfect Graph Theorems. ~ A.K. Singh. R. Natarajan. #ITP #Coq #Math