{"id":6740,"date":"2019-09-01T11:40:43","date_gmt":"2019-09-01T09:40:43","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6740"},"modified":"2019-09-01T11:40:43","modified_gmt":"2019-09-01T09:40:43","slug":"resumen-de-lecturas-compartidas-durante-agosto-de-2019","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-agosto-de-2019\/","title":{"rendered":"Resumen de lecturas compartidas durante agosto de 2019"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante agosto de 2019, en <a href=\"https:\/\/twitter.com\/Jose_A_Alonso\">Twitter<\/a> fundamentalmente sobre programaci\u00f3n funcional y demostraci\u00f3n asistida por ordenador.<\/p>\n<p>Las lecturas est\u00e1n ordenadas seg\u00fan su fecha de publicaci\u00f3n en <a href=\"https:\/\/twitter.com\/Jose_A_Alonso\">Twitter<\/a>.<\/p>\n<p>Al final de cada art\u00edculo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.<\/p>\n<p>Una recopilaci\u00f3n de todas las lecturas compartidas se encuentra en <a href=\"https:\/\/github.com\/jaalonso\/Lecturas_GLC\">GitHub<\/a>.<br \/>\n<!--more--><\/p>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/TESL_Language.html\">A formal development of a polychronous polytimed coordination language<\/a>. ~ H. Nguyen Van, F. Boulanger, B. Wolff. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/www.tyconmismatch.com\/papers\/itp2019_ll1.pdf\">A verified LL(1) parser generator<\/a>. ~ S. Lasser et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www-ps.informatik.uni-kiel.de\/~sad\/haskell2019-preprint.pdf\">Verifying effectful Haskell programs in Coq<\/a>. ~ J. Christiansen, S. Dylus, N. Bunkenburg. #ITP #Coq #Haskell<\/li>\n<li><a href=\"https:\/\/chrisdone.com\/posts\/clientside-programming-haskell\/\">Client-side web programming in Haskell: A retrospective<\/a> ~ Chris Done. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.ahri.net\/2019\/07\/practical-event-driven-and-sourced-programs-in-haskell\/\">Practical event driven &amp; sourced programs in Haskell<\/a>. ~ Adam Piper. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/haskell-love-story\">Haskell: A functional love story<\/a>. ~ Ilya Peresadin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/ocharles.org.uk\/blog\/posts\/2018-12-25-fast-downward.html\">Solving planning problems with Fast Downward and Haskell<\/a>. ~ Ollie Charles. #Haskell #AI<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2019-08-01-codestatistics-umap.html\">Code line patterns: Creating maps of Stackage and PyPi<\/a>. ~ Simeon Carstens, Matthias Meschede. #Haskell #Python<\/li>\n<li><a href=\"https:\/\/elpais.com\/elpais\/2019\/07\/29\/ciencia\/1564394653_192603.html\">Los intereses comerciales marcan el futuro de la inteligencia artificial<\/a>. ~ Javier Salas. #IA<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2019\/08\/01\/imo-2019-q1\/\">IMO 2019 Q1<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/well-typed.com\/blog\/2019\/08\/exploring-cloud-builds-in-hadrian\/\">Exploring cloud builds in Hadrian<\/a>. ~ David Eichmann. #Haskell<\/li>\n<li><a href=\"https:\/\/blog.sigplan.org\/2019\/07\/31\/program-synthesis-in-2019\/\">Program synthesis in 2019<\/a>. ~ James Bornholt. #ProgramSynthesis #FormalVerification #ATP<\/li>\n<li><a href=\"https:\/\/dorchard.blog\/2019\/08\/02\/considering-the-order-of-results-when-computing-cartesian-product-short\/\">Considering the order of results when computing Cartesian product<\/a>. ~ Dominic Orchard. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/Angeliki_Koutsoukou-Argyraki\/publication\/334549483_FORMALISING_MATHEMATICS_-IN_PRAXIS_A_MATHEMATICIAN'S_VERY_FIRST_EXPERIENCES_WITH_ISABELLEHOL\/links\/5d30f782299bf1547cc25f63\/FORMALISING-MATHEMATICS-IN-PRAXIS-A-MATHEMATICIANS-VERY-FIRST-EXPERIENCES-WITH-ISABELLE-HOL.pdf\">Formalising Mathematics-in praxis; A mathematician&#8217;s very first experiences with Isabelle\/HOL<\/a>. ~ A. Koutsoukou-Argyraki. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/Publications\/documents\/Schaefer_2019_Engineering.pdf\">Engineering formal systems in constructive type theory<\/a>. ~ S. Chafar. #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.11354\">Lazy stream programming in Prolog<\/a>. ~ P- Tarau, J. Wielemaker, T. Schrijvers. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/permutive\/optimized-docker-builds-for-haskell-76a9808eb10b\">Optimized Docker builds for Haskell Stack<\/a>. ~ Tim Spence. #Haskell #Docker<\/li>\n<li><a href=\"https:\/\/kth.diva-portal.org\/smash\/get\/diva2:1338661\/FULLTEXT01.pdf\">Comparing verification of list functions in LiquidHaskell and Idris<\/a>. ~ A. Westerberg, G. Ung. #Haskell #LiquidHaskell #Idris #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/elpais.com\/elpais\/2019\/08\/01\/ciencia\/1564654546_001863.html\">Dos debates sobre la inteligencia artificial<\/a>. ~ Javier Sampedro. #IA<\/li>\n<li><a href=\"https:\/\/www.technologyreview.com\/s\/614057\/china-squirrel-has-started-a-grand-experiment-in-ai-education-it-could-reshape-how-the\/\">China has started a grand experiment in AI education. It could reshape how the world learns<\/a>. ~ Noah Sheldon. #AI #Education<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3341690\">Equations reloaded (high-level dependently-typed functional programming and proving in Coq)<\/a>. ~ M. Sozeau, C. Mangin. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3341706\">Higher-order type-level programming in Haskell<\/a>. ~ C. Kiss, T. Field, S. Eisenbach, S. Peyton Jones. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/vaibhavsagar.com\/blog\/2019\/07\/04\/functional-devops\/index.html\">Functional DevOps in a Dysfunctional World<\/a>. ~ Vaibhav Sagar. #Haskell #Nix<\/li>\n<li><a href=\"https:\/\/coq.discourse.group\/t\/survey-of-category-theory-in-coq\/371\">Survey of category theory in Coq<\/a>. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.cs.mcgill.ca\/~dto4\/projects\/gsoc-02-acc.html\">Using the Accelerate library to implement Chebyshev functions<\/a>. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/justtesting.org\/post\/186788963306\/functional-blockchain-contracts\">Functional Blockchain Contracts<\/a>. ~ Manuel Chakravarty. #Haskell #Blockchain<\/li>\n<li><a href=\"https:\/\/blog.frankel.ch\/exercises-programming-style\/13\/\">Exercises in programming style: FP &amp; I\/O<\/a>. ~ Nicolas Fr\u00e4nkel. #Programming<\/li>\n<li><a href=\"http:\/\/lisp-univ-etc.blogspot.com\/2019\/08\/programming-algorithms-data-structures.html\">Programming algorithms: Data structures<\/a>. ~ Vsevolod Dyomkin. #Programming #Lisp #Algorithms<\/li>\n<li><a href=\"https:\/\/www.birkey.co\/2019-08-04-why-emacs.html\">Why Emacs<\/a>. ~ Kasim Tuman. #Emacs<\/li>\n<li><a href=\"http:\/\/bit.ly\/31pCRLl\">Selected problems from the International Mathematical Olympiad 2019 in Isabelle\/HOL<\/a>. ~ Manuel Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/bit.ly\/31mOfaZ\">Moving towards ML: Evaluation functions<\/a>. ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/bit.ly\/2Kh2sk0\">Building a better brain<\/a>. ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/bit.ly\/2M4YFIB\">Communicating concurrent Kleene algebra for distributed systems specification<\/a>. ~ Maxime Buyse. #AFP #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/bit.ly\/2Kz8kE8\">Verifying finality for Blockchain systems<\/a>. ~ Karl Palmskog et als. #ITP #Coq #Blockchain<\/li>\n<li><a href=\"http:\/\/bit.ly\/2KtZNCx\">10 years seL4: Still the best, still getting better<\/a>. ~ Gernot Heiser. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/bit.ly\/2M78khY\">A Haskell implementation of Conway&#8217;s Game of Life, viewable on the console, no external libs<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/bit.ly\/2KtVcQN\">Formally justified and modular Bayesian inference for probabilistic programs<\/a>. ~ Adam Micha\u0142 \u015acibior. #PhD_Thesis #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/bit.ly\/2M4ZG3k\">Una implementaci\u00f3n en Haskell de un lenguaje funcional no determinista<\/a>. ~ Manuel Velasco Su\u00e1rez. #TFG #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/bit.ly\/2KzaxPW\">A formally verified HOL algebra for dynamic reliability block diagrams<\/a>. ~ Y. Elderhalli, O. Hasan, S. Tahar. #ITP #HOL4<\/li>\n<li><a href=\"http:\/\/bit.ly\/33c9Ft4\">What does it mean for a program analysis to be sound?<\/a> ~ Ilya Sergey. | SIGPLAN Blog #CompSci #Program_analysis<\/li>\n<li><a href=\"http:\/\/bit.ly\/2ThrpyL\">How Monoids are useful in programming?<\/a> ~ @tsoding #Haskell<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/simple-tcpip-services-servant.html\">Dead-simple TCP\/IP services using servant<\/a>. ~ Justin Le. #Haskell #I1M2016<\/li>\n<li><a href=\"https:\/\/haskell-explained.gitlab.io\/blog\/posts\/2019\/07\/31\/polysemy-is-cool-part-2\/index.html\">Polysemy is fun! &#8211; Part 2<\/a>. ~ Raghu Kaippully. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/bit.ly\/2TdPPsS\">The Ramanujan Machine: Automatically generated conjectures on fundamental constants<\/a>. ~ Gal Raayoni et als. #MachineLearning #Math<\/li>\n<li><a href=\"http:\/\/www.ramanujanmachine.com\">The Ramanujan Machine: Using algorithms to discover new mathematics<\/a>. #MachineLearning #Math<\/li>\n<li><a href=\"http:\/\/bit.ly\/2Tekia7\">Monte Carlo Tree Search in NetLogo<\/a>. ~ F. Sancho. #NetLogo #IA<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3341704\">Dependently typed Haskell in industry (experience report)<\/a>. ~ David Thrane Christiansen et als. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/thomashoneyman.com\/articles\/practical-profunctor-lenses-optics\/\">Practical profunctor lenses &amp; optics in PureScript<\/a>. ~ Thomas Honeyman. #PureScript<\/li>\n<li><a href=\"http:\/\/krin.gs\/publication\/nogatz-linter-iclp19\/nogatz-linter-iclp19.pdf\">Prolog coding guidelines: Status and tool support<\/a>. ~ F. Nogatz, P. K\u00f6rner, S. Krings. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/journals.plos.org\/ploscompbiol\/article?id=10.1371\/journal.pcbi.1007007\">Ten simple rules for writing and sharing computational analyses in Jupyter Notebooks<\/a>. ~ A. Rule et als. #OpenScience #Jupyter<\/li>\n<li><a href=\"https:\/\/www.fpcomplete.com\/blog\/2017\/12\/building-haskell-apps-with-docker\">Building Haskell Apps with Docker<\/a>. ~ Deni Bertovic . #Haskell #Docker<\/li>\n<li><a href=\"https:\/\/freecontent.manning.com\/basic-text-processing-in-functional-style\/\">Basic text processing in functional style<\/a>. ~ Vitaly Bragilevsky. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/bit.ly\/2OPRNkR\">Intro to Web Prolog for erlangers<\/a>. ~ T. Lager #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/odone.io\/posts\/2019-08-12-building-a-blog-in-haskell-with-yesod%E2%80%93returning-JSON.html\">Building a blog in Haskell with Yesod\u2013Returning JSON<\/a>. ~ Riccardo Odone #Haskell<\/li>\n<li><a href=\"https:\/\/thorstenball.com\/blog\/2019\/04\/09\/learn-more-programming-languages\/\">Learn more programming languages, even if you won&#8217;t use them<\/a>. ~ Thorsten Ball #Programming<\/li>\n<li><a href=\"http:\/\/lisp-univ-etc.blogspot.com\/2019\/08\/programming-algorithms-arrays.html%20~%20Vsevolod%20Dyomkin.\">Programming algorithms: Arrays<\/a>. #Programming #CommonLisp<\/li>\n<li><a href=\"https:\/\/dash.harvard.edu\/bitstream\/handle\/1\/14226096\/DICK-DISSERTATION-2015.pdf?sequence=6&amp;isAllowed=y\">After Math: (Re)configuring minds, proof, and computing in the postwar United States<\/a>. ~ Stephanie Aleen Dick. #PhD_Thesis #ATP #Logic #Math<\/li>\n<li><a href=\"https:\/\/cris.vub.be\/files\/46086440\/pearl.pdf\">Pearl: How to do proofs? (Practically proving properties about effectful programs\u2019 results)<\/a>. ~ K. Jacobs, A. Nuyts, D. Devriese. #ITP #Agda #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/philsci-archive.pitt.edu\/16326\/\">Deep Learning: A philosophical introduction<\/a>. ~ C. Buckner. #DeepLearning<\/li>\n<li><a href=\"https:\/\/github.com\/cdepillabout\/pretty-simple%20\">pretty-simple: pretty-printer for Haskell data types that have a Show instance<\/a>. ~ Dennis Gosnell. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/academic.udayton.edu\/SaverioPerugini\/papers\/access\/CSC2019\/CSC2019Perugini.pdf\">An introduction to declarative programming in CLIPS and Prolog<\/a>. ~ J.L. Watkin, A.C. Volk, S. Perugini. #DeclarativeProgramming #CLIPS #Prolog<\/li>\n<li><a href=\"https:\/\/vaibhavsagar.com\/blog\/2019\/08\/11\/ihaskell-nix-docker\/\">Easy IHaskell Docker images with Nix<\/a>. ~ Vaibhav Sagar. #Haskell #Docker #Nix<\/li>\n<li><a href=\"https:\/\/blog.shaynefletcher.org\/2019\/08\/partitions-of-set.html\">Partitions of a set<\/a>. Shayne Fletcher. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/boxbase.org\/entries\/2019\/aug\/12\/explaining-lambda-calculus-to-developer\/\">Explaining lambda calculus to a front-end web developer<\/a>. ~ Henri Tuhola #LambdaCalculus<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Laplace_Transform.html\">Laplace transform in Isabelle\/HOL<\/a>. Fabian Immler. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/download.atlantis-press.com\/article\/125914883.pdf\">WordNet and Prolog: why not?<\/a> ~ P. Julian-Iranzo, F. Saenz-Perez. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/samgrayson.me\/2019-08-06-monads-as-a-programming-pattern\/\">Monads as a programming pattern<\/a>. ~ Samuel Grayson. #Programming #Monads<\/li>\n<li><a href=\"http:\/\/mightybyte.github.io\/monad-challenges\">The monad challenges (A set of challenges for jump starting your understanding of monads)<\/a>. ~ Doug Beardsley. #Haskell #Monads<\/li>\n<li><a href=\"http:\/\/mightybyte.net\/purity-types-monads\/purity-types-monads.html\">Coding and reasoning with purity, strong types, and monads<\/a>. ~ Doug Beardsley (mightybyte). #Haskell #Monads<\/li>\n<li><a href=\"https:\/\/kowainik.github.io\/posts\/2018-06-21-haskell-build-tools\">Haskell: Build tools<\/a>. ~ Kowainik. #Haskell #Cabal #Stack<\/li>\n<li><a href=\"https:\/\/www.snoyman.com\/blog\/2019\/08\/haskell-kata-with-try-file-lock\">Haskell kata: withTryFileLock<\/a>. ~ M. Snoyman. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.morgenthum.tech\/articles\/write-haskell-game\">How to write a game in Haskell from scratch<\/a>. ~ Mario Morgenthum. #Haskell #Game<\/li>\n<li><a href=\"https:\/\/typeclasses.com\/python\">Transition to Haskell from Python<\/a>. ~ Chris Martin, Julie Moronuki. #Python #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/rudymatela\/express\">Dynamically-typed Haskell expressions involving applications and variables<\/a>. ~ Rudy Matela. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/Ebanflo42\/Persistence\">A topological data analysis library for Haskell<\/a>. ~ Eben Kadile. #Haskell #FunctionalProgramming #Math #Topology<\/li>\n<li><a href=\"https:\/\/github.com\/cdepillabout\/pretty-simple\">Pretty-printer for Haskell data types that have a Show instance<\/a>. ~ Dennis Gosnell. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Adaptive_State_Counting.html\">Formalisation of an adaptive state counting algorithm in Isabelle\/HOL<\/a>. ~ Robert Sachtleben. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/github.com\/emina\/rosette\">Rosette: a solver-aided programming language that extends Racket with language constructs for program synthesis, verification, and more<\/a>. ~ Emina Torlak. #Programming #Racket #Rosette #DSL #SAT #SMT<\/li>\n<li><a href=\"https:\/\/github.com\/devonhollowood\/search-algorithms\">Haskell library containing common graph search algorithms<\/a>. ~ Devon Hollowood. #Haskell #FunctionalProgramming #Algorithms<\/li>\n<li><a href=\"https:\/\/infoscience.epfl.ch\/record\/268824\">Verified functional programming<\/a>. ~ N. Voirol. #PhD_Thesis #FunctionalProgramming #Scala<\/li>\n<li><a href=\"https:\/\/content.sciendo.com\/view\/journals\/forma\/27\/2\/article-p133.xml\">On monomorphisms and subfields<\/a>. ~ C. Schwarzweller. #ITP #Mizar #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1908.05294\">Undecidability of D_&lt; and its decidable fragments<\/a>. ~ J. Hu, O. Lhot\u00e1k. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/hustmphrrr.github.io\/blog\/2019\/compare-dots.html\">Comparison between different definitions of Dependent Object Types (DOTs)<\/a>. ~ J. Hu. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/blog.toggl.com\/programming-languages-explained-with-music-comic\/\">Programming languages explained with music<\/a>. ~ Emma Murray. #Programming<\/li>\n<li><a href=\"https:\/\/github.com\/farliz\/emacs-academia\">Una serie de videos que te mostrar\u00e1n de forma pr\u00e1ctica y simple, c\u00f3mo utilizar Emacs para la producci\u00f3n de documentos acad\u00e9micos<\/a>. #Emacs<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1802.08437\">Abstract completion, formalized<\/a>. ~ N. Hirokawa et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/pxtp.gforge.inria.fr\/2019\/papers\/PxTP_2019_paper_5.pdf\">Verifying bit-vector invertibility conditions in Coq<\/a>. ~ B. Ekici et als. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/math.andrej.com\/2019\/08\/21\/derivations-as-computations\/\">Derivations as computations<\/a>. ~ Andrej Bauer. #ITP #Andromeda<\/li>\n<li><a href=\"https:\/\/github.com\/Andromedans\/andromeda\">Andromeda: A minimalist implementation of type theory, suitable for experimentation<\/a>. ~ Andrej Bauer #ITP #Andromeda<\/li>\n<li><a href=\"http:\/\/www.stochasticlifestyle.com\/the-essential-tools-of-scientific-machine-learning-scientific-ml\/\">The essential tools of Scientific Machine Learning (Scientific ML)<\/a>. ~ Christopher Rackauckas. #MachineLearning #JuliaLang<\/li>\n<li><a href=\"https:\/\/www.microsiervos.com\/archivo\/ordenadores\/historia-desarrollo-software-logica-lenguajes-codigo.html\">La historia del desarrollo de software en dos minutos: un siglo de l\u00f3gica, lenguajes y c\u00f3digo<\/a>. ~ @Alvy #Programaci\u00f3n #Historia<\/li>\n<li><a href=\"https:\/\/blog.acolyer.org\/2019\/08\/23\/learning-to-prove-theorems-via-interacting-with-proof-assistants\/\">Learning to prove theorems via interacting with proof assistants<\/a>. ~ Adrian Colyer. #ITP #MachineLearning<\/li>\n<li><a href=\"https:\/\/alhassy.github.io\/TypedLisp\/\">Typed Lisp, a primer<\/a>. ~ Musa Al-hassy. #Lisp #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/srid\/rib\">Rib: a Haskell library for writing your own static site generator<\/a>. ~ Sridhar Ratnakumar. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.sigplan.org\/2019\/08\/22\/from-programs-to-deep-models-part-1\/\">From programs to deep models (Part 1)<\/a>. ~ Eran Yahav. #Programming #MachineLearning<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/haskell-history\">Haskell. History of a community-powered language<\/a>. ~ Denis Oleynikov, Gints Dreimanis. #Haskell #FunctionalProgramming #History<\/li>\n<li><a href=\"https:\/\/github.com\/jagajaga\/FP-Course-ITMO\">Haskell ITMO course at CTD<\/a>. ~ Dmitry Kovanikov, Arseniy Seroka. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/haskell\/rfcs\">Haskel&#8217;: Discussion about proposed changes to the Haskell programming language<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/chrisdone.com\/posts\/static-smart-constructors\/\">Static smart constructors with double splices<\/a>. ~ Chris Done #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.metalevel.at\/trs\/\">Prolog implementation of the Knuth-Bendix completion procedure<\/a>. ~ Markus Triska. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/semantic-domain.blogspot.com\/2019\/08\/new-draft-paper-survey-on-bidirectional.html\">New draft paper: Survey on bidirectional typechecking<\/a>. ~ Neel Krishnaswami. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/en.wikipedia.org\/wiki\/Comparison_of_functional_programming_languages\">Comparison of functional programming languages<\/a>. ~ Wikipedia. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/wiki.haskell.org\/Let_vs._Where\">Haskell: let vs<\/a>. where. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/seVSlKazsNk\">Point-free or die: Tacit programming in Haskell and beyond<\/a>. ~ Amar Shah #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.parsonsmatt.org\/2016\/10\/26\/grokking_fix.html\">Grokking fix<\/a>. ~ Matt Parsons. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/335335097_Verifying_an_Incremental_Theory_Solver_for_Linear_Arithmetic_in_IsabelleHOL\">Verifying an incremental theory solver for linear arithmetic in Isabelle\/HOL<\/a>. ~ R. Bottesch, M.W. Haslbeck, R. Thiemann. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/andreipopescu.uk\/pdf\/Goedel_CADE_2019.pdf\">A formally verified abstract account of G\u00f6del\u2019s incompleteness theorems<\/a>. ~ A. Popescu, D. Traytel. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/ore.exeter.ac.uk\/repository\/handle\/10871\/38402\">Isabelle\/DOF. (User and implementation manual)<\/a>. ~ A.D. Brucker, B. Wolff. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1908.06479\">Studying algebraic structures using Prover9 and Mace4<\/a>. ~ R. Arthan, P. Oliva. #ATP #Prover9 #Mace4 #Math<\/li>\n<li><a href=\"https:\/\/github.com\/wimmers\/munta\">MUNTA: Fully verified model checker for timed automata<\/a>. ~ Simon Wimmer. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1908.06478\">Type-based resource analysis on Haskell<\/a>. ~ F. Siglm\u00fcller. #Haskell #FunctionalProgramming #Algorithms<\/li>\n<li><a href=\"https:\/\/stackoverflow.com\/questions\/5889696\/difference-between-data-and-newtype-in-haskell\">Difference between `data` and `newtype` in Haskell<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/hIZxTQP1ifo\">Type Classes vs. the World<\/a>. ~ Edward Kmett. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?PxTP2019.4\">Verifying bit-vector invertibility conditions in Coq<\/a>. ~ Burak Ekici et als. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?PxTP2019.6\">Reconstructing veriT proofs in Isabelle\/HOL<\/a>. ~ M. Fleury, H.J. Schurr. #ITP #IsabelleHOL #SMT #veriT<\/li>\n<li><a href=\"https:\/\/www.infoq.com\/presentations\/ai-ml-functional-programming\/?utm_source=twitter.com&amp;utm_medium=social&amp;utm_campaign=presentation-computer-mathematics--ai-a\">Computer mathematics, AI and functional programming<\/a>. ~ Moa Johansson. #ATP #ITP #Math #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/moajohansson\/IsaHipster\">IsaHipster: Theory exploration for Isabelle using HipSpec<\/a>. ~ Moa Johansson. #ITP #IsabelleHOL #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/caotic123\/Kei\">Kei: A small and expressive dependently typed language<\/a>. ~ Tiago Campos. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mpardalos.xyz\/posts\/customizable_datatypes.html\">Customizable datatypes<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/r6.ca\/blog\/20110808T035622Z.html\">A very general method of computing shortest paths<\/a>. ~ Russell O\u2019Connor. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/twanvl.nl\/blog\/haskell\/simple-reflection-of-expressions\">Simple reflection of expressions<\/a>. ~ Twan van Laarhoven. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/hackage.haskell.org\/package\/simple-reflect-0.3.3\">simple-reflect: Simple reflection of expressions containing variables<\/a>. ~ Twan van Laarhoven. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/apfelmus.nfshost.com\/articles\/monoid-fingertree.html\">Monoids and finger trees<\/a>. ~ Heinrich Apfelmus. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/comonad.com\/reader\/wp-content\/uploads\/2009\/07\/AllAboutMonoids.pdf\">All about monoids<\/a>. ~ Edward Kmett. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/pbrisbin.com\/posts\/applicative_functors\/\">Applicative functors<\/a>. ~ Pat Brisbin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/hackernoon.com\/advantages-of-functional-programming-for-blockchain-protocols-1ca2d4ac1033\">Advantages of functional programming for Blockchain protocols<\/a>. #FunctionalProgramming #Blockchain<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/241132399_La_incidencia_filosofica_de_la_programacion_logica\">La incidencia filos\u00f3fica de la programaci\u00f3n l\u00f3gica<\/a>. ~ Lu\u00eds Moniz Pereira. #Programaci\u00f3nL\u00f3gica #L\u00f3gica #IA<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1904.11281\">Deductive proof of Ethereum smart contracts using Why3<\/a>. ~ Z. Nehai, F. Bobot. #FormalVerification #Why3<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/8\/19\/q-learning-primer\">Q-learning primer<\/a>. ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cs-syd.eu\/posts\/2016-07-24-overcoming-boolean-blindness-evidence\">Overcoming boolean blindness with evidence<\/a>. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/iuwUUlDfHcw\">Teaching Haskell for understanding<\/a>. ~ Julie Moronuki. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/xtendo.org\/monad\">The monad fear<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/marktoberdorf\/baastad.pdf\">Monads for functional programming<\/a>. ~ Philip Wadler. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/adit.io\/posts\/2013-06-10-three-useful-monads.html\">Three useful monads<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.mjoldfield.com\/atelier\/2014\/08\/monads-reader.html\">Monads in Haskell: Reader<\/a>. ~ Martin Oldfield. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/brandon.si\/code\/the-state-monad-a-tutorial-for-the-confused\/\">The State monad: A tutorial for the confused?<\/a> ~ Brandon Simmons. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.haskellforall.com\/2012\/12\/the-continuation-monad.html\">The continuation monad<\/a>. ~ G. Gonzalez. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/blog.ielliott.io\/continuations-from-the-ground-up\/\">Continuations from the ground up<\/a>. ~ Isaac Elliott. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/matryoshka.gforge.inria.fr\/pubs\/fernandez_burgos_bsc_thesis.pdf\">Formalization of sorting algorithms in Isabelle\/HOL<\/a>. ~ Marco Pierre Fernandez Burgos. #BSc_Thesis #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/github.com\/marco10507\/formalization-of-sorting-algorithms\">Formalization of sorting algorithms in Isabelle\/HOL (Code)<\/a>. ~ Marco Pierre Fernandez Burgos. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29436-6_30.pdf\">Certified equational reasoning via ordered completion<\/a>. ~ C. Sternagel, S. Winkle. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/matryoshka.gforge.inria.fr\/pubs\/blans_bsc_thesis.pdf\">Homotopy type theory: Synthetic homotopy theory and proof verification<\/a>. ~ M. Blans. #BSc_Thesis #ITP #Agda #HoTT<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1908.07776\">Free theorems simply, via dinaturality<\/a>. ~ J. Voigtl\u00e4nder. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/gvolpe.github.io\/blog\/functional-dependencies-and-type-families\/\">Functional dependencies &amp; type families<\/a>. ~ Gabriel Volpe #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.newfrenzy.org\/best-practices-for-using-functional-programming-in-python\/\">Best practices for using functional programming in Python<\/a>. ~ Tara Smith. #Python #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/graninas\/automatic-whitebox-testing-showcase\">Automatic white-box testing with free monads<\/a>. ~ Alexander Granin #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2009\/01\/12\/abstraction-intuition-and-the-monad-tutorial-fallacy\/\">Abstraction, intuition, and the &#8220;monad tutorial fallacy&#8221;<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/blog.sigfpe.com\/2007\/04\/trivial-monad.html\">The trivial monad<\/a>. ~ Dan Piponi. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/two-wrongs.com\/a-gentle-introduction-to-monad-transformers\">A gentle introduction to monad transformers<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/sandrolovnicki\/pLam\">pLam: An interpreter for learning and exploring pure \u03bb-calculus<\/a>. ~ Sandro Lovni\u010dki. #LambdaCalculus #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/stackoverflow.com\/questions\/44965\/what-is-a-monad\">What is a monad?<\/a> #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/gist.github.com\/jhrr\/61727c9934c53f0f06b2\">Programming with effects<\/a>. ~ Graham Hutton. #Haskell #FunctionalProgramming<\/li>\n<li>What is a monad? ~ Graham Hutton. <a href=\"https:\/\/youtu.be\/t1e8gqXLbsU\">https:\/\/youtu.be\/t1e8gqXLbsU<\/a> #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/eduph.github.io\/ANNandSC\/\">Artificial neural networks and simplicial complexes<\/a>. ~ Eduardo Paluzo. #NeuralNetworks #Math<\/li>\n<li><a href=\"http:\/\/www.ps.uni-saarland.de\/Publications\/documents\/Kaiser_2019_Thesis.pdf\">Formal verification of the equivalence of system F and the pure type system L2<\/a>. ~ Jonas Kaiser. #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3342605\">Deferring the details and deriving programs<\/a>. ~ Liam O\u2019Connor. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3342606\">Tic tac types: a gentle introduction to dependently typed programming (functional pearl)<\/a>. ~ S. Innes, N. Wu. #FunctionalProgramming #Idris #Haskell<\/li>\n<li><a href=\"https:\/\/nicksanford.io\/posts\/2018-08-06-haskell-pyramid.html\">Haskell pyramid<\/a>. ~ Nick Sanford. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/haskell-explained.gitlab.io\/blog\/posts\/2019\/08\/27\/pattern-synonyms\">PatternSynonyms for expressive code<\/a>. ~ Raghu Kaippully. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/wiki.haskell.org\/Humor\/LearningCurve\">The Haskell learning curve<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/free.cofree.io\/2019\/08\/21\/mu-nu\/\">Fixed points and non-fixed points of Haskell functors<\/a>. ~ Ziyang Liu. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/free.cofree.io\/2017\/12\/27\/free\/\">Free monoids and free monads, free of category theory<\/a>. ~ Ziyang Liu. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/free.cofree.io\/2019\/07\/31\/beautiful-bridges\/\">Solving the &#8220;Beautiful bridges&#8221; problem, algebraically<\/a>. ~ Ziyang Liu. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/@djoepramono\/that-simple-guide-that-could-help-you-get-started-with-haskell-8af1681c7ef7\">That guide that could help you get started with Haskell<\/a>. ~ Djoe Pramono #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/builds.openlogicproject.org\/courses\/set-theory\/\">Set theory: An open introduction<\/a>. ~ Tim Button. #eBook #SetTheory #Logic #Math<\/li>\n<li><a href=\"https:\/\/mvanier.livejournal.com\/3917.html\">Yet another monad tutorial<\/a>. ~ Mike Vanier. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/SKolodynski\/IsarMathLib\">IsarMathLib: a library of formalized mathematics for Isabelle\/ZF<\/a>. ~ Slawomir Kolodynski. #ITP #IsabelleZF #Math<\/li>\n<li><a href=\"http:\/\/isarmathlib.org\/\">IsarMathLib: A library of formalized mathematics for Isabelle\/ZF theorem proving environment<\/a>. ~ Slawomir Kolodynski. #ITP #IsabelleZF #Math<\/li>\n<li><a href=\"https:\/\/open.library.ubc.ca\/media\/download\/pdf\/24\/1.0380600\/3\">Automated reasoning in first-order real vector spaces<\/a>. ~ C. Kwan. #MSc_Thesis #ITP #ACL2 #Math<\/li>\n<li><a href=\"http:\/\/www.staff.science.uu.nl\/~swier004\/publications\/2019-jfp-submission.pdf\">Functional pearl: Heterogeneous random-access lists<\/a>. ~ W. Swierstra. #FunctionalProgramming #Agda<\/li>\n<li><a href=\"https:\/\/docs.google.com\/presentation\/d\/1bSANLVcGnfVIFjicj81Uo_MYQhsF0FZi_EF-NEKFecE\/edit?usp=sharing\">The Haskell pyramid<\/a>. ~ Lucas Di Cioccio. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/lisp-univ-etc.blogspot.com\/2019\/08\/programming-algorithms-key-values.html\">Programming algorithms: Key-values<\/a>. ~ Vsevolod Dyomkin. #Programming #CommonLisp #Algorithms<\/li>\n<li><a href=\"https:\/\/github.com\/bbatsov\/emacs-lisp-style-guide\">A community-driven Emacs Lisp style guide<\/a>. ~ Bozhidar Batsov. #Programming #Emacs #Lisp<\/li>\n<li><a href=\"https:\/\/github.com\/soupi\/minimal-haskell-emacs\">A minimal Emacs configuration for Haskell programming<\/a>. ~ Gil Mizrahi #Emacs #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/@miguelsaddress\/funtores-aplicativos-y-m%C3%B3nadas-en-im%C3%A1genes-21ab0e60fe23\">Funtores, aplicativos y m\u00f3nadas en im\u00e1genes<\/a>. ~ Miguel \u00c1. Moreno #Haskell #Programaci\u00f3nFuncional<\/li>\n<li><a href=\"https:\/\/sahandsaba.com\/understanding-sat-by-implementing-a-simple-sat-solver-in-python.html\">Understanding SAT by implementing a simple SAT solver in Python<\/a>. ~ Sahand Saba. #Python #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/cdepillabout\/post-about-nix-and-haskell\/blob\/master\/2019-08-03-q-and-as-about-nix-for-haskellers.md\">Questions and answers about Nix for haskellers<\/a>. #Hakell #Nix<\/li>\n<\/ul>\n<\/div>\n<div id=\"postamble\" class=\"status\">\n<p class=\"date\">\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante agosto de 2019, en Twitter fundamentalmente sobre programaci\u00f3n funcional y demostraci\u00f3n asistida por ordenador. Las lecturas est\u00e1n ordenadas seg\u00fan su fecha de publicaci\u00f3n en Twitter. Al final de cada art\u00edculo se encuentran etiquetas relativas a los sistemas que usa o a su contenido. Una recopilaci\u00f3n de&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[6],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6740"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=6740"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6740\/revisions"}],"predecessor-version":[{"id":6741,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6740\/revisions\/6741"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6740"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6740"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6740"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}