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