Resumen de lecturas compartidas durante agosto de 2019
Esta entrada es una recopilación de lecturas compartidas, durante agosto 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.
- A formal development of a polychronous polytimed coordination language. ~ H. Nguyen Van, F. Boulanger, B. Wolff. #ITP #IsabelleHOL
- A verified LL(1) parser generator. ~ S. Lasser et als. #ITP #Coq
- Verifying effectful Haskell programs in Coq. ~ J. Christiansen, S. Dylus, N. Bunkenburg. #ITP #Coq #Haskell
- Client-side web programming in Haskell: A retrospective ~ Chris Done. #Haskell #FunctionalProgramming
- Practical event driven & sourced programs in Haskell. ~ Adam Piper. #Haskell #FunctionalProgramming
- Haskell: A functional love story. ~ Ilya Peresadin. #Haskell #FunctionalProgramming
- Solving planning problems with Fast Downward and Haskell. ~ Ollie Charles. #Haskell #AI
- Code line patterns: Creating maps of Stackage and PyPi. ~ Simeon Carstens, Matthias Meschede. #Haskell #Python
- Los intereses comerciales marcan el futuro de la inteligencia artificial. ~ Javier Salas. #IA
- IMO 2019 Q1. ~ Kevin Buzzard. #ITP #LeanProver #Math
- Exploring cloud builds in Hadrian. ~ David Eichmann. #Haskell
- Program synthesis in 2019. ~ James Bornholt. #ProgramSynthesis #FormalVerification #ATP
- Considering the order of results when computing Cartesian product. ~ Dominic Orchard. #Haskell #FunctionalProgramming
- Formalising Mathematics-in praxis; A mathematician’s very first experiences with Isabelle/HOL. ~ A. Koutsoukou-Argyraki. #ITP #IsabelleHOL #Math
- Engineering formal systems in constructive type theory. ~ S. Chafar. #PhD_Thesis #ITP #Coq
- Lazy stream programming in Prolog. ~ P- Tarau, J. Wielemaker, T. Schrijvers. #Prolog #LogicProgramming
- Optimized Docker builds for Haskell Stack. ~ Tim Spence. #Haskell #Docker
- Comparing verification of list functions in LiquidHaskell and Idris. ~ A. Westerberg, G. Ung. #Haskell #LiquidHaskell #Idris #FunctionalProgramming
- Dos debates sobre la inteligencia artificial. ~ Javier Sampedro. #IA
- China has started a grand experiment in AI education. It could reshape how the world learns. ~ Noah Sheldon. #AI #Education
- Equations reloaded (high-level dependently-typed functional programming and proving in Coq). ~ M. Sozeau, C. Mangin. #ITP #Coq
- Higher-order type-level programming in Haskell. ~ C. Kiss, T. Field, S. Eisenbach, S. Peyton Jones. #Haskell #FunctionalProgramming
- Functional DevOps in a Dysfunctional World. ~ Vaibhav Sagar. #Haskell #Nix
- Survey of category theory in Coq. #ITP #Coq #Math
- Using the Accelerate library to implement Chebyshev functions. #Haskell #FunctionalProgramming #Math
- Functional Blockchain Contracts. ~ Manuel Chakravarty. #Haskell #Blockchain
- Exercises in programming style: FP & I/O. ~ Nicolas Fränkel. #Programming
- Programming algorithms: Data structures. ~ Vsevolod Dyomkin. #Programming #Lisp #Algorithms
- Why Emacs. ~ Kasim Tuman. #Emacs
- Selected problems from the International Mathematical Olympiad 2019 in Isabelle/HOL. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
- Moving towards ML: Evaluation functions. ~ James Bowen. #Haskell #FunctionalProgramming
- Building a better brain. ~ James Bowen. #Haskell #FunctionalProgramming
- Communicating concurrent Kleene algebra for distributed systems specification. ~ Maxime Buyse. #AFP #ITP #IsabelleHOL #Math
- Verifying finality for Blockchain systems. ~ Karl Palmskog et als. #ITP #Coq #Blockchain
- 10 years seL4: Still the best, still getting better. ~ Gernot Heiser. #ITP #IsabelleHOL
- A Haskell implementation of Conway’s Game of Life, viewable on the console, no external libs. #Haskell #FunctionalProgramming
- Formally justified and modular Bayesian inference for probabilistic programs. ~ Adam Michał Ścibior. #PhD_Thesis #Haskell #FunctionalProgramming
- Una implementación en Haskell de un lenguaje funcional no determinista. ~ Manuel Velasco Suárez. #TFG #Haskell #FunctionalProgramming
- A formally verified HOL algebra for dynamic reliability block diagrams. ~ Y. Elderhalli, O. Hasan, S. Tahar. #ITP #HOL4
- What does it mean for a program analysis to be sound? ~ Ilya Sergey. | SIGPLAN Blog #CompSci #Program_analysis
- How Monoids are useful in programming? ~ @tsoding #Haskell
- Dead-simple TCP/IP services using servant. ~ Justin Le. #Haskell #I1M2016
- Polysemy is fun! – Part 2. ~ Raghu Kaippully. #Haskell #FunctionalProgramming
- The Ramanujan Machine: Automatically generated conjectures on fundamental constants. ~ Gal Raayoni et als. #MachineLearning #Math
- The Ramanujan Machine: Using algorithms to discover new mathematics. #MachineLearning #Math
- Monte Carlo Tree Search in NetLogo. ~ F. Sancho. #NetLogo #IA
- Dependently typed Haskell in industry (experience report). ~ David Thrane Christiansen et als. #Haskell #FunctionalProgramming
- Practical profunctor lenses & optics in PureScript. ~ Thomas Honeyman. #PureScript
- Prolog coding guidelines: Status and tool support. ~ F. Nogatz, P. Körner, S. Krings. #Prolog #LogicProgramming
- Ten simple rules for writing and sharing computational analyses in Jupyter Notebooks. ~ A. Rule et als. #OpenScience #Jupyter
- Building Haskell Apps with Docker. ~ Deni Bertovic . #Haskell #Docker
- Basic text processing in functional style. ~ Vitaly Bragilevsky. #Haskell #FunctionalProgramming
- Intro to Web Prolog for erlangers. ~ T. Lager #Prolog #LogicProgramming
- Building a blog in Haskell with Yesod–Returning JSON. ~ Riccardo Odone #Haskell
- Learn more programming languages, even if you won’t use them. ~ Thorsten Ball #Programming
- Programming algorithms: Arrays. #Programming #CommonLisp
- After Math: (Re)configuring minds, proof, and computing in the postwar United States. ~ Stephanie Aleen Dick. #PhD_Thesis #ATP #Logic #Math
- Pearl: How to do proofs? (Practically proving properties about effectful programs’ results). ~ K. Jacobs, A. Nuyts, D. Devriese. #ITP #Agda #FunctionalProgramming
- Deep Learning: A philosophical introduction. ~ C. Buckner. #DeepLearning
- pretty-simple: pretty-printer for Haskell data types that have a Show instance. ~ Dennis Gosnell. #Haskell #FunctionalProgramming
- An introduction to declarative programming in CLIPS and Prolog. ~ J.L. Watkin, A.C. Volk, S. Perugini. #DeclarativeProgramming #CLIPS #Prolog
- Easy IHaskell Docker images with Nix. ~ Vaibhav Sagar. #Haskell #Docker #Nix
- Partitions of a set. Shayne Fletcher. #Haskell #FunctionalProgramming
- Explaining lambda calculus to a front-end web developer. ~ Henri Tuhola #LambdaCalculus
- Laplace transform in Isabelle/HOL. Fabian Immler. #ITP #IsabelleHOL #Math
- WordNet and Prolog: why not? ~ P. Julian-Iranzo, F. Saenz-Perez. #Prolog #LogicProgramming
- Monads as a programming pattern. ~ Samuel Grayson. #Programming #Monads
- The monad challenges (A set of challenges for jump starting your understanding of monads). ~ Doug Beardsley. #Haskell #Monads
- Coding and reasoning with purity, strong types, and monads. ~ Doug Beardsley (mightybyte). #Haskell #Monads
- Haskell: Build tools. ~ Kowainik. #Haskell #Cabal #Stack
- Haskell kata: withTryFileLock. ~ M. Snoyman. #Haskell #FunctionalProgramming
- How to write a game in Haskell from scratch. ~ Mario Morgenthum. #Haskell #Game
- Transition to Haskell from Python. ~ Chris Martin, Julie Moronuki. #Python #Haskell
- Dynamically-typed Haskell expressions involving applications and variables. ~ Rudy Matela. #Haskell #FunctionalProgramming
- A topological data analysis library for Haskell. ~ Eben Kadile. #Haskell #FunctionalProgramming #Math #Topology
- Pretty-printer for Haskell data types that have a Show instance. ~ Dennis Gosnell. #Haskell #FunctionalProgramming
- Formalisation of an adaptive state counting algorithm in Isabelle/HOL. ~ Robert Sachtleben. #ITP #IsabelleHOL
- Rosette: a solver-aided programming language that extends Racket with language constructs for program synthesis, verification, and more. ~ Emina Torlak. #Programming #Racket #Rosette #DSL #SAT #SMT
- Haskell library containing common graph search algorithms. ~ Devon Hollowood. #Haskell #FunctionalProgramming #Algorithms
- Verified functional programming. ~ N. Voirol. #PhD_Thesis #FunctionalProgramming #Scala
- On monomorphisms and subfields. ~ C. Schwarzweller. #ITP #Mizar #Math
- Undecidability of D_< and its decidable fragments. ~ J. Hu, O. Lhoták. #ITP #Agda
- Comparison between different definitions of Dependent Object Types (DOTs). ~ J. Hu. #ITP #Agda
- Programming languages explained with music. ~ Emma Murray. #Programming
- Una serie de videos que te mostrarán de forma práctica y simple, cómo utilizar Emacs para la producción de documentos académicos. #Emacs
- Abstract completion, formalized. ~ N. Hirokawa et als. #ITP #IsabelleHOL
- Verifying bit-vector invertibility conditions in Coq. ~ B. Ekici et als. #ITP #Coq
- Derivations as computations. ~ Andrej Bauer. #ITP #Andromeda
- Andromeda: A minimalist implementation of type theory, suitable for experimentation. ~ Andrej Bauer #ITP #Andromeda
- The essential tools of Scientific Machine Learning (Scientific ML). ~ Christopher Rackauckas. #MachineLearning #JuliaLang
- La historia del desarrollo de software en dos minutos: un siglo de lógica, lenguajes y código. ~ @Alvy #Programación #Historia
- Learning to prove theorems via interacting with proof assistants. ~ Adrian Colyer. #ITP #MachineLearning
- Typed Lisp, a primer. ~ Musa Al-hassy. #Lisp #Haskell #FunctionalProgramming
- Rib: a Haskell library for writing your own static site generator. ~ Sridhar Ratnakumar. #Haskell #FunctionalProgramming
- From programs to deep models (Part 1). ~ Eran Yahav. #Programming #MachineLearning
- Haskell. History of a community-powered language. ~ Denis Oleynikov, Gints Dreimanis. #Haskell #FunctionalProgramming #History
- Haskell ITMO course at CTD. ~ Dmitry Kovanikov, Arseniy Seroka. #Haskell #FunctionalProgramming
- Haskel’: Discussion about proposed changes to the Haskell programming language. #Haskell #FunctionalProgramming
- Static smart constructors with double splices. ~ Chris Done #Haskell #FunctionalProgramming
- Prolog implementation of the Knuth-Bendix completion procedure. ~ Markus Triska. #Prolog #LogicProgramming
- New draft paper: Survey on bidirectional typechecking. ~ Neel Krishnaswami. #FunctionalProgramming
- Comparison of functional programming languages. ~ Wikipedia. #FunctionalProgramming
- Haskell: let vs. where. #Haskell #FunctionalProgramming
- Point-free or die: Tacit programming in Haskell and beyond. ~ Amar Shah #Haskell #FunctionalProgramming
- Grokking fix. ~ Matt Parsons. #Haskell #FunctionalProgramming
- Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL. ~ R. Bottesch, M.W. Haslbeck, R. Thiemann. #ITP #IsabelleHOL
- A formally verified abstract account of Gödel’s incompleteness theorems. ~ A. Popescu, D. Traytel. #ITP #IsabelleHOL #Logic
- Isabelle/DOF. (User and implementation manual). ~ A.D. Brucker, B. Wolff. #ITP #IsabelleHOL
- Studying algebraic structures using Prover9 and Mace4. ~ R. Arthan, P. Oliva. #ATP #Prover9 #Mace4 #Math
- MUNTA: Fully verified model checker for timed automata. ~ Simon Wimmer. #ITP #IsabelleHOL
- Type-based resource analysis on Haskell. ~ F. Siglmüller. #Haskell #FunctionalProgramming #Algorithms
- Difference between
data
andnewtype
in Haskell. #Haskell #FunctionalProgramming - Type Classes vs. the World. ~ Edward Kmett. #Haskell #FunctionalProgramming
- Verifying bit-vector invertibility conditions in Coq. ~ Burak Ekici et als. #ITP #Coq
- Reconstructing veriT proofs in Isabelle/HOL. ~ M. Fleury, H.J. Schurr. #ITP #IsabelleHOL #SMT #veriT
- Computer mathematics, AI and functional programming. ~ Moa Johansson. #ATP #ITP #Math #Haskell #FunctionalProgramming
- IsaHipster: Theory exploration for Isabelle using HipSpec. ~ Moa Johansson. #ITP #IsabelleHOL #Haskell
- Kei: A small and expressive dependently typed language. ~ Tiago Campos. #Haskell #FunctionalProgramming
- Customizable datatypes. #Haskell #FunctionalProgramming
- A very general method of computing shortest paths. ~ Russell O’Connor. #Haskell #FunctionalProgramming
- Simple reflection of expressions. ~ Twan van Laarhoven. #Haskell #FunctionalProgramming
- simple-reflect: Simple reflection of expressions containing variables. ~ Twan van Laarhoven. #Haskell #FunctionalProgramming
- Monoids and finger trees. ~ Heinrich Apfelmus. #Haskell #FunctionalProgramming
- All about monoids. ~ Edward Kmett. #Haskell #FunctionalProgramming
- Applicative functors. ~ Pat Brisbin. #Haskell #FunctionalProgramming
- Advantages of functional programming for Blockchain protocols. #FunctionalProgramming #Blockchain
- La incidencia filosófica de la programación lógica. ~ Luís Moniz Pereira. #ProgramaciónLógica #Lógica #IA
- Deductive proof of Ethereum smart contracts using Why3. ~ Z. Nehai, F. Bobot. #FormalVerification #Why3
- Q-learning primer. ~ James Bowen. #Haskell #FunctionalProgramming
- Overcoming boolean blindness with evidence. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming
- Teaching Haskell for understanding. ~ Julie Moronuki. #Haskell #FunctionalProgramming
- The monad fear. #Haskell #FunctionalProgramming
- Monads for functional programming. ~ Philip Wadler. #Haskell #FunctionalProgramming
- Three useful monads. #Haskell #FunctionalProgramming
- Monads in Haskell: Reader. ~ Martin Oldfield. #Haskell #FunctionalProgramming
- The State monad: A tutorial for the confused? ~ Brandon Simmons. #Haskell #FunctionalProgramming
- The continuation monad. ~ G. Gonzalez. #Haskell #FunctionalProgramming
- Continuations from the ground up. ~ Isaac Elliott. #Haskell #FunctionalProgramming
- Formalization of sorting algorithms in Isabelle/HOL. ~ Marco Pierre Fernandez Burgos. #BSc_Thesis #ITP #IsabelleHOL
- Formalization of sorting algorithms in Isabelle/HOL (Code). ~ Marco Pierre Fernandez Burgos. #ITP #IsabelleHOL
- Certified equational reasoning via ordered completion. ~ C. Sternagel, S. Winkle. #ITP #IsabelleHOL
- Homotopy type theory: Synthetic homotopy theory and proof verification. ~ M. Blans. #BSc_Thesis #ITP #Agda #HoTT
- Free theorems simply, via dinaturality. ~ J. Voigtländer. #Haskell #FunctionalProgramming
- Functional dependencies & type families. ~ Gabriel Volpe #Haskell #FunctionalProgramming
- Best practices for using functional programming in Python. ~ Tara Smith. #Python #FunctionalProgramming
- Automatic white-box testing with free monads. ~ Alexander Granin #Haskell #FunctionalProgramming
- Abstraction, intuition, and the “monad tutorial fallacy”. ~ Brent Yorgey. #Haskell #FunctionalProgramming
- The trivial monad. ~ Dan Piponi. #Haskell #FunctionalProgramming
- A gentle introduction to monad transformers. #Haskell #FunctionalProgramming
- pLam: An interpreter for learning and exploring pure λ-calculus. ~ Sandro Lovnički. #LambdaCalculus #Haskell #FunctionalProgramming
- What is a monad? #Haskell #FunctionalProgramming
- Programming with effects. ~ Graham Hutton. #Haskell #FunctionalProgramming
- What is a monad? ~ Graham Hutton. https://youtu.be/t1e8gqXLbsU #Haskell #FunctionalProgramming
- Artificial neural networks and simplicial complexes. ~ Eduardo Paluzo. #NeuralNetworks #Math
- Formal verification of the equivalence of system F and the pure type system L2. ~ Jonas Kaiser. #PhD_Thesis #ITP #Coq
- Deferring the details and deriving programs. ~ Liam O’Connor. #ITP #Agda
- Tic tac types: a gentle introduction to dependently typed programming (functional pearl). ~ S. Innes, N. Wu. #FunctionalProgramming #Idris #Haskell
- Haskell pyramid. ~ Nick Sanford. #Haskell #FunctionalProgramming
- PatternSynonyms for expressive code. ~ Raghu Kaippully. #Haskell #FunctionalProgramming
- The Haskell learning curve. #Haskell #FunctionalProgramming
- Fixed points and non-fixed points of Haskell functors. ~ Ziyang Liu. #Haskell #FunctionalProgramming
- Free monoids and free monads, free of category theory. ~ Ziyang Liu. #Haskell #FunctionalProgramming
- Solving the “Beautiful bridges” problem, algebraically. ~ Ziyang Liu. #Haskell #FunctionalProgramming
- That guide that could help you get started with Haskell. ~ Djoe Pramono #Haskell #FunctionalProgramming
- Set theory: An open introduction. ~ Tim Button. #eBook #SetTheory #Logic #Math
- Yet another monad tutorial. ~ Mike Vanier. #Haskell #FunctionalProgramming
- IsarMathLib: a library of formalized mathematics for Isabelle/ZF. ~ Slawomir Kolodynski. #ITP #IsabelleZF #Math
- IsarMathLib: A library of formalized mathematics for Isabelle/ZF theorem proving environment. ~ Slawomir Kolodynski. #ITP #IsabelleZF #Math
- Automated reasoning in first-order real vector spaces. ~ C. Kwan. #MSc_Thesis #ITP #ACL2 #Math
- Functional pearl: Heterogeneous random-access lists. ~ W. Swierstra. #FunctionalProgramming #Agda
- The Haskell pyramid. ~ Lucas Di Cioccio. #Haskell #FunctionalProgramming
- Programming algorithms: Key-values. ~ Vsevolod Dyomkin. #Programming #CommonLisp #Algorithms
- A community-driven Emacs Lisp style guide. ~ Bozhidar Batsov. #Programming #Emacs #Lisp
- A minimal Emacs configuration for Haskell programming. ~ Gil Mizrahi #Emacs #Haskell #FunctionalProgramming
- Funtores, aplicativos y mónadas en imágenes. ~ Miguel Á. Moreno #Haskell #ProgramaciónFuncional
- Understanding SAT by implementing a simple SAT solver in Python. ~ Sahand Saba. #Python #Logic
- Questions and answers about Nix for haskellers. #Hakell #Nix