{"id":7587,"date":"2020-09-01T18:55:35","date_gmt":"2020-09-01T16:55:35","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7587"},"modified":"2021-08-30T18:57:42","modified_gmt":"2021-08-30T16:57:42","slug":"resumen-de-lecturas-compartidas-durante-agosto-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-agosto-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas durante agosto de 2020"},"content":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante agosto de 2020, 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:\/\/arxiv.org\/abs\/2008.12613\">Type-driven neural programming by example<\/a>. ~ Kiara Grouwstra. #PhD_Thesis #Haskell #FunctionalProgramming #NeuralNetwork<\/li>\n<li><a href=\"https:\/\/gitlab.com\/tycho01\/hasktorch\/-\/tree\/synthesis\/synthesis\">Typed neuro-symbolic program synthesis for the typed lambda calculus<\/a>. ~ Kiara Grouwstra. #Haskell #FunctionalProgramming #NeuralNetwork<\/li>\n<li><a href=\"https:\/\/www.cl.cam.ac.uk\/~lp15\/papers\/Formath\/Ackermann.pdf\">Ackermann&#8217;s function in iterative form: A subtle termination proof with Isabelle\/HOL<\/a>. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/era.ed.ac.uk\/bitstream\/handle\/1842\/37209\/Butler2020.pdf\">Formalising cryptography using CryptHOL<\/a>. ~ David Thomas Butler. #PhD_Thesis #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2008.09253\">Describing console I\/O behavior for testing student submissions in Haskell<\/a>. ~ Oliver Westphal, Janis Voigtl\u00e4nder. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/rainbyte.net.ar\/posts\/200828-01-haskell-0-to-io.html\">Haskell from 0 to IO (Maybe Hero)<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/towardsdatascience.com\/knowledge-representation-and-reasoning-with-answer-set-programming-376e3113a421\">Knowledge representation and reasoning with Answer Set Programming<\/a>. ~ Natalie Kuster. #ASP #LogicProgramming<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/how-close-are-computers-to-automating-mathematical-reasoning-20200827\/\">How close are computers to automating mathematical reasoning?<\/a> ~ Stephen Ornes. #ATP #ITP #Math #CompSci<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/can-computers-solve-the-collatz-conjecture-20200826\/\">Computer scientists attempt to corner the Collatz conjecture<\/a>. ~ Kevin Hartnett. #ATP #SAT_Solver #Math #CompSci<\/li>\n<li><a href=\"https:\/\/www.ac.tuwien.ac.at\/files\/tr\/ac-tr-20-008.pdf\">Finding the hardest formulas for resolution<\/a>. ~ Tom\u00e1\u0161 Peitl, Stefan Szeider. #ATP #SAT_Solver #Logic<\/li>\n<li><a href=\"https:\/\/www.47deg.com\/blog\/what-is-haskell\/\">What is Haskell, and who should use it?<\/a> ~ Jason McClellan. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.05523\">Towards a verified model of the Algorand consensus protocol in Coq<\/a>. ~ Musab A. Alturki et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Relational_Disjoint_Set_Forests.html\">Relational disjoint-set forests in Isabelle\/HOL<\/a>. ~ Walter Guttmann. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/softwarefoundations.cis.upenn.edu\/vc-current\/\">Verifiable C<\/a>. ~ Andrew W. Appel, Qinxiang Cao. #eBook #ITP #Coq<\/li>\n<li><a href=\"https:\/\/youtu.be\/TPpmmkmUaws\">Do more with your types: GADTs and LiquidHaskell<\/a>. ~ Alejandro Serrano, Haskeller. #Haskell #FunctionalProgramming #LiquidHaskell<\/li>\n<li><a href=\"https:\/\/ocaml.xyz\/_downloads\/fb4b6b2df3a933e0d679dbb8a3f72ff9\/book.pdf\">OCaml scientific computing (Functional programming meets Data Science)<\/a>. ~ Liang Wang, Jianxin Zhao. #eBook #OCaml #FunctionalProgramming #DataScience<\/li>\n<li><a href=\"http:\/\/anshula.com\/blog\/latticetheoryduality.pdf\">Automating proofs of lattice inequalities in Coq with reinforcement learning and duality<\/a>. ~ Anshula Gandhi, Favio E. Miranda-Perea, Lourdes del Carmen Gonz. #ITP #Coq #MachineLearning<\/li>\n<li><a href=\"https:\/\/sites.google.com\/view\/anshula-research-blog\/entries\/getting-started-with-proving-math-theorems-through-reinforcement-learning\">Getting started with proving math theorems through reinforcement learning (An experiment at MIT&#8217;s Brains, Minds, and Machines Lab)<\/a>. ~ Anshula Gandhi. #ITP #Coq #MachineLearning<\/li>\n<li><a href=\"https:\/\/sites.google.com\/view\/anshula-research-blog\/entries\/guaranteeing-proof-termination\">Guaranteeing proof termination (Dealing with infinite proof search in reinforcement-learning automated proofs)<\/a>. ~ Anshula Gandhi. #ITP #Coq #MachineLearning<\/li>\n<li><a href=\"https:\/\/ucsd-progsys.github.io\/liquidhaskell-blog\/2020\/08\/20\/lh-as-a-ghc-plugin.lhs\/\">LiquidHaskell is a GHC plugin<\/a>. ~ Ranjit Jhala. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/amandeepsp.github.io\/fp-is-awesome\/\">Functional programming is awesome!!<\/a> ~ Amandeep Singh. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.logicmatters.net\/resources\/pdfs\/IFL2_LM.pdf\">An introduction to formal logic<\/a>. ~ Peter Smith. #eBook #Logic<\/li>\n<li><a href=\"https:\/\/www.logicmatters.net\/resources\/pdfs\/godelbook\/GodelBookLM.pdf\">An introduction to G\u00f6del&#8217;s theorems<\/a>. ~ Peter Smith. #eBook #Logic<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2020-08-22-some-more-list-algorithms.html\">Some more list algorithms<\/a>. ~ Donnacha Ois\u00edn Kidney. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/EgbertRijke\/HoTT-Intro\">Introduction to Homotopy Type Theory<\/a>. ~ Egbert Rijke. #HoTT #ITP #Agda #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2008.09067v1\">Adventures in mathematical reasoning<\/a>. ~ Toby Walsh. #ATP #Math<\/li>\n<li><a href=\"https:\/\/www.well-typed.com\/blog\/2020\/08\/memory-fragmentation\/\">Understanding memory fragmentation<\/a>. ~ David Eichmann. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/julesh.com\/2020\/08\/15\/probabilistic-programming-with-continuations\/\">Probabilistic programming with continuations<\/a>. ~ Jules Hedges. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.ams.org\/journals\/bull\/2017-54-03\/S0273-0979-2016-01556-4\/S0273-0979-2016-01556-4.pdf\">Five stages of accepting constructive mathematics<\/a>. ~ Andrej Bauer. #Logic #Math<\/li>\n<li><a href=\"https:\/\/mathvault.ca\/hub\/higher-math\/math-symbols\/logic-symbols\/\">Logic symbols (A comprehensive collection of the most notable symbols in formal\/mathematical logic)<\/a>. ~ Math Vault. #Logic #Math<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/Talks\/quarantine.pdf\">Formal Mathematics and the Lean theorem prover<\/a>. ~ Jeremy Avigad. #Logic #Math #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/youtu.be\/uPCxm1_R_4I\">Formal Mathematics and the Lean theorem prover [Video<\/a>]. ~ Jeremy Avigad. #Logic #Math #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3406088.3409022\">Effect handlers in Haskell, evidently<\/a>. ~ Ningning Xie, Daan Leijen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3406088.3409016\">Scripted signal functions<\/a>. ~ David A. Stuart. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/lexi-lambda.github.io\/blog\/2020\/08\/13\/types-as-axioms-or-playing-god-with-static-types\/\">Types as axioms, or: playing god with static types<\/a>. ~ Alexis King. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2008.07912\">Inductive logic programming at 30: a new introduction<\/a>. ~ Andrew Cropper, Sebastijan Duman\u010di\u0107. #ILP #MachineLearning #LogicProgramming<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/computer-search-settles-90-year-old-math-problem-20200819\">Computer search settles 90-year-old Math problem<\/a>. ~ Kevin Hartnett. #Math #CompSci #ATP #SAT_Solvers<\/li>\n<li><a href=\"https:\/\/schooloffp.co\/2020\/08\/17\/whirlwind-tour-of-cabal-for-beginners.html\">Whirlwind tour of Cabal for beginners<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/felixmulder.com\/writing\/2020\/08\/20\/How-Stylish-Haskell-works.html\">How stylish-haskell works<\/a>. ~ Felix Mulder. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3406088.3409024\">A graded Monad for deadlock-free concurrency (Functional Pearl)<\/a>. ~ Andrej Iva\u0161kovi\u0107, Alan Mycroft. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3406088.3409026\">Finger trees explained anew, and slightly simplified (Functional Pearl)<\/a>. ~ Koen Claessen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/enhancing-functor-structures-step-by-step-1.html\">Enhancing functor structures step-by-step (Part 1)<\/a>. ~ Justin Le. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/enhancing-functor-structures-step-by-step-2.html\">Enhancing functor structures step-by-step (Part 2)<\/a>. ~ Justin Le. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mathvault.ca\/hub\/higher-math\/math-symbols\/set-theory-symbols\/\">Set theory symbols<\/a>. ~ Math Vault. #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Ordinal_Partitions.html\">Ordinal partitions in Isabelle\/HOL<\/a>. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/eprint.iacr.org\/2020\/962.pdf\">Post-quantum verification of Fujisaki-Okamoto<\/a>. ~ Dominique Unruh. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/youtu.be\/UjcpfKtq7wY\">Logipedia: towards a Wikipedia of formal proofs<\/a>. ~ Gilles Dowek. #ITP #Math<\/li>\n<li><a href=\"https:\/\/topology.pubpub.org\/\">Topology (A categorical approach)<\/a>. ~ Tai-Danae Bradley, Tyler Bryson, and John Terilla. #Ebook #Math #CategoryTheory<\/li>\n<li><a href=\"https:\/\/www.helsinki.fi\/sites\/default\/files\/atoms\/files\/finalshortpapermain.pd\">Hybrid logic in the Isabelle proof assistant: Benefits, challenges and the road ahead<\/a>. ~ Asta Halkj\u00e6r From.f#page=27 #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1906.11203\">A formalisation of the SPARC TSO memory model for multi-core machine code<\/a>. ~ Zhe Hou, David Sanan, Alwen Tiu, Yang Liu, Jin Song Dong. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.helsinki.fi\/sites\/default\/files\/atoms\/files\/finalshortpapermain.pd\">Generalised Veltman semantics in Agda<\/a>. ~ J.M. Rovira, L. Mikec, J.J. Joosten.f#page=90 #ITP #Agda #Logic<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3386569.3392375\">Penrose: from mathematical notation to beautiful diagrams<\/a>. ~ K. Ye, W. Ni, M. Krieger, D. Ma&#8217;ayan, J. Wise, J. Aldrich. #DSL #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"http:\/\/fse.studenttheses.ub.rug.nl\/23070\/1\/bCS_2020_HarmannyAJ.pdf\">Automatic verification of annotated sequential imperative programs<\/a>. ~ Alinda Harmanny. #Haskell #FunctionalProgramming #Logic<\/li>\n<li><a href=\"https:\/\/notxor.nueva-actitud.org\/blog\/2020\/08\/14\/un-poco-mas-sobre-magit\/\">Un poco m\u00e1s sobre magit<\/a>. #Emacs #Git<\/li>\n<li><a href=\"https:\/\/github.com\/foxthomson\/impartial\">A proof of the Sprague-Grundy theorem and other results related to impartial games in Lean<\/a>. ~ Fox Thomson. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1904.03241\">HOList: An environment for machine learning of higher-order theorem proving<\/a>. ~ Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, Stewart Wilcox. #ITP #HOL_Light #MachineLearning<\/li>\n<li><a href=\"https:\/\/kowainik.github.io\/posts\/haskell-mini-patterns\">Haskell mini-patterns handbook<\/a>. ~ Dmitrii Kovanikov, Veronika Romashkina. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2008.04165v1\">Proof-carrying plans: a resource logic for AI planning<\/a>. ~ Alasdair Hill, Ekaterina Komendantskaya, Ronald P. A. Petrick. #ITP #Agda #AI<\/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>. ~ Ralph Bottesch, Max W. Haslbeck, Ren\u00e9 Thiemann. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/olivernash.org\/2020\/08\/08\/mathlib\/index.html\">The Mathlib formalisation project needs your help (A serious effort to formalise modern mathematics)<\/a>. ~ Oliver Nash. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/lean-forward.github.io\/lean-together\/2019\/slides\/wu.pdf\">A verified tableau prover for modal logic K- ~ Minchao Wu<\/a>. #ITP #LeanProver #Logic<\/li>\n<li><a href=\"https:\/\/iokasimov.github.io\/posts\/2020\/08\/wgc-effects\">Cross wolf, goat and cabbage across the river with effects<\/a>. ~ Murat Kasimov #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/jmtd.net\/log\/generic_haskell\/\">Generic Haskell<\/a>. ~ Jonathan Dowland. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/wcl.cs.rpi.edu\/papers\/DDDAS2020_Cruz.pdf\">Towards provably correct probabilistic flight systems<\/a>. ~ Elkin Cruz-Camacho, Saswata Paul, Fotis Kopsaftopoulos, Carlos A. Varela. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Amicable_Numbers.html\">Amicable numbers in Isabelle\/HOL<\/a>. ~ Angeliki Koutsoukou-Argyraki. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/lean-forward.github.io\/lean-together\/2019\/slides\/buzzard.pdf\">Using Lean with undergraduate mathematicians<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/lean-forward.github.io\/lean-together\/2019\/slides\/hoelzl.pdf\">mathlib: Lean\u2019s mathematical library<\/a>. ~ Johannes H\u00f6lzl. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/lean-forward.github.io\/lean-together\/2019\/slides\/hudon.pdf\">Embedding specialized proof languages into Lean (A case study)<\/a>. ~ Simon Hudon. #ITP #LeanProver #Logic<\/li>\n<li><a href=\"https:\/\/lean-forward.github.io\/lean-together\/2019\/slides\/lewis.pdf\">A formal proof of Hensel\u2019s lemma over the p-adic integers<\/a>. ~ Robert Y. Lewis. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/w2XCnbLBHmw\">How to design co-programs<\/a>. ~ Jeremy Gibbons. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/bentnib.org\/posts\/2020-08-13-non-idempotent-intersection-types.html\">Quantitative typing with non-idempotent intersection types<\/a>. ~ Bob Atkey. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/lean-forward.github.io\/lean-together\/2019\/slides\/avigad.pdf\">Datatypes as quotients of polynomial functors<\/a>. ~ Jeremy Avigad. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/lean-forward.github.io\/lean-together\/2019\/slides\/barton.pdf\">Model categories in Lean<\/a>. ~ Reid Barton. #ITP #LeanProver #CategoryTheory<\/li>\n<li><a href=\"https:\/\/lean-forward.github.io\/lean-together\/2019\/slides\/bentzen.pdf\">A formalization of a Henkin-style completeness proof for propositional modal logic in Lean<\/a>. ~ Bruno Bentzen. #ITP #LeanProver #Logic<\/li>\n<li><a href=\"https:\/\/lean-forward.github.io\/lean-together\/2019\/slides\/blanchette.pdf\">So what are hammers good for?<\/a> ~ Jasmin Blanchette. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/youtu.be\/gm2pK01S8_g\">Data vs Control: a tale of two functors<\/a>. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/icgl9FuPxKA\">Building a web library using super hard Haskell<\/a>. ~ Marcin Rze\u017anicki. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/2uD6bCbL1-A\">Zero-overhead abstractions in Haskell using staging<\/a>. ~ Andres L\u00f6h. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.andreipopescu.uk\/pdf\/conserv_HOL_IsabelleHOL.pdf\">Safety and conservativity of definitions in HOL and Isabelle\/HOL<\/a>. ~ Ond\u0159ej Kun\u010dar, Andrei Popescu. #Logic #ITP #HOL #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02380196v2\/document\">Coq Coq correct! (Verification of type checking and erasure for Coq, in Coq)<\/a>. ~ M. Sozeau, S. Boulier, Y. Forster, N. Tabareau, T. Winterhalter. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-02422273\/document\">FreeSpec: Specifying, verifying and executing impure computations in Coq<\/a>. ~ Thomas Letan, Yann R\u00e9gis-Gianas. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/eprints.whiterose.ac.uk\/161211\/15\/Popescu2020_Article_CoConAConferenceManagementSyst.pdf\">CoCon: A conference management system with formally verified document confidentiality<\/a>. ~ Andrei Popescu, Peter Lammich, Ping Hou. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/youtu.be\/fty9QL4aSRc\">Haskell to core: Understanding Haskell features through their desugaring<\/a>. ~ Vladislav Zavialov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/KY27LsV11Rg\">Agile generation of Cloud API bindings with Haskell<\/a>. ~ Michal Gajda. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/JbeqwfZ2dRc\">GraphQL :heart: Haskell<\/a>. ~ Alejandro Serrano. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/FDx0nXFQloE\">Formalising undergraduate mathematics<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/wwwf.imperial.ac.uk\/~buzzard\/one_off_lectures\/ug_maths.pdf\">Formalising undergraduate mathematics [Slides<\/a>]. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/devanla.com\/posts\/read-you-a-blaze.html\">Read you a blaze<\/a>. ~ Guru Devanla. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/b3wRqlEc6ts\">Down to the wire<\/a>. ~ Eric Torreborre. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/LBiFYbQMAXc\">Getting acquainted with Lens<\/a>. ~ Pawel Szulc. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/wb5PLv6-e6I\">Stan: Haskell static analyser<\/a>. ~ Veronika Romashkina, Dmitrii Kovanikov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.genbeta.com\/desarrollo\/lenguaje-prolog-ejemplo-paradigma-programacion-logica\">El lenguaje Prolog: un ejemplo del paradigma de programaci\u00f3n l\u00f3gica<\/a>. ~ Marcos Merino #Prolog #Programaci\u00f3nL\u00f3gica<\/li>\n<li><a href=\"https:\/\/blog.patchgirl.io\/haskell\/2020\/08\/02\/testing-haskell-with-stack-ghcid-and-hspec.html\">Testing Haskell code with Stack, Ghcid and Hspec<\/a>. ~ Iori Matsuhara. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/boxbase.org\/entries\/2020\/aug\/5\/how-a-haskell-programmer-wrote-a-tris-in-haskell\/\">How a Haskell programmer wrote a tris in Purescript<\/a>. ~ Henri Tuhola. #Haskell #Purescript #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/lorentz-haskell-newtypes\">Lorentz: Achieving correctness with Haskell Newtypes<\/a>. ~ Kostya Ivanov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.fpcomplete.com\/haskell\/tutorial\/fundeps\/\">Functional dependencies<\/a>. ~ Michael Snoyman. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/4i8hvUcKnH0\">Clojure basics: How code is evaluated<\/a>. #Clojure #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/jH2Je6wUvPs\">Elastic sheet-defined functions<\/a>. ~ Simon Peyton Jones. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/5-P0Jjku3cY\">The many faces of isOrderedTree<\/a>. ~ Joachim Breitner. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/HhpH8DKFBls\">Bit vectors without compromises<\/a>. ~ Andrew Lelechenko. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www21.in.tum.de\/~eberlm\/pdfs\/algorithms_survey.pdf\">Verified textbook algorithms (A biased survey)<\/a>. ~ T. Nipkow, M. Eberl, M.P.L. Haslbeck. #ITP #FormalVerification #Algorithms<\/li>\n<li><a href=\"https:\/\/scholarship.tricolib.brynmawr.edu\/bitstream\/handle\/10066\/22621\/2020LowensteinS.pdf?sequence=1&amp;isAllowed=y\">Tools for teaching Theoretical Computer Science<\/a>. ~ Sam Lowenstein. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.taezos.dev\/posts\/2020-07-30-extracting-io.html\">Haskell &#8211; Extracting IO<\/a>. ~ Ken Aguilar. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.michaelpj.com\/blog\/2020\/08\/02\/lenses-for-tree-traversals.html\">Lenses for tree traversas<\/a>. ~ Michael Peyton Jones. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.poisson.chat\/posts\/2020-08-08-definitional-lawfulness.html\">Definitional lawfulness: proof by inspection testing<\/a>. ~ Li-yao Xia. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/michaelbeeson.com\/research\/papers\/Tarski-JAR.pdf\">Finding proofs in Tarskian geometry<\/a>. ~ M. Beeson, L. Wos. #ATP #Otter #Math via @SandMouth<\/li>\n<li><a href=\"https:\/\/www.philipzucker.com\/defunctionalizing-arithmetic-to-an-abstract-machine\/\">Defunctionalizing arithmetic to an abstract machine<\/a>. ~ Philip Zucker. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2008.00120\">The Tactician (extended version): A seamless, interactive tactic learner and prover for Coq<\/a>. ~ Lasse Blaauwbroek, Josef Urban, Herman Geuvers. #ITP #Coq #MachineLearning<\/li>\n<li><a href=\"https:\/\/leanprover.github.io\/theorem_proving_in_lean\/\">Theorem proving in Lean (Release 3.18.4, Aug 06, 2020)<\/a>. ~ Jeremy Avigad, Leonardo de Moura, Soonho Kong. #eBook #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/100.html\">Formalizing 100 theorems in Lean<\/a>. #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/www.lirmm.fr\/~viampietro\/files\/SHARC19.pdf\">Designing critical digital systems (Formal verification of a token player for synchronously executed Petri Nets)<\/a>. ~ Vincent Iampietro. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/cicm-conference.org\/2020\/NFM\/paper_1_Koepke_Penquitt_Schuetz_Sturzenhecker.pdf\">Formalizing foundational notions in Naproche-SAD<\/a>. ~ P. Koepke, J. Penquitt, M. Sch\u00fctz, E. Sturzenhecker. #ITP #NaprocheSAD #Math<\/li>\n<li><a href=\"https:\/\/paedubucher.ch\/articles\/2020-08-03-four-in-a-row-in-haskell-part-i.html\">\u00abFour in a Row\u00bb in Haskell (Part I: Background and General Considerations)<\/a>. ~ Patrick Bucher. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/paedubucher.ch\/articles\/2020-08-05-four-in-a-row-in-haskell-part-ii.html\">\u00abFour in a Row\u00bb in Haskell (Part II: Implementation of the Board Logic)<\/a>. ~ Patrick Bucher. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/people.math.harvard.edu\/~knill\/graphgeometry\/papers\/fundamental.pdf\">Some fundamental theorems in Mathematics<\/a>. ~ Oliver Knill. #Math<\/li>\n<li><a href=\"https:\/\/research.fb.com\/wp-content\/uploads\/2020\/08\/Eliminating-Bugs-with-Dependent-Haskell-Experience-Report.pdf\">Eliminating bugs with dependent Haskell(Experience report)<\/a>. ~ Noam Zilberstein. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.andres-loeh.de\/StagedSOP\/staged-sop-paper.pdf\">Staged sums of products<\/a>. ~ Matthew Pickering, Andres L\u00f6h, Nicolas Wu. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/i-am-tom\/haskell-exercises\">GHC exercises (A little course to learn about some of the more obscure GHC extensions)<\/a>. ~ Tom Harding. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.poisson.chat\/posts\/2020-08-05-applicative-difference-lists.html\">Generic traversals with applicative difference lists<\/a>. ~ Li-yao Xia. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2020\/07\/effev.pdf\">Effect handlers in Haskell, evidently<\/a>. ~ N. Xie, D. Leijen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/richarde.dev\/papers\/2018\/stitch\/stitch.pdf\">Stitch: the sound type-indexed type checker (functional pearl)<\/a>. ~ R.A. Eisenberg. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/richarde.dev\/papers\/2020\/workflows\/workflows.pdf\">Composing effects into tasks and workflows<\/a>. ~ Y. Par\u00e8s, J.P. Bernardy, R.A. Eisenberg. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/bolt12\/tymfgg-pearl\">Type your matrices for great good (Functional pearl): A Haskell library of typed matrices and applications<\/a>. ~ Armando Santos. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/blog.merigoux.ovh\/en\/2019\/12\/20\/taxes-formal-proofs.html\">A mathematical formulation of the tax code? (Reverse engineering the tax code and analysis by automated theorem proving)<\/a>. ~ Denis Merigoux. #ATP #SMT<\/li>\n<li><a href=\"https:\/\/terrytao.wordpress.com\/2010\/10\/21\/245a-problem-solving-strategies\/\">Problem solving strategies<\/a>. ~ Terence Tao (2010). #Math<\/li>\n<li><a href=\"https:\/\/solmos.netlify.app\/post\/2020-07-06-emacs-for-statisticians\/emacs-for-statisticians\/\">Emacs for statisticians (Part 1): Analyzing data on remote servers using Spacemacs and ESS<\/a>. ~ Sergio Olmos. #Emacs #Rstat<\/li>\n<li><a href=\"https:\/\/pdxscholar.library.pdx.edu\/pdxopen\/29\/\">Lectures on mathematical computing with Python<\/a>. ~ Jay Gopalakrishnan. #eBook #Python #Math<\/li>\n<li><a href=\"https:\/\/www.cs.us.es\/~jalonso\/apuntes\/Matematicas_en_Lean\/Matematicas_en_Lean.pdf\">#ForMatUS: Libro &#8220;Matem\u00e1ticas en Lean&#8221;<\/a>. #DAO #LeanProver #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/www.philipzucker.com\/checkpoint-implementing-linear-relations-for-linear-time-invariant-systems\/\">Checkpoint: Implementing linear relations for linear time invariant systems<\/a>. ~ Philip Zucker. #JuliaLang #CategoryTheory<\/li>\n<li><a href=\"https:\/\/www.47deg.com\/blog\/mu-in-haskell-symposium\/\">Describing microservices using modern Haskell<\/a>. ~ Alejandro Serrano. #FuncionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/gergo.erdi.hu\/blog\/2020-08-01-solving_text_adventure_games_via_symbolic_execution\/\">Solving text adventure games via symbolic execution<\/a>. ~ Gerg\u0151 \u00c9rdi. #Haskell #FunctionalProgramming #SMT<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante agosto de 2020, 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\/7587"}],"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=7587"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7587\/revisions"}],"predecessor-version":[{"id":7588,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7587\/revisions\/7588"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7587"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7587"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7587"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}