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