Resumen de lecturas compartidas durante mayo de 2020
Esta entrada es una recopilación de lecturas compartidas, durante mayo de 2020, 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.
- Gaussian integers in Isabelle/HOL. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
- Power sum polynomials and the Girard–Newton theorem in Isabelle/HOL. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
- The Ramanujan Machine: Automatically generated conjectures on fundamental constants. ~ Gal Raayoni et als. #MachineLearning #Math
- UWisconsin course on Haskell and Rust. #Haskell #Rust
- Learn to moonwalk with waterflow problem. ~ Murat Kasimov. #Haskell #FunctionalProgramming
- Property testing in depth: genvalidity’s fixed-size type generators. ~ Tom Sydney Kerckhove. #Haskell #QuickCheck
- New AI enables teachers to rapidly develop intelligent tutoring systems. #AI #Teaching
- Verified certification of reachability checking for timed automata. ~ Simon Wimmer, Joshua von Mutius. #ITP #IsabelleHOL
- Formalized proofs of the infinity and normal form predicates in the first-order theory of rewriting. ~ Alexander Lochmann, Aart Middeldorp. #ITP #IsabelleHOL
- Formal proof of the group law for Edwards elliptic curves. ~ Thomas Hales, Rodrigo Raya. #ITP #IsabelleHOL #Math
- Formal adventures in convex and conical spaces. ~ Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. #ITP #Coq #Math
- More random access lists. ~ Donnacha Oisín Kidney (@oisdk). #Haskell #FunctionalProgramming
- History of Logo. ~ C. Solomon et als. #Logo #Programming
- Interactive teaching of programming language theory with a proof assistant. ~ Horpácsi Dániel et als. #ITP #Coq
- A problem-based curriculum for algorithmic programming. ~ Nikházy László. #Programming
- Bye-bye Python. Hello Julia! ~ Rhea Moutafis (@RheaMoutafis). #Python #JuliaLang #Programming
- Design by Contract with Lean theorem prover. ~ Nam Nguyen. #ITP #LeanProver #Programming
- Data flow – what functional programming and Unix philosophy can teach us about data streaming. ~ Bartosz Mikulski (@mikulskibartosz). #FunctionalProgramming
- Intervals and their relations. ~ Marco Perone (@marcoshuttle). #Haskell #FunctionalProgramming #Math
- Frozen lake in Haskell. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming #AI
- Advanced programming languages. ~ Matt Might (@mattmight). #Haskell #Scala #SML #OCaml #Scheme #FunctionalProgramming
- The age of algorithms. ~ Serge Abiteboul, Gilles Dowek. #eBook #Algorithms
- Proving theorems with computers. ~ Kevin Buzzard. #ITP #Math
- Formalization of forcing in Isabelle/ZF. ~ Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf. #ITP #IsabelleZF #Logic
- Banach-Steinhaus theorem in Isabelle/HOL. ~ Dominique Unruh, Jose Manuel Rodriguez Caballero. #ITP #IsabelleHOL #Math
- Eat Haskell string types for breakfast. ~ Ziyang Liu. #Haskell #FunctionalProgramming
- Environment variables parsing for free (applicatives). ~ Clément Delafargue. #Haskell #FunctionalProgramming
- Monoids as one-object categories, or not? ~ @Iceland_jack #Haskell #FunctionalProgramming #CategoryTheory
- π with leftovers: a mechanisation in Agda. ~ Uma Zalakain, Ornela Dardha. #ITP #Agda
- The Chalmers online functional programming seminar series. #FunctionalProgramming
- An efficient normalisation procedure for linear temporal logic: Isabelle/HOL formalisation. ~ Salomon Sickert. #ITP #IsabelleHOL
- Matrices for ODEs in Isabelle/HOL. ~ Jonathan Julian Huerta y Munive. #ITP #IsabelleHOL #Math
- A linear algebra approach to linear metatheory. ~ James Wood, Robert Atkey. #ITP #Agda
- Certified semantics for relational programming. ~ Dmitry Rozplokhas, Andrey Vyatkin, Dmitry Boulytchev. #ITP #Coq
- Why is Lisp not as popular as Python? ~ Jan Meww (@JanMeww). #Python #CommonLisp #Scheme #Clojure
- Learning programs by learning from failures. ~ Andrew Cropper, Rolf Morel. #ILP #MachineLearning #LogicProgramming
- Clean vs. defaulty representations in Prolog. ~ Markus Triska (@MarkusTriska). #Prolog #LogicProgramming
- Diagram chasing in interactive theorem proving. ~ Markus Himmel. #BsC_Thesis #ITP #LeanProver #Math
- Learning selection strategies in Buchberger’s algorithm. ~ Dylan Peifer, Michael Stillman, Daniel Halpern-Leistner. #MachineLearning #Math
- On the effect of learned clauses on stochastic local search. ~ Jan-Hendrik Lorenz, Florian Wörz. #ATP #SAT_solvers
- L’intelligence artificielle et l’apprentissage profond. ~ Benjamin Bradu. #AI #DeepLearning
- Extensions. ~ Veronika Romashkina (@vrom911). #Haskell #FunctionalProgramming
- Indexed monads: examples and discussion. ~ Adam Wespiser (@wespiser). #Haskell #FunctionalProgramming
- The origins and motivations of univalent foundations (A personal mission to develop computer proof verification to avoid mathematical mistakes). ~ Vladimir Voevodsky (2014). #Logic #Math #ITP via @AngelikiKoutso1
- Evolution of Emacs Lisp. ~ Stefan Monnier et als. #Emacs #Lisp
- 15 reasons why I use Emacs, with GIFs. ~ Dominik Tarnowski. #Emacs
- Blackjack: Following the patterns. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming #AI
- Recursion theorem in ZF. ~ Georgy Dunaev. #ITP #IsabelleZF #Logic #Math
- Haskell: Function application vs fmap vs sequential application vs bind. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming
- The science behind functional programming. ~ Rafa Paradela. #CategoryTheory #FuncionalProgramming #Kotlin
- Irrationality criteria for series by Erdős and Straus in Isabelle/HOL. ~ Angeliki Koutsoukou-Argyraki, Wenda Li. #ITP #IsabelleHOL #Math
- A quick look at impredicativity. ~ Simon Peyton Jones. #Haskell #FunctionalProgramming
- Proof-relevant category theory in Agda. ~ Jason Z.S. Hu, Jacques Carette. #ITP #Agda #CategoryTheory
- Janet: a functional and imperative programming language. #FunctionalProgramming #JanetLang
- MathZero, the classification problem, and set-theoretic type theory. ~ David McAllester. #MachineLearning #TypeTheory
- A formalization of Knuth–Bendix orders in Isabelle/HOL. ~ Christian Sternagel, René Thiemann. #ITP #IsabelleHOL
- Formalising Mathematics in a theorem prover. ~ K. Buzzard. #ITP #Math
- Types vs. datatypes vs. typeclasses in Haskell. ~ Jesse Evers (@_jlevers). #Haskell #FunctionalProgramming
- Automatic test generationfor Haskell programming assignments. ~ Vladimír Štill. #Haskell #FunctionalProgramming
- Vídeos de las clases de algorítmica con Haskell. #Haskell #ProgramaciónFuncional #Algorítmica #I1M2019
- Vídeos de las clases de razonamiento automático con Isabelle/HOL. #Lógica #DAO #IsabelleHOL #LMF2019
- Dynamic IFC theorems for free! ~ Maximilian Algehed, Jean-Philippe Bernardy, Cătălin Hrit. #ITP #Agda #FunctionalProgramming
- Machine-checked semantic session typing. ~ Jonas Kastberg Hinrichsen et als. #ITP #Coq
- MathZero, the classification problem, and set-theoretic type theory. ~ David McAllester. #MachineLearning #TypeTheory
- Interesting ATP proofs. #ATP #Logic #Math
- Automating Mathematics? ~ Siddhartha Gadgil. #ITP #Math
- ProvingGround: Automated Theorem proving by learning. ~ Siddhartha Gadgil. #ATP #Math #HoTT
- Purely functional data structures and monoids. ~ Donnacha Oisín Kidney (@oisdk). #Haskell #FunctionalProgramming
- Frozen lake with Q-learning! ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming #MachineLearning
- 2020 Berkeley Lean Seminar. #ITP #LeanProver
- Backtracking generators for random testing. ~ Benjamin Pierce. #ITP #Coq #FunctionalProgramming
- The essence of Bluespec (A core language for rule-based hardware design). Thomas Bourgeat et als. #ITP #Coq
- PubSub implementation in Haskell with formal verification in Coq. ~ Boro Sitnikovski, Biljana Stojcevska, Lidija Goracinova-Ilieva, Irena Stojmenovska. #Haskell #FuncionalProgramming #ITP #Coq
- Why functors and applicatives compose but monads don’t. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming
- Why functors and applicatives compose but monads don’t. [Slides]. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming
- Competitive programming in Haskell: sorting tree shapes. ~ Brent Yorgey. #Haskell #FunctionalProgramming
- Galois theory for non-mathematicians. ~ Mikael Davidsson. #Math
- Stateful protocol composition and typing in Isabelle/HOL. ~ Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker. #ITP #IsabelleHOL
- Visualizing Cantor’s theorem on dense linear orders using Coq. ~ Evan Marzion. #ITP #Coq #Math
- The complex numbers are a ring. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
- How to build with Stack. #Haskell #FunctionalProgramming
- How to script with Stack. #Haskell #FunctionalProgramming
- How to play with Stack. #Haskell #FunctionalProgramming
- Profiling and performance. #Haskell #FunctionalProgramming
- Monad transformers. #Haskell #FunctionalProgramming
- Recommended Haskell libraries. #Haskell #FunctionalProgramming
- String types. #Haskell #FunctionalProgramming
- Synonyms in base. #Haskell #FunctionalProgramming
- Lenses. #Haskell #FunctionalProgramming
- Safe exception handling. #Haskell #FunctionalProgramming
- Data types. #Haskell #FunctionalProgramming
- Data structures. #Haskell #FunctionalProgramming
- Common typeclasses. #Haskell #FunctionalProgramming
- Applied Haskell 101 course. #Haskell #FunctionalProgramming
- Crash course to applicative syntax. #Haskell #FunctionalProgramming
- All about strictness. #Haskell #FunctionalProgramming
- European Lisp Symposium 2020 videos. #Lisp #Programming
- SIXEL Library for Haskell: displaying images on ghci. ~ Junji Hashimoto. #Haskell #FunctionalProgramming
- Error messages in Haskell, and how to improve them. ~ Anthony Super. #Haskell #FunctionalProgramming
- Simple Haskell is best Haskell. ~ Sam Halliday. #Haskell #FunctionalProgramming
- Competitive programming in Haskell: building unordered trees. ~ Brent Yorgey. #Haskell #FunctionalProgramming
- Sets, logic and maths for computing. ~ David Makinson.1#v=onepage&q&f=false #eBook #Logic #Math #CompSci
- A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper. ~ Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger. #FuncionalProgramming #Haskell
- Mathematics in Lean. ~ Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, Patrick Massot. #ITP #LeanProver #Math
- Dynamically flunking the coding interview (A gentle introduction to functional dynamic programming). ~ Maxfield Chen. #Haskell #FunctionalProgramming
- The complex number game. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver
- Accumulating independent errors. ~ Tim Humphries (@thumphriees). #Haskell #FunctionalProgramming
- HandWiki: Online Encyclopedia of Science and Computing.
- How to generate random lambda terms? ~ Maciej Bendkowski. #Haskell #FunctionalProgramming
- Prototyping controlled mathematical languages in Jupyter notebooks. ~ Jan Frederik Schaefer, Kai Amann, Michael Kohlhase. #MKM
- Toward the formal verification of HILECOP: Formalization and implementation of synchronously executed Petri nets. ~ Vincent Iampietro, David Andreu, David Delahaye. #ITP #Coq
- A proof and formalization of the initiality conjecture of dependent type theory. ~ Menno de Boer. #ITP #Coq
- Symbolic reasoning about quantum circuits in Coq. ~ Wenjun Shi, Qinxiang Cao, Yuxin Deng, Hanru Jiang, Yuan Feng. #ITP #Coq
- Simply typed lambda calculus. ~ Splinter Suidman. #Haskell #FuncionalProgramming #LambdaCalculus
- A verified algorithm for computing the Smith normal form of a matrix. ~ Jose Divasón. #ITP #IsabelleHOL #Math
- A survey of languages for formalizing mathematics. ~ Cezary Kaliszyk, Florian Rabe. #Logic #Math #ITP #MKM
- Monoidal puzzle solving. ~ Jonas Carpay (@jonascarpay) #Haskell #FunctionalProgramming
- Capítulo 1 de “Paradojas del nihilismo: La Academia”: Desilusión. #Universidad
- New LaTeX.css library enables websites to look like LaTeX docs. #LaTeX #Math
- Formalising perfectoid spaces. ~ Kevin Buzzard, Johan Commelin, Patrick Massot. #ITP #LeanProver #Math
- Natural numbers with addition form a monoid. ~ James Chapman. #ITP #Agda #Math
- Code-level model checking in the software development workflow. ~ Nathan Chong et als. #FormalVerification #ModelChecking
- How to integrate formal proofs into software development. ~ Daniel Schwartz-Narbonne. #FormalVerification
- Curry-Howard tutorial in literate Haskell. ~ Keith Pinson. #Haskell #FunctionalProgramming #Logic
- On marketing Haskell. ~ Stephen Diehl (@smdiehl) #Haskell #FunctionalProgramming
- A calculator with Reflex and CodeWorld. ~ Chris Smith (@cdsmithus). #Haskell #CodeWorld
- Competitive programming in Haskell: permutations. ~ Brent Yorgey. #Haskell #FunctionalProgramming
- Economic argument for functional programming. ~ Michael Snoyman (@snoyberg). #Haskell #FunctionalProgramming
- Economic argument for functional programming [Slides]. ~ Michael Snoyman (@snoyberg). #Haskell #FunctionalProgramming
- A proof assistant based formalisation of core Erlang. ~ Péter Bereczky, Dániel Horpácsi, Simon Thompson. #ITP #Coq #Erlang
- Verification of closest pair of points algorithms. ~ Martin Rau, Tobias Nipkow. #ITP #IsabelleHOL #Algorithms