Resumen de lecturas compartidas durante abril de 2020
Esta entrada es una recopilación de lecturas compartidas, durante abril 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.
- There’s a mathematician in your compiler. ~ James Phillips. #Logic #Math #CompSci #Scala #FunctionalProgramming via @FunctorFact
- Animations in Kaleidogen. ~ Joachim Breitner (@nomeata). #Haskell #FunctionalProgramming
- Curried functions. ~ Graham Hutton (@haskellhutt). #Haskell #FunctionalProgramming
- Migrating from QuickCheck to Hedgehog: mixed results. ~ Fraser Tweedale (@hackuador). #Haskell #FunctionalProgramming
- A distributed and trusted web of formal proofs. ~ Dale Miller. #ITP #Logic #Math #CompSci
- Explosive proofs of mathematical truths. ~ Scott Viteri, Simon DeDeo. #ITP #Coq
- The Hitchhiker’s Guide to Logical Verification. ~ Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl. #eBook #ITP #LeanProver
- Reasoning with conditional probabilities and joint distributions in Coq. ~ Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. #ITP #Coq #Math
- Generalized monoidal effects and handlers. ~ Ruben P. Pieters, Tom Schrijvers, Exequiel Rivas. #Haskell #FunctionalProgramming
- Refactoring a neural network implementation in Haskell. ~ The H2 Wiki. #Haskell #FunctionalProgramming #NeuralNetwork
- ACM Open access to LFP (Conference on LISP and Functional Programming). #Lisp #FunctionalProgramming
- The power of tiny DSLs. ~ Jack Kelly. #Haskell #CodeWorld
- Verified functional programming in Agda. ~ Aaron Stump. #eBook #ITP #Agda
- El problema de Basilea. ~ Urtzi Buijs (@UrtziBuijs). #Matemáticas
- The Bates LaTeX Manual. #LaTeX
- Composition of functions cheatsheet. #Haskell #FunctionalProgramming
- Doing a math assignment with the Lean theorem prover. ~ Andrew Helwer (@ahelwer). #ITP #LeanProver #Math
- Replacing Jupyter with Orgmode. ~ Rohit Goswami (@rg0swami). #Emacs #OrgMode #Python
- Practical proof search for Coq by type inhabitation. ~ Lukasz Czajka. #ITP #Coq
- Haskell: Why monad composes operations sequentially. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming
- Pointless style. ~ Chris Dornan (@CDornan). #Haskell #FunctionalProgramming
- Write unbreakable Python. ~ Jesse Warden (@jesterxl). #Python #FunctionalProgramming
- Functor (expanded). ~ Chris Dornan (@CDornan). #Haskell #FunctionalProgramming
- Introducing the #ProjectEuler100 challenge: the “dark souls” of coding achievements. ~ Quincy Larson (@ossia). #Programming #Math
- Maintaining a library of formal mathematics. ~ Floris van Doorn, Gabriel Ebner, Robert Y. Lewis. #ITP #LeanProver #Math
- Coursework: The power and limits of Logic. ~ Greg Restall (@consequently). #Logic
- Key benefits of working in Haskell. ~ Sreenidhi Nair (@ersran9). #Haskell #FunctionalProgramming
- A fast verified liveness analysis in SSA form. ~ Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie. #ITP #Coq
- Certifying certainty and uncertainty in approximate membership query structures. ~ Kiran Gopinathan, Ilya Sergey. #ITP #Coq
- The interplay between logic and computation. ~ Zena M. Ariola. #Logic #CompSci
- Understanding the power of LISP. ~ @josh_b_rad. #Lisp
- A comprehensive framework for saturation theorem proving. ~ Sophie Tourret. #ITP #IsabelleHOL #Logic
- Esencia del álgebra lineal. #Matemáticas
- Fundamentals of Artificial Intelligence. ~ K.R. Chowdhary. #AI #Logic
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL. ~ Sadegh Dalvandi, Brijesh Dongol, Simon Doherty. #ITP #IsabelleHOL
- Verifying the DPLL algorithm in Dafny. ~ Cezar-Constantin Andrici, Ştefan Ciobâcă. #Dafny #Verification
- Herramientas de razonamiento automático en GeoGebra: qué son y para qué sirven. ~ M. Pilar Vélez, Tomás Recio, Steven Van Vaerenbergh. #Razonamiento_automático #GeoGebra
- Functional Pearls: Heterogeneous binary random-access lists. ~ Wouter Swierstra. #Agda #FunctionalProgramming
- On beyond Prolog. ~ Anne Ogborn (@AnnieTheObscure). #Prolog #LogicProgramming
- Zipping trees. Part 1. ~ Joseph Morag. #Haskell #FunctionalProgramming
- Zipping trees. Part 2. ~ Joseph Morag. #Haskell #FunctionalProgramming
- Formalization of an algorithm for greedily computing associative aggregations on sliding windows. ~ Lukas Heimes, Dmitriy Traytel, Joshua Schneider. #ITP #IsabelleHOL
- Things software engineers trip up on when learning Haskell. ~ William Yao (@williamyaoh). #Haskell #FuncionalProgramming
- 10 minute Lean tutorial: proving logical propositions. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Logic
- Doglike programming book (Chicken jerky flavoured introduction to functional programming). ~ Juuso Vuorinen. #eBook #Haskell #FunctionalProgramming
- At the interface of algebra and statistics. ~ Tai-Danae Bradley. #PhD_Thesis #Math
- Haskell Wizards (Character illustrations of Haskell users). #Haskell #FunctionalProgramming
- Computable analysis and notions of continuity in Coq. ~ Florian Steinberg, Laurent Thery, Holger Thies. #ITP #Coq #Math
- Programming totally with head and tail. ~ Li-yao Xia (@lysxia). #Haskell #FunctionalProgramming
- Prolog technology reinforcement learning prover. ~ Zsolt Zombori, Josef Urban, Chad E. Brown. #ATP #MachineLearning #Prolog
- Programming algorithms. ~ Vsevolod Domkin #eBook #CommonLisp #Programming #Algorithms
- Online seminar lists. #Math #CompSci
- Towards faster iteration in industrial Haskell. ~ Patrick Thomson (@importantshock). #Haskell #FunctionalProgramming
- Trakhtenbrot’s theorem in Coq, a constructive approach to finite model theory. ~ Dominik Kirst, Dominique Larchey-Wendling. #ITP #Coq #Math
- The three kinds of Haskell exceptions and how to use them. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming
- Why Haskell matters. ~ Thomas Mahler. #Haskell #FunctionalProgramming
- Distilling the requirements of Gödel’s Incompleteness theorems with a proof assistant. ~ Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL #Logic #Math
- Towards a formal proof of the Cook-Levin theorem. ~ Lennard Gäher. #ITP #Coq #Logic #Math
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL. ~ René Thiemann et als. #ITP #IsabelleHOL
- What Is Haskell, who uses it, and where can you learn to code it. ~ Alexander Sechin. #Haskell #FunctionalProgramming
- The mechanization of Mathematics. ~ Jeremy Avigad. #ITP #Math
- The mechanization of Mathematics. ~ Jeremy Avigad. #ITP #Math
- Great moments in Haskell history. ~ Chris Martin (@chris__martin), Julie Moronuki (@argumatronic). #Haskell #FunctionalProgramming
- Algebraically closed fields in Isabelle/HOL. ~ Paulo Emı́lio de Vilhena, Lawrence C. Paulson. #ITP #IsabelleHOL #Math
- Introduction to relude an alternative Haskell prelude. ~ Dmitrii Kovanikov (@ChShersh). #Haskell #FunctionalProgramming
- Lucas’s theorem in Isabelle/HOL. ~ Chelsea Edmonds. #ITP #IsabelleHOL #Math
- Blazing fast Fibonacci numbers using Monoids. ~ G. Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming #Math
- Deep generation of Coq lemma names using elaborated terms. ~ Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric. #ITP #Coq #MachineLearning
- Formal verification of flow equivalence in desynchronized designs. ~ Jennifer Paykin, Brian Huffman, Daniel M. Zimmerman, Peter A. Beerel. #ITP #Coq
- The Imandra automated reasoning system (system description). ~ Grant Olneya Passmore et als. #ITP
- Deriving isomorphically. ~ Hans Hoeglund. #Haskell #FunctionalProgramming
- When will computers prove theorems? ~ Kevin Buzzard. #ITP #Math
- Recursive functions. ~ Walter Dean. #Logic #Math
- Is HoTT the way to do mathematics? ~ Kevin Buzzard. #Math #HoTT #ITP
- El método Moore o cómo aprender matemáticas al estilo tejano. ~ Pedro Alegría. #Matemáticas
- Active Prelude to Calculus. ~ Matthew Boelkins. #Math
- Active Calculus 2.1. ~ Matthew Boelkins. #Math
- Active Calculus Multivariable: 2018 Edition. ~ Steve Schlicker, David Austin, Matt Boelkins. #Math
- Detecting fake news for the new coronavirus by reasoning on the Covid-19 ontology. ~ Adrian Groza. #ATP #Racer
- Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems. ~ Florian Kammüller. #ITP #IsabelleHOL
- Diagnosis in tennis serving technique. ~ Eugenio Roanes-Lozano et als. #KBS #CAS #GroebnerBases #Logic #Math #CompSci
- Scala book (Learn Scala fastwith small, easy lessons). ~ Alvin Alexander, et al. #eBook #Scala #FunctionalProgramming
- A simplified version of Bitcoin, implemented in Agda. ~ Guilherme Horta Alvares da Silva. #ITP #Agda #FunctionalProgramming
- Consider Haskell. ~ Gil Mizrahi (@_gilmi). #Haskell #FunctionalProgramming
- The Lambert W function on the reals. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
- Introduction to Artificial Intelligence. ~ Wolfgang Ertel. #eBook #Logic #AI
- Open Textbook Library: Open textbooks are textbooks that have been funded, published, and licensed to be freely used, adapted, and distributed. #eBooks
- Mathematical logic (On numbers, sets, structures, and symmetry). ~ Romana Kossak. #eBook #Logic #Math
- Philosophical and mathematical logic. ~ Harrie de Swart. #eBook #Logic #Math
- Foundations of programming languages. ~ Kent D. Lee. #eBook #Programming #CompSci
- The invisible map. ~ Kevin Buzzard (@XenaProject). #Logic #Math #ITP #LeanProver
- Proofs from THE BOOK. ~ Martin Aigner, Günter M. Ziegler #FreeEbook #Math