{"id":6719,"date":"2019-01-01T10:59:02","date_gmt":"2019-01-01T09:59:02","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6719"},"modified":"2019-09-01T11:00:39","modified_gmt":"2019-09-01T09:00:39","slug":"resumen-de-lecturas-compartidas-durante-diciembre-de-2018","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-diciembre-de-2018\/","title":{"rendered":"Resumen de lecturas compartidas durante diciembre de 2018"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante diciembre de 2018, 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>.<\/p>\n<p><!--more--><\/p>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/arxiv.org\/abs\/1803.05998\">|{Math, Philosophy, Programming, Writing}| = 1<\/a>. ~ Attila Egri-Nagy. #Math #Philosophy #Programming<\/li>\n<li><a href=\"https:\/\/pdfs.semanticscholar.org\/7454\/9e68cca4d929fd008c259a2dc18667e0efe7.pdf\">Certifying the true error: Machine learning in Coq with verified generalization guarantees<\/a>. ~ A. Bagnall, G. Stewart. #ITP #Cop #MachineLearnig<\/li>\n<li><a href=\"https:\/\/www.ideals.illinois.edu\/bitstream\/handle\/2142\/102075\/casper-report.pdf\">Verification of Casper in the Coq proof assistant<\/a>. ~ K. Palmskog et als. #ITP #Coq #Blockchain<\/li>\n<li><a href=\"http:\/\/www.lsv.fr\/~fthire\/research\/sttforall\/paper\/sttforall.pdf\">Sharing a library between proof assistants: reaching out to the HOL family<\/a>. ~ F. Thir\u00e9. #ITP #Dedukti #Coq #Matita #OpenTheory #LeanProver #PVS<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-01668246\/file\/presentation.pdf\">Interoperability between arithmetic proofs using Dedukti<\/a>. ~ F. Thir\u00e9 #ITP #Dedukti #Coq #Matita #OpenTheory #LeanProver #PVS<\/li>\n<li><a href=\"https:\/\/github.com\/Deducteam\/Logipedia\">Logipedia: an arithmetic library that is shared between several proof systems<\/a>. ~ F. Thir\u00e9. #ITP #Dedukti #Coq #Matita #OpenTheory #LeanProver #PVS<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1811.09840\">Three Euler\u2019s sieves and a fast prime generator (Functional pearl)<\/a>. ~ I. Salvo, A. Pacifico. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"http:\/\/www.st.cs.uni-saarland.de\/edu\/seminare\/2005\/advanced-fp\/slides\/meiser.pdf\">QuickCheck (a lightweight tool for random testing of Haskell programs)<\/a>. ~ K. Claessen, J. Hughes. #Haskell #QuickCheck<\/li>\n<li><a href=\"https:\/\/www.lri.fr\/~mpereira\/thesis.pdf\">Tools and techniques for the verification of modular stateful code<\/a>. ~ M.J. Parreira. #ITP #Why3<\/li>\n<li><a href=\"http:\/\/wadler.blogspot.com\/2018\/12\/programming-language-foundations-in-agda.html\">Programming language foundations in Agda<\/a>. ~ Philip Wadler. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/youtu.be\/NGBsSOOXv1A\">Histoire des math\u00e9matiques dans l&#8217;humanit\u00e9<\/a>. ~ Cedric Villani. #Math<\/li>\n<li><a href=\"https:\/\/plfa.github.io\">Programming language foundations in Agda<\/a>. ~ Philip Wadler, Wen Kokke. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1811.11317\">Adventures in formalisation: Financial contracts, modules, and two-level type theory<\/a>. ~ Danil Annenkov. #PhD_Thesis #ITP #Coq #Agda #Lean<\/li>\n<li><a href=\"http:\/\/cs.lmu.edu\/~ray\/notes\/introhaskell\">Introduction to Haskell<\/a>. ~ Ray Toal #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/cs.lmu.edu\/~ray\/classes\/pl\/\">Course: Programming languages<\/a>. ~ Ray Toal #Programming<\/li>\n<li><a href=\"https:\/\/github.com\/ekmett\/guanxi\">guanxi: An exploration of relational programming in Haskell<\/a>. ~ Edward Kmett #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.isle.org\/~langley\/papers\/integrative.eaai19.pdf\">An integrative framework for artificial intelligence education<\/a>. ~ P. Langley. #Teaching #AI<\/li>\n<li><a href=\"https:\/\/thealmarty.com\/2018\/12\/04\/programming-with-lenses-in-haskell-and-ocaml\/\">Programming with Lenses in Haskell and OCaml<\/a>. #Haskell #OCaml #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.parsonsmatt.org\/2018\/12\/04\/laziness_quiz.html\">Laziness Quiz<\/a>. ~ Matt Parsons. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/gitlab.com\/danielhones\/pycategories\">Pycategories: Python library implementing ideas from category theory<\/a>. ~ Daniel Hones. #Python #Haskell #CategoryTheory<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/alchemical-groups.html\">Alchemical groups: Advent of code with free groups and group homomorphisms<\/a>. ~ Justin Le. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/gallium.inria.fr\/blog\/fixin-your-automata\/\">Fixin&#8217; your automata<\/a>. ~ Fran\u00e7ois Pottier. #OCaml #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/bor0.wordpress.com\/2018\/12\/05\/dependently-typed-lambda-calculus-in-haskell\/\">Dependently typed lambda calculus in Haskell<\/a>. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/@ertu.ctn\/why-clojure-seriously-why-9f5e6f24dc29\">Why Clojure? I\u2019ll tell you why \u2026<\/a> ~ Ertu\u011frul \u00c7etin. #Clojure #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.freecodecamp.org\/a-behind-the-scenes-look-at-map-filter-and-reduce-in-swift-1991f5c7bc80\">A behind the scenes look at Map, Filter, and Reduce in Swift<\/a>. ~ Boudhayan Biswas. #Swift #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dev.to\/leandrotk_\/functional-programming-principles-in-javascript-26g7\">Functional programming principles in Javascript<\/a>. ~ @leandrotk_ #FunctionalProgramming #JavaScript<\/li>\n<li><a href=\"http:\/\/t-news.cn\/Floc2018\/FLoC2018-pages\/proceedings_paper_123.pdf\">Verified analysis of random binary tree structures<\/a>. ~ M. Eberl, M.W. Haslbeck, T. Nipkow. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/t-news.cn\/Floc2018\/FLoC2018-pages\/proceedings_paper_325.pdf\">Automated theorem proving in a chat environment<\/a>. ~ R. Zhumagambetov, M. Sterling. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/t-news.cn\/Floc2018\/FLoC2018-pages\/proceedings_paper_4.pdf\">Automating the diagram method to prove correctness of program transformations<\/a>. ~ D. Sabel. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/t-news.cn\/Floc2018\/FLoC2018-pages\/proceedings_paper_13.pdf\">A simple functional presentation and an inductive correctness proof of the Horn algorithm<\/a>. ~ A. Ravara. #Logic #SAT<\/li>\n<li><a href=\"http:\/\/t-news.cn\/Floc2018\/FLoC2018-pages\/proceedings_paper_322.pdf\">Implementing a proof assistant using focusing and logic programming<\/a>. ~ T. Libal. #ITP #LogicProgramming #Prolog<\/li>\n<li><a href=\"http:\/\/t-news.cn\/Floc2018\/FLoC2018-pages\/proceedings_paper_287.pdf\">Shaving with Occam&#8217;s razor: deriving minimalist theorem provers for minimal logic<\/a>. ~ P. Tarau. #Logic #ATP #Prolog #LogicProgramming<\/li>\n<li><a href=\"http:\/\/t-news.cn\/Floc2018\/FLoC2018-pages\/proceedings_paper_755.pdf\">Rating of geometric automated theorem provers<\/a>. ~ N. Baeta, P. Quaresma. #ATP #Geometry<\/li>\n<li><a href=\"https:\/\/qfpl.io\/posts\/intro-to-state-machine-testing-3\/\">Introduction to state machine testing: part 3<\/a>. ~ Andrew McMiddlin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/lens-by-example.chrispenner.ca\/articles\/traversals\/writing-traversals\">Lens by example: Writing traversals<\/a>. ~ Chris Penner. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/docs.perl6.org\/language\/haskell-to-p6\">Haskell to Perl 6: nutshell (Learning Perl 6 from Haskell, in a nutshell)<\/a>. #Haskell #Perl<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/griff\/publications\/Lochmann-Sternagel-CPP19.pdf\">Certified ACKBO<\/a>. ~ A. Lochmann, C. Sternagel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/t-news.cn\/Floc2018\/FLoC2018-pages\/proceedings_paper_761.pdf\">Towards intuitive reasoning in axiomatic geometry<\/a>. ~ M. Dor\u00e9, K. Broda. #ITP #ELFE #Haskell #Math<\/li>\n<li><a href=\"https:\/\/www.onikudaki.net\/blog\/archives\/196\">Binding to a C++ CORBA interface in Haskell<\/a>. ~ Michael Oswald. #Haskell #Cpp<\/li>\n<li><a href=\"http:\/\/matryoshka.gforge.inria.fr\/pubs\/metathy_paper.pdf\">Formalizing the metatheory of logical calculi and automatic provers in Isabelle\/HOL<\/a>. ~ J.C. Blanchette. #ITP #IsabelleHOL #Logic #ATP<\/li>\n<li><a href=\"https:\/\/bitbucket.org\/isafol\/isafol\/wiki\/Home\">IsaFoL: Isabelle Formalization of Logic<\/a>. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/www21.in.tum.de\/~haslbema\/documents\/provingcontests_draft18.pdf\">Competitive proving for fun<\/a>. ~ M.P.L. Haslbeck, S. Wimmer. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/github.com\/ProofSystem\/Encyclopedia\/blob\/master\/main.pdf\">Towards an encyclopaedia of proof systems<\/a>. #Logic<\/li>\n<li><a href=\"http:\/\/ps.uni-saarland.de\/Publications\/documents\/Schneider_2018_PhDThesis.pdf\">A verified compiler for a linear imperative\/functional intermediate language<\/a>. ~ S. Schneider. #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/dspace.library.uu.nl\/bitstream\/handle\/1874\/369181\/Thesis-Tomas-Ehrencron.pdf\">Techniques behind SMT solvers<\/a>. ~ T. Ehrencron. #SMT #LiquidHaskell #ATP<\/li>\n<li><a href=\"https:\/\/interestingengineering.com\/15-of-the-most-important-algorithms-that-helped-define-mathematics-computing-and-physics%20\">15 of the most important algorithms that helped define Mathematics, Computing, and Physics<\/a>. ~ C. McFadden. #Algorithms #Math #CompSci #Physics<\/li>\n<li><a href=\"https:\/\/medium.com\/syncedreview\/2018-in-review-10-ai-failures-c18faadf5983\">2018 in review: 10 AI failures<\/a>. #AI<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1812.03624\">Formalization of metatheory of the Quipper quantum programming language in a linear logic<\/a>. ~ M.Y. Mahmoud, A.P. Felty. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/jeremydaw\/idt\">Intuitionistic dual tableaux in HOL<\/a>. ~ Jeremy E. Dawson. #ITP #HOL #Logic<\/li>\n<li><a href=\"https:\/\/blogs.ncl.ac.uk\/andreymokhov\/united-monoids\/\">United monoids<\/a>. ~ A. Mokhov. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/shifting-the-stars.html\">Shifting the stars: Advent of code with galilean optimization<\/a>. ~ Justin Le. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2018-12-12-benchgraph.html\">DIY benchmark history with Criterion and Shiny<\/a>. ~ Th\u00e9ophane Hufschmitt. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/@fommil\/why-not-both-8adadb71a5ed\">Why not both? (Build Haskell projects with either cabal or stack)<\/a>. ~ Sam Halliday. #Haskell<\/li>\n<li><a href=\"https:\/\/nokomprendo.frama.io\/tuto_fonctionnel\/posts\/tuto_fonctionnel_25\/2018-08-25-en-README.html\">A webcam server in 35 lines of Haskell<\/a>. #Haskell<\/li>\n<li><a href=\"http:\/\/sagebook.gforge.inria.fr\/english.html\">Computational mathematics with SageMath<\/a>. ~ Paul Zimmermann et als. #eBook #SageMath<\/li>\n<li><a href=\"https:\/\/link.springer.com\/article\/10.1007\/s10817-018-09504-w\">A verified implementation of algebraic numbers in Isabelle\/HOL<\/a>. ~ S.J.C. Joosten, R. Thiemann, A. Yamada. #ITP #IsabelleHOL #Haskell #Math<\/li>\n<li><a href=\"http:\/\/www.lix.polytechnique.fr\/Labo\/Dale.Miller\/blanco-phd-draft.pdf\">Applications of foundational proof certificates in theorem proving<\/a>. ~ M. Roberto. #PhD_Thesis #FPC #ATP<\/li>\n<li><a href=\"https:\/\/www.lri.fr\/~mpereira\/thesis.pdf\">Tools and techniques for the verification of modular stateful code<\/a>. ~ M.J. Pereira. #PhD_Thesis #ITP #Why3<\/li>\n<li><a href=\"https:\/\/plus.maths.org\/content\/will-machine-learning-replace-mathematicians\">Will machine learning replace mathematicians?<\/a> ~ Chris Budd. #Math #AI #ITP<\/li>\n<li><a href=\"https:\/\/github.com\/isovector\/thinking-with-types\">Thinking with types: Type-level programming in Haskell<\/a>. ~ Sandy Maguire. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/thescipub.com\/pdf\/10.3844\/jmssp.2018.209.218\">Formalizing probability concepts in a type theory<\/a>. ~ F. Kachapova. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1712.07474\">Can one design a geometry engine? On the (un)decidability of affine Euclidean geometries<\/a>. ~ J.A. Makowsky. #Logic #Math #ATP<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1812.03318\">A verified Timsort C implementation in Isabelle\/HOL<\/a>. ~ Y. Zhang, Y. Zhao, D. Sanan. #ITP #IsabelleHOL #Algorithms<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1812.05878\">In praise of sequence (co-)algebra and its implementation in Haskell<\/a>. ~ K. Clenaghan. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/www.nytimes.com\/2018\/12\/17\/science\/donald-knuth-computers-algorithms-programming.html\">The Yoda of Silicon Valley<\/a>. ~ S. Roberts. #CompSci<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/2018\/12\/17\/why-dependent-haskell\">Why dependent Haskell is the future of software development<\/a>. ~ V. Zavialov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-01830255v2\/document\">A Coq mechanised formal semantics for realistic SQL queries (Formally reconciling SQL and bag relational algebra)<\/a>. ~ V. Benzaken, \u00c9. Contejean. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/matryoshka.gforge.inria.fr\/pubs\/overbeek_msc_thesis.pdf\">Formalizing the semantics of concurrent revisions<\/a>. ~ R. Overbeek. #Msc_Thesis #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Order_Lattice_Props.html\">Properties of orderings and lattices<\/a>. ~ G. Struth. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Constructive_Cryptography.html\">Constructive cryptography in HOL<\/a>. ~ A. Lochbihler, S.R. Sefidgar. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/2018\/11\/14\/logical-background\">Constructive and non-constructive proofs in Agda (Part 1): Logical background<\/a>. ~ Danya Rogozin #ITP #Agda #Logic<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/2018\/11\/26\/agda-in-nutshell\">Constructive and non-constructive proofs in Agda (Part 2): Agda in a nutshell<\/a>. ~ Danya Rogozin. #ITP #Agda #Logic<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/2018\/11\/30\/playing-with-negation\">Constructive and non-constructive proofs in Agda (Part 3): Playing with negation<\/a>. ~ Danya Rogozin #ITP #Agda #Logic<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2018-12-14-primes-in-agda.html\">Prime sieves in Agda<\/a>. ~ Donnacha Ois\u00edn Kidney. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/2018\/11\/05\/signal-processing\">Signal processing in Haskell<\/a>. ~ Rinat Stryungis. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2018-12-18-traversing-graphs.html\">Pure &amp; lazy breadth-first traversals of graphs in Haskell<\/a>. ~ Donnacha Ois\u00edn Kidney. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2018\/10\/22\/purescript-ii-typeclasses-and-monads\">Purescript II: Typeclasses and Monads<\/a>. ~ James Bowen. #Purescript #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2018\/10\/29\/purescript-iii-web-pages-with-react\">Purescript III: Making a Web Page with Purescript and React!<\/a> ~ James Bowen. #Purescript #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2018\/11\/5\/purescript-iv-building-a-bridge\">Purescript IV: Routing and navigation!<\/a> ~ James Bowen. #Purescript #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/link.springer.com\/article\/10.1007\/s10817-012-9260-7\">Proof pearl: A mechanized proof of GHC\u2019s mergesort<\/a>. ~ C. Sternagel. #ITP #IsabelleHOL #Haskell #Algorithms<\/li>\n<li><a href=\"https:\/\/cvlad.info\/clasical-logic-in-haskell\">Classical logic in Haskell<\/a>. ~ Vladimir Ciobanu. #Haskell #FunctionalProgramming #Logic<\/li>\n<li><a href=\"http:\/\/www.cs.umd.edu\/~rrand\/thesis.pdf\">Formally verified quantum programming<\/a>. ~ R. Rand. #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2018-12-21-balancing-scans.html\">Balancing scans<\/a>. ~ Donnacha Ois\u00edn Kidney. #Haskell #Agda<\/li>\n<li><a href=\"https:\/\/bartoszmilewski.com\/2018\/12\/20\/open-season-on-hylomorphisms\">Open season on hylomorphisms<\/a>. ~ B. Milewski. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/probcomp\/metaprob\">Metaprob: A language for probabilistic programming and metaprogramming, embedded in Clojure<\/a>. #Clojure #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/hackernoon.com\/clojure-functional-programming-38cc6a9298f5\">Clojure &amp; functional programming<\/a>. ~ @leandrotk_ #Clojure #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.gaussianos.com\/el-yin-yang-y-el-numero-aureo\">El yin-yang y el n\u00famero \u00e1ureo<\/a>. ~ M.A. Morales. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/brianmckenna.org\/blog\/higher_kinded_parametricity\">Higher kinded parametricity<\/a>. ~ Brian McKenna. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www21.in.tum.de\/~eberlm\/linrec.pdf\">Verified solving and asymptotics of linear recurrences<\/a>. ~ M. Eberl. #ITP #IsabelleHOL #Math #Algorithmic<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-01962912\/document\">Verifying a security hypervisor model by infinite symbolic execution and invariant strengthening<\/a>. ~ V. Rusu, G. Grimaud, M. Hauspie. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/images.math.cnrs.fr\/Decomposer-et-iterer-pour-resoudre-un-probleme.html\">D\u00e9composer et it\u00e9rer pour r\u00e9soudre un probl\u00e8me<\/a>. ~ G. Legendre, J. Salomon. #Algorithms #Math<\/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>. ~ @acid2 #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/alhassy.github.io\/PathCat\">Graphs are to categories as lists are to monoids<\/a>. ~ Musa Al-hassy. #CategoryTheory #Agda #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/alhassy\/CatsCheatSheet\">A listing of common theorems in elementary category theory<\/a>. ~ Musa Al-hassy. #CategoryTheory #Agda<\/li>\n<li><a href=\"https:\/\/github.com\/alhassy\/CoqCheatSheet\">Reference sheet for the Coq language<\/a>. ~ Musa Al-hassy. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/alhassy.github.io\/literate\/\">Literate Agda with Org-mode<\/a>. ~ Musa Al-hassy. #ITP #Agda #Emacs #OrgMode<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/thiemann\/paper\/LPAR18_LLL.pdf\">A verified efficient implementation of the LLL basis reduction algorithm<\/a>. ~ R. Bottesch, M.W. Haslbeck, R. Thiemann. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/compiling-to-categories-3-a-bit-cuter\">Compiling to categories 3: A bit cuter<\/a>. ~ Philip Zucker. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/bit.ly\/2RjX3x1\">Essential logic for computer science<\/a>. ~ R. Page, R. Gamboa. #Logic #ITP #ACL2<\/li>\n<li><a href=\"https:\/\/dodisturb.me\/posts\/2018-12-25-The-Essence-of-Datalog.html\">The essence of Datalog<\/a>. #Haskell #FunctionalProgramming #LogicProgramming<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/Jerzy_Karczmarczuk\/publication\/2437746_Functional_Programming_and_Mathematical_Objects\/links\/549467c80cf29b94481ea108.pdf\">Functional programming and mathematical objects<\/a>. ~ J. Karczmarczuk. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/nextjournal.com\/zampino\/latte-cantor\">Proving Cantor&#8217;s theorem in Clojure using LaTTe<\/a>. ~ Andrea Amantini. #ITP #LaTTe #Clojure<\/li>\n<li><a href=\"http:\/\/math.ucr.edu\/home\/baez\/books.html\">How to learn Math and Physics<\/a>. ~ John Carlos Baez. #Math #Physics<\/li>\n<li><a href=\"http:\/\/www3.risc.jku.at\/publications\/download\/risc_5814\/Paper.pdf\">Gr\u00f6bner bases and Macaulay matrices in Isabelle\/HOL<\/a>. ~ A. Maletzky. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/www3.risc.jku.at\/publications\/download\/risc_5815\/Paper.pdf\">A generic and executable formalization of signature-based Gr\u00f6bner basis algorithms<\/a>. A. Maletzky. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/algorithms.wtf\">Algorithms<\/a>. ~ Jeff Erickson. #eBook #Algorithms<\/li>\n<li><a href=\"http:\/\/mfleck.cs.illinois.edu\/building-blocks\">Building blocks for theoretical computer science<\/a>. ~ M.M. Fleck. #eBook #CompSci<\/li>\n<li><a href=\"http:\/\/opendatastructures.org\">Open data structures (An open content textbook)<\/a>. P. Morin. #eBook #Algorithms #CompSci<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1812.11108\">Towards a constructive formalization of Perfect Graph Theorems<\/a>. ~ A.K. Singh, R. Natarajan. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/friguzzi\/aleph\">Port of Aleph (an Inductive Logic Programming system) to SWI-Prolog<\/a>. ~ Fabrizio Riguzzi. #ILP #Prolog<\/li>\n<li><a href=\"https:\/\/www.johndcook.com\/blog\/2018\/12\/30\/groups-2019\/\">Groups of order 2019<\/a>. ~ John D. Cook. #Math #Python<\/li>\n<li><a href=\"http:\/\/hojaynumeros.blogspot.com\/2018\/12\/resumen-de-calculos-sobre-el-ano-2019.html\">Resumen de c\u00e1lculos sobre el a\u00f1o 2019<\/a>. ~ Antonio Rold\u00e1n. #Matem\u00e1ticas<\/li>\n<li><a href=\"http:\/\/yoda.guillaume.pagesperso-orange.fr\/N1000\/N2019.htm\">Nombre 2019, deux-mille-dix-neuf<\/a>. ~ G\u00e9rard Villemin. #Maths<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2018\/12\/30\/learning-lean-by-example\">Learning Lean by example<\/a>. ~ Kevin Buzzard. #ITP #LeanTheoremProver #Math<\/li>\n<\/ul>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante diciembre de 2018, 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\/6719"}],"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=6719"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6719\/revisions"}],"predecessor-version":[{"id":6720,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6719\/revisions\/6720"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6719"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6719"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6719"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}