{"id":6916,"date":"2019-11-01T07:05:44","date_gmt":"2019-11-01T06:05:44","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6916"},"modified":"2020-01-07T07:07:29","modified_gmt":"2020-01-07T06:07:29","slug":"resumen-de-lecturas-compartidas-durante-octubre-de-2019","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-octubre-de-2019\/","title":{"rendered":"Resumen de lecturas compartidas durante octubre de 2019"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante octubre 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>.<\/p>\n<p><!--more--><\/p>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/xavierleroy.org\/courses\/EUTypes-2019\">Proving the correctness of a compiler<\/a>. ~ Xavier Leroy. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/kbuzzard\/xena\">Lean Library currently studying for a degree at Imperial College<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/mullikine.github.io\/posts\/macro-tutorial\/\">Didactic emacs-lisp macro example (ie. a tutorial)<\/a>. ~ Shane Mulligan (@mullikine). #Emacs #Lisp<\/li>\n<li><a href=\"http:\/\/hackage.haskell.org\/package\/lens-tutorial-1.0.4\/docs\/Control-Lens-Tutorial.html\">Tutorial for the lens library.<\/a> #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/git.imp.fu-berlin.de\/leo-iii\/compmeta_pub\/raw\/master\/exercises\/resources\/Isabelle_ND_cheatsheet.pdf\">Mapping of ND proof templates to Isabelle formalization<\/a>. ~ A. Steen. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/umazalakain.info\/static\/thesis.pdf\">Type-checking session-typed \u03c0-calculus with Coq<\/a>. ~ Uma Zalakain. #MSc_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/gist.github.com\/AndrasKovacs\/1f57b66108e7d61351d3a61a642ef066\">Constructing finitary inductive types from natural numbers<\/a>. ~ Andras Kovacs (@andrasKovacs6). #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/www.cs.toronto.edu\/~hector\/pcr.pdf\">Programming cognitive robots<\/a>. ~ Hector J. Levesque. #eBook #AI #DeclarativeProgramming #Schem #Racket<\/li>\n<li><a href=\"https:\/\/prologhub.pl\/homoiconic-prolog-explain-yourself\/\">Homoiconic Prolog: Explain yourself!<\/a> ~ Paul Brown. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2019-10-02-what-is-good-about-haskell.html\">What is good about Haskell?<\/a> ~ Donnacha Ois\u00edn Kidney (@oisdk). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/winitzki\/sofp\/raw\/master\/sofp-src\/sofp.pdf\">The science of functional programming (A tutorial, with examples in Scala)<\/a>. ~ Sergei Winitzki. #eBook #FunctionalProgramming #Scala<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/335106273_Computer_Science_and_Metaphysics_A_Cross-Fertilization\">Computer science and metaphysics: A cross-fertilization<\/a>. ~ Christoph Benzm\u00fcller et als. #ITP #Isabelle-HOL<\/li>\n<li><a href=\"https:\/\/dodisturb.me\/posts\/2019-10-03-Verifying-the-Titular-Properties-of-a-Leftist-Heap.html\">Verifying the titular properties of a leftist heap<\/a>. ~ Mistral Contrastin (@madgen_). #Haskell #FunctionalProgramming #Algorithms<\/li>\n<li><a href=\"https:\/\/www.andrew.cmu.edu\/user\/avigad\/Papers\/learning_logic_and_proof.pdf\">Learning logic and proof with an interactive theorem prover<\/a>. ~ J. Avigad. #ITP #LeanProver #Logic<\/li>\n<li><a href=\"http:\/\/bit.ly\/2oTPtwA\">Proof technology in mathematics research and teaching<\/a>. #eBook #ATP #ITP #Math<\/li>\n<li><a href=\"https:\/\/www.repository.cam.ac.uk\/bitstream\/handle\/1810\/280564\/SchematicProof.pdf?sequence=1&amp;isAllowed=y\">A common type of rigorous proof that resists Hilbert\u2019s programme<\/a>. ~ A. Bundy, M.A. Jamnik. #Logic #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1909.09137\">Bayesian optimisation with Gaussian processes for premise selection<\/a>. ~ Agnieszka S\u0142owik et als. #ATP #Vampire #MachineLearning<\/li>\n<li><a href=\"https:\/\/williamyaoh.com\/posts\/2019-10-05-you-are-already-smart-enough.html\">You are already smart enough to write Haskell<\/a>. ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-01912885\/document\">Didactical issues at the interface of mathematics and computer science<\/a>. ~ V. Durand-Guerrier, A. Meyer, S. Modeste. #Math #ComSci<\/li>\n<li><a href=\"https:\/\/www.geeksforgeeks.org\/10-famous-bugs-in-the-computer-science-world\">10 famous bugs in the computer science world<\/a>. #CompSci #Programming<\/li>\n<li><a href=\"https:\/\/dkalemis.wordpress.com\/2013\/11\/23\/the-correspondence-between-monads-in-category-theory-and-monads-in-haskell\">The correspondence between monads in category theory and monads in Haskell<\/a>. ~ D. Kalemis (@dkalemis). #Haskell #FunctionalProgramming #CategoryTheory<\/li>\n<li><a href=\"https:\/\/github.com\/alhassy\/AgdaCheatSheet\">AgdaCheatSheet: Basics of the dependently-typed functional language Agda<\/a>. ~ Musa Al-hassy. #ITP #Agda<\/li>\n<li><a href=\"http:\/\/matryoshka.gforge.inria.fr\/pubs\/fischer_msc_thesis.pdf\">Verification of GPU program optimizations in Lean<\/a>. ~ B. Fischer. #MSc_Thesis #ITP #LeanProver<\/li>\n<li><a href=\"http:\/\/bit.ly\/30SLltT\">A promising path towards autoformalization and general Artificial Intelligence<\/a>. ~ Christian Szegedy. #AI #PLN #ITP<\/li>\n<li><a href=\"https:\/\/homes.cs.washington.edu\/~thickstn\/docs\/lean.pdf\">Number theory in a proof assistant<\/a>. ~ John Thickstun. #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/prl.korea.ac.kr\/~pronto\/home\/papers\/oopsla19.pdf\">Automatic and scalable detection of logical errors in functional programming assignments<\/a>. ~ Dowon Song et als. #OCaml #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/link.springer.com\/article\/10.1007\/s10817-019-09534-y\">An assertional proof of red\u2013black trees using Dafny<\/a>. ~ Ricardo Pe\u00f1a. #Dafny<\/li>\n<li><a href=\"https:\/\/www.cl.cam.ac.uk\/~jrh13\/spisa19\/paper_10.pdf\">GRIFT: A richly-typed, deeply-embedded RISC-V semantics written in Haskell<\/a>. ~ Benjamin Selfridge. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=226\">NetLogo: Grafos<\/a>. F. Sancho (@sanchocaparrini). #NetLogo<\/li>\n<li><a href=\"https:\/\/ahmet-celik.github.io\/papers\/CELIK-DISSERTATION-2019.pdf\">Proof engineering for large-scale verification projects<\/a>. ~ Ahmet Celik. #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2019-10-11-ormolu-first-release.html\">Ormolu: a formatter for Haskell source code<\/a>. ~ Mark Karpov, Utku Demir. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007%2F978-3-319-91908-9_15.pdf\">The next 7000 programming languages<\/a>. ~ Robert Chatley, Alastair Donaldson, and Alan Mycroft. #Programming<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/with-category-theory-mathematics-escapes-from-equality-20191010\/\">With category theory, mathematics escapes from equality<\/a>. ~ Kevin Hartnett. #Math #CategoryTheory<\/li>\n<li><a href=\"ftp:\/\/ftp.cs.princeton.edu\/techreports\/2019\/011.pdf\">Verified extraction for Coq<\/a>. ~ Olivier Savary B\u00e9langer. #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"http:\/\/casperbp.net\/store\/from-definitional-interpreter-to-symbolic-executor.pdf\">From definitional interpreter to symbolic executor<\/a>. ~ Adrian D. Mensing et als. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2019\/10\/12\/competitive-programming-in-haskell-reading-large-inputs-with-bytestring\/\">Competitive programming in Haskell: reading large inputs with ByteString<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/maslinux.es\/openlibra-un-enorme-banco-de-libros-con-licencia-libre\/\">OpenLibra: Un enorme banco de libros con licencia libre<\/a>. #OpenLibra<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=228\">Planificaci\u00f3n: Fundamentos (y NetLogo)<\/a>. ~ Fernando Sancho (@sanchocaparrini). #IA #NetLogo<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1903.03425\">The ethics of AI ethics (An evaluation of guidelines)<\/a>. ~ Thilo Hagendorff. #AI<\/li>\n<li><a href=\"http:\/\/neilmitchell.blogspot.com\/2019\/10\/monads-as-graphs.html\">Monads as graphs<\/a>. ~ Neil Mitchell. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/prologhub.pl\/prolog-forwards-and-backwards\/\">Prolog: forwards and backwards<\/a>. ~ Paul Brown. #Prolog #LogicProgramming<\/li>\n<li><a href=\"http:\/\/prologhub.pl\/hello-tau-prolog\/\">Hello, Tau Prolog!<\/a> ~ Paul Brown. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/papers\/mathlib-paper.pdf\">The Lean mathematical library<\/a>. ~ The mathlib Community. #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/functors-and-vectors\/\">Functors, vectors, and quantum circuits<\/a>. ~ Philip Zucker (@SandMouth). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1910.03740\">The resolution of Keller&#8217;s conjecture<\/a>. ~ J. Brakensiek, M. Heule, J. Mackey. #ATP #SAT #Math via @ozanerdem<\/li>\n<li><a href=\"https:\/\/blog.sigplan.org\/2019\/10\/14\/how-to-design-co-programs\/\">How to design co-programs<\/a>. ~ Jeremy Gibbons. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Clean.html\">Clean: An abstract imperative programming language and its theory<\/a>. ~ F. Tuong, B. Wolff. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Aristotles_Assertoric_Syllogistic.html\">Aristotle&#8217;s assertoric syllogistic in Isabelle\/HOL<\/a>. ~ Angeliki Koutsoukou-Argyraki (@AngelikiKoutso1). #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/chrispenner.ca\/posts\/wc\">Beating C with 80 lines of Haskell: wc<\/a>. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/jaspervdj.be\/posts\/2019-10-15-flip-partial-application.html\">Partial application using flip<\/a>. ~ Jasper Van der Jeugt (@jaspervdj). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/ruc.udc.es\/dspace\/handle\/2183\/24095\">Un procesador de expresiones epist\u00e9micas en programas l\u00f3gicos<\/a>. ~ Javier Garea Cidre. #TFG #LogicProgramming #ASP<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Sigma_Commit_Crypto.html\">Sigma protocols and commitment schemes<\/a>. ~ David Butler, Andreas Lochbihler. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/blog.sigplan.org\/2019\/10\/17\/what-type-soundness-theorem-do-you-really-want-to-prove\/\">What type soundness theorem do you really want to prove?<\/a> ~ Derek Dreyer et als. #CompSci #TypeTheory<\/li>\n<li><a href=\"http:\/\/neilmitchell.blogspot.com\/2019\/10\/improving-rebindable-syntax.html\">Improving rebindable syntax<\/a>. ~ Neil Mitchell. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.slideshare.net\/paulszulc\/painless-haskell\">Painless Haskell<\/a>. ~ Pawe\u0142 Szulc (@rabbitonweb). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/blog\/the-inner-magic-behind-the-z3-theorem-prover\/\">The inner magic behind the Z3 theorem prover<\/a>. ~ Nikolaj Bj\u00f8rner, Leonardo de Moura. #ATP #SMT #Z3<\/li>\n<li><a href=\"http:\/\/math.jhu.edu\/~eriehl\/lambda.pdf\">A categorical view of computational effects<\/a>. ~ Emily Riehl (@emilyriehl). #CategoryTheory #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.slideshare.net\/lauramcastro\/so-i-used-erlang-is-my-system-as-scalable-as-they-say-itd-be\">So I used Erlang \u2026 is my system as scalable as they say it&#8217;d be?<\/a> ~ Laura M. Castro (@lauramcastro). #Erlang #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arosien.github.io\/talks\/better-testing\">Writing programs that write tests: better testing with Scala<\/a>. ~ Adam Rosien (@arosien). #Scala #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/top-software-written-in-haskell\">Software written in Haskell: Stories of success<\/a>. ~ Yulia Gavrilova, Gints Dreimanis. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mml-book.github.io\/book\/mml-book.pdf\">Mathematics for machine learning<\/a>. ~ Marc Peter Deisenroth, A Aldo Faisal, Cheng Soon Ong. #eBook #MachineLearning #Math<\/li>\n<li><a href=\"https:\/\/github.com\/haroldcarr\/presentations\/raw\/master\/2019-10-18-lambda-world-cadiz-recursion-schemes.pdf\">Refactoring recursion<\/a>. ~ Harold Carr (@haroldcarr). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/marcosh.github.io\/presentations\/2019\/10\/18\/fun-with-categories.html\">Fun with categories<\/a>. ~ Marco Perone (@marcoshuttle). #CategoryTheory #Idris #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/wwwf.imperial.ac.uk\/~buzzard\/docs\/lean\/sandwich.html\">The sandwich theorem<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.cs.umd.edu\/~mwh\/papers\/hietala19voqc.html\">A verified optimizer for quantum circuits<\/a>. ~ Kesha Hietala et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/ucsd-progsys.github.io\/liquidhaskell-blog\/2019\/10\/20\/why-types.lhs\/\">Liquid types vs. Floyd-Hoare logic<\/a>. ~ Ranjit Jhala (@RanjitJhala). #LiquidHaskell #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/kaygun.tumblr.com\/post\/183562822804\/pr%C3%BCfer-encodingdecoding-of-a-tree-in-common-lisp\">Pr\u00fcfer encoding\/decoding of a tree in Common Lisp<\/a>. ~ Atabey Kaygun (@Atabey_Kaygun). #CommonLisp #Algorithms<\/li>\n<li><a href=\"http:\/\/www.cs.cmu.edu\/~mheule\/15816-f19\/schedule.html\">Course: Advanced topics in logic (Automated reasoning and satisfiability)<\/a>. ~ Marijn Heule and Ruben Martins. #ATP #SAT<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1910.08416\">Programming and symbolic computation in Maude<\/a>. ~ F. Dur\u00e1n et als. #ITP #Maude<\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/papers\/mathlib-paper.pdf\">The Lean mathematical library<\/a>. ~ The mathlib Community. #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?LFMTP2019.5\">Rapid prototyping formal systems in MMT: 5 case studies<\/a>. ~ Dennis M\u00fcller, and Florian Rabe. #ITP #MMT #Logic<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?LFMTP2019.6\">A weakly initial algebra for higher-order abstract syntax in Cedille<\/a>. ~ Aaron Stump. #ITP #Cedille<\/li>\n<li><a href=\"https:\/\/dev.to\/drbearhands\/haskell-for-madmen-setup-4cj9\">Haskell for madmen: Setup<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dev.to\/drbearhands\/haskell-for-madmen-hello-monad-3926\">Haskell for madmen: Hello, monad!<\/a> #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/albohlabs\/awesome-haskell\">A curated list of amazingly awesome Haskell articles and talks for beginners<\/a>. ~ Daniel Pfefferkorn (@albohlabs). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/kensanata\/ggg\/\">Gmail Gnus GPG Guide (GGGG)<\/a>. ~ Alex Schroeder. #Emacs #Gmail #Gnus #GPG<\/li>\n<li><a href=\"https:\/\/github.com\/blanchette\/logical_verification_2019\/raw\/master\/logical_verification_in_lean.pdf\">Logical verification in Lean<\/a>. ~ A. Bentkamp, J. Blanchette, J. H\u00f6lzl. #eBook #ITP #LeanProver #Logic #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/podcasts.apple.com\/se\/podcast\/337-provable-security-podcast-series-episode-2-automated\/id1122785133?i=1000453779171&amp;l=en\">Automated Reasoning in the Cloud with John Harrison<\/a>. #ATP<\/li>\n<li><a href=\"http:\/\/www.lix.polytechnique.fr\/~dale\/papers\/icdcit-2019.pdf\">A distributed and trusted web of formal proofs<\/a>. ~ Dale Miller. #Logic #ITP #ATP<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02317118\/document\">A first step in the translation of Alloy to Coq<\/a>. ~ Salwa Souaf, Fr\u00e9d\u00e9ric Loulergue. #ITP #Coq #Alloy<\/li>\n<li><a href=\"http:\/\/chalkdustmagazine.com\/features\/can-computers-prove-theorems\/\">Can computers prove theorems?<\/a> ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.cs.vu.nl\/~jbe248\/lv2017\/notes.pdf\">Logical verification (Course notes)<\/a>. ~ F. van Raamsdonk. #eBook #ITP #Coq #Logic<\/li>\n<li><a href=\"https:\/\/medium.com\/@cdsmithus\/applicative-without-currying-f4c3bd9f1552\">Applicative without currying<\/a>. ~ Chris Smith (@cdsmithus). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/iohk.io\/en\/research\/library\/papers\/system-f-in-agdafor-fun-and-profit\/\">System F in Agda, for fun and profit<\/a>. ~ J. Chapman, R. Kireev, C. Nester, P. Wadler. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/eprint.iacr.org\/2019\/1185.pdf\">Formalising \u03a3-protocols and commitment schemes using CryptHOL<\/a>. ~ D. Butler, A. Lochbihler, D. Aspinall, A. Gasc\u00f3n. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/VerifyThis2019.html\">VerifyThis 2019 (Polished Isabelle solutions)<\/a>. ~ P. Lammich, S. Wimmer. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www21.in.tum.de\/teaching\/fpv\/WS1920\/slides.pdf\">Functional programming and verification<\/a>. ~ T. Nipkow. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/magazines\/2019\/11\/240390-deepxplore\/fulltext\">DeepXplore: Automated whitebox testing of deep learning systems<\/a>. ~ K. Pei, Y. Cao, J. Yang, S. Jana. #DeepLearning<\/li>\n<li><a href=\"https:\/\/engineering.fb.com\/security\/simon-marlow\/\">Simon Marlow, Simon Peyton Jones, and Satnam Singh win Most Influential ICFP Paper Award<\/a>. #Hsakell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2019\/10\/24\/chalkdust-and-the-natural-number-game\/\">Chalkdust, and the natural number game!<\/a> ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.mi.fu-berlin.de\/inf\/groups\/ag-ki\/publications\/Aqvists-Logic\/Aqvist-farjami.pdf\">\u00c5qvist&#8217;s dyadic deontic logic E in HOL<\/a>. ~ C. Benzm\u00fcller, A. Farjami, X. Parent. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1904.03917\">Fifty years of Hoare&#8217;s Logic<\/a>. K.R. Apt, E.R. Olderog. #Logic #Verification #CompSci<\/li>\n<li><a href=\"http:\/\/lisp-univ-etc.blogspot.com\/2019\/10\/programming-algorithms-graphs.html\">Programming algorithms: Graphs<\/a>. ~ Vsevolod Dyomkin. #CommonLisp #Algorithms<\/li>\n<li><a href=\"https:\/\/blog.poisson.chat\/posts\/2019-10-25-infinite-types-existential-newtype.html\">Infinite types and existential newtypes<\/a>. ~ Li-yao Xia. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.newton.ac.uk\/seminar\/20170710143015301\">Proof assistants: from symbolic logic to real mathematics?<\/a> ~ Lawrence C Paulson #ITP #Logic #Math<\/li>\n<li><a href=\"https:\/\/en.wikipedia.org\/wiki\/List_of_software_bugs\">List of software bugs<\/a>. ~ Wikipedia #Programming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1910.11797\">Deep reinforcement learning in HOL4<\/a>. ~ T. Gauthier #ITP #HOL4 #DeepLearning<\/li>\n<li><a href=\"https:\/\/www.cl.cam.ac.uk\/~jrh13\/papers\/cacm.pdf\">Formally verified Mathematics<\/a>. ~ J. Avigad, J. Harrison. #ITP #Math<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-00809448\/document\">Les assistants de preuve, ou comment avoir confiance en ses d\u00e9monstrations<\/a>. ~ J. Narboux. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.reddit.com\/r\/math\/comments\/dnc0jj\/imo_grand_challenge_automated_problem_solving\/\">IMO Grand Challenge (Automated problem solving)<\/a>. #ITP #Math #IMO<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1910.10703\">Metamath Zero: The cartesian theorem prover<\/a>. ~ M. Carneiro #ITP #MetamathZero<\/li>\n<li><a href=\"http:\/\/jeff560.tripod.com\/set.html\">Earliest uses of symbols of set theory and logic<\/a>. ~ J. Miller #Logic #Math<\/li>\n<li><a href=\"https:\/\/openreview.net\/pdf?id=rJxd7vsWPS\">Dex: array programming with typed indices<\/a>. ~ D. Maclaurin et als #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/google-research\/dex-lang\">Dex: a research language for array processing in the Haskell\/ML family<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/bit.ly\/2hp4IUz\">The Zen of Haskell<\/a>. ~ #Haskell<\/li>\n<li><a href=\"https:\/\/notxor.nueva-actitud.org\/blog\/2019\/06\/30\/gestionar-bibliografia-con-emacs\/\">Gestionar bibliograf\u00eda con Emacs<\/a>. #Emacs<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1910.12320\">Formalising perfectoid spaces<\/a>. ~ K. Buzzard, J. Commelin, P. Massot. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/blog.poisson.chat\/posts\/2019-10-26-reasonable-continuations.html\">The reasonable effectiveness of the continuation monad<\/a>. ~ Li-yao Xia. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.poisson.chat\/posts\/2019-10-27-continuation-submonads.html\">A monad is just a submonad of the continuation monad, what&#8217;s the problem?<\/a> ~ Li-yao Xia. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/336838722_Computer-supported_Exploration_of_a_Categorical_Axiomatization_of_Modeloids\">Computer-supported exploration of a categorical axiomatization of modeloids<\/a>. ~ L. Tiemens, D.S. Scott, C. Benzm\u00fcller, M. Benda. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02333553v1\/document\">Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq<\/a>. ~ C. Doczkal, D. Pous. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/tel-02333396\/file\/thesis.pdf\">Formalisation tools for classical analysis (A case study in control theory)<\/a>. ~ D. Rouhling. #PhD_Thesis #ITP Coq #Math<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02086931\/document\">Short proof of Menger\u2019s Theorem in Coq (Proof Pearl)<\/a>. ~ C. Doczkal. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.microsiervos.com\/archivo\/internet\/wayback-machine-conservar-paginas-enlaces-outlinks.html\">La Wayback Machine ahora permite conservar p\u00e1ginas de forma fiable junto con todas las p\u00e1ginas a las que enlazan<\/a>. ~ @Alvy. #Internet<\/li>\n<li><a href=\"https:\/\/www.johndcook.com\/blog\/2019\/10\/29\/computing-pi-with-bc\/\">Computing pi with bc<\/a>. ~ John D. Cook. #Math #CompSci<\/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 octubre 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\/6916"}],"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=6916"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6916\/revisions"}],"predecessor-version":[{"id":6917,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6916\/revisions\/6917"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6916"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6916"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6916"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}