{"id":7065,"date":"2020-03-01T10:20:25","date_gmt":"2020-03-01T09:20:25","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7065"},"modified":"2020-03-01T10:20:25","modified_gmt":"2020-03-01T09:20:25","slug":"resumen-de-lecturas-compartidas-del-22-al-29-de-febrero-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-del-22-al-29-de-febrero-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas del 22 al 29 de febrero de 2020"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, del 22 al 29 de febrero, 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>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<div id=\"outline-container-org31bda14\" class=\"outline-2\">\n<h2 id=\"org31bda14\"><span class=\"section-number-2\">1<\/span> DAO: Demostraci\u00f3n asistida por ordenador<\/h2>\n<div id=\"text-1\" class=\"outline-text-2\"><\/div>\n<div id=\"outline-container-org945c470\" class=\"outline-3\">\n<h3 id=\"org945c470\"><span class=\"section-number-3\">1.1<\/span> DAO con Agda<\/h3>\n<div id=\"text-1-1\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/arxiv.org\/abs\/2002.06047\">Flexible coinduction in Agda<\/a>. ~ Luca Ciccone. #MSc_Thesis #ITP #Agda<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2002.07079\">The Cantor-Schr\u00f6der-Bernstein Theorem for \u221e-groupoids<\/a>. ~ Mart\u0131\u0301n Escard\u00f3. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/github.com\/jonaprieto\/agda-metis\">agda-metis: Metis prover reasoning for propositional logic in Agda<\/a>. ~ Jonathan Prieto-Cubides. #ITP #Agda #Metis<\/li>\n<li><a href=\"https:\/\/github.com\/jonaprieto\/agda-prop\">agda-prop: A library for classical propositional logic in Agda<\/a>. ~ Jonathan Prieto-Cubides. #ITP #Agda #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/jonaprieto\/athena\">Athena: a tool that translates Metis ATP proofs to the Agda programming language to check their correctness<\/a>. ~ Jonathan Prieto-Cubides. #Haskell #ITP #Agda #Metis #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/martinescardo\/TypeTopology\/\">Various new theorems in constructive univalent mathematics written in Agda<\/a>. ~ Mart\u00edn Escard\u00f3. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/raw.githubusercontent.com\/jonaprieto\/athena\/master\/pubs\/paper\/paper.pdf\">Proof-reconstruction in type theory for propositional logic<\/a>. ~ Jonathan Prieto-Cubides, Andr\u00e9s Sicard-Ram\u00edrez. #ITP #Agda #Metis #Logic<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org9b72cdb\" class=\"outline-3\">\n<h3 id=\"org9b72cdb\"><span class=\"section-number-3\">1.2<\/span> DAO con Coq<\/h3>\n<div id=\"text-1-2\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/people.rennes.inria.fr\/Assia.Mahboubi\/\/vu.html\">Course: Machine-checked Mathematics<\/a>. ~ Assia Mahboubi. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02086931\/document\">Short proof of Menger&#8217;s theorem in Coq (Proof Pearl)<\/a>. ~ Christian Doczka. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02316859v2\/document\">Graph theory in Coq: Minors, treewidth, and isomorphisms<\/a>. ~ Christian Doczkal and Damien Pous. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02333553v3\/document\">Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq<\/a>. ~ Christian Doczkal, and Damien Pous. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/kwarc.info\/people\/frabe\/Research\/KR_oafexp_20.pdf\">Experiences from exporting major proof assistant libraries<\/a>. ~ Michael Kohlhase, and Florian Rabe. #ITP #Coq #HOL_Light #IsabelleHOL #Mizar #PVS #MMT<\/li>\n<li><a href=\"https:\/\/www.comp.nus.edu.sg\/~hobor\/Publications\/2020\/CertifiedDijkstra.pdf\">A machine-checked C implementation of Dijkstra\u2019s shortest path algorithm<\/a>. ~ Anshuman Mohan, Shengyi Wang, and Aquinas Hobor. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.hindawi.com\/journals\/wcmc\/2020\/7346763\/\">Formal verification of hardware components in critical systems<\/a>. ~ Wilayat Khan et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/Publications\/details\/Doczkal:2016:PhDThesis.html\">A machine-checked constructive metatheory of computation tree logic<\/a>. ~ Christian Doczkal (2016). #PhD_Thesis #ITP #Coq #Logic<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org9a6de01\" class=\"outline-3\">\n<h3 id=\"org9a6de01\"><span class=\"section-number-3\">1.3<\/span> DAO con HOL4<\/h3>\n<div id=\"text-1-3\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/arxiv.org\/abs\/2002.10212\">A mechanised semantics for HOL with ad-hoc overloading<\/a>. ~ Johannes \u00c5man Pohjola, Arve Gengelbach. #ITP #HOL4<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgbfdc983\" class=\"outline-3\">\n<h3 id=\"orgbfdc983\"><span class=\"section-number-3\">1.4<\/span> DAO con Isabelle\/HOL<\/h3>\n<div id=\"text-1-4\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?ThEdu19.5\">Teaching a formalized logical calculus<\/a>. ~ Asta Halkj\u00e6r From et als. #Logic #Teaching #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2002.09282\">Isabelle\/Spartan: A dependent type theory framework for Isabelle<\/a>. ~ Joshua Chen. #ITP #IsabellleHOL #HoTT<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Goodstein_Lambda.html\">Implementing the Goodstein function in \u03bb-calculus<\/a>. ~ Bertram Felgenhauer. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/VeriComp.html\">A generic framework for verified compilers in Isabelle\/HOL<\/a>. ~ Martin Desharnais. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.research-collection.ethz.ch\/bitstream\/handle\/20.500.11850\/400029\/2\/phdthesis-acreto-online.pdf\">On memory addressing<\/a>. ~ Reto Achermann. #PhD_Thesis #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.ssrg.ece.vt.edu\/papers\/tacas20.pdf\">Highly automated formal proofs over memory usage of assembly code<\/a>. ~ Freek Verbeek et als. #ITP #IsabelleHOL<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgcf235ea\" class=\"outline-3\">\n<h3 id=\"orgcf235ea\"><span class=\"section-number-3\">1.5<\/span> DAO en general<\/h3>\n<div id=\"text-1-5\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/www-sop.inria.fr\/marelle\/personnel\/Laurent.Thery\/math.html\">A selected bibliography on formalised mathematics<\/a>. ~ Laurent Th\u00e9ry. #ITP #Math<\/li>\n<li><a href=\"https:\/\/new.kwarc.info\/people\/frabe\/Research\/rabe_mmtsys_20.pdf\">MMT: The Meta Meta Tool (system description)<\/a>. ~ Florian Rabe. #ITP #MMT<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgcc8cf98\" class=\"outline-2\">\n<h2 id=\"orgcc8cf98\"><span class=\"section-number-2\">2<\/span> Programaci\u00f3n declarativa<\/h2>\n<div id=\"text-2\" class=\"outline-text-2\"><\/div>\n<div id=\"outline-container-orgbd08bab\" class=\"outline-3\">\n<h3 id=\"orgbd08bab\"><span class=\"section-number-3\">2.1<\/span> Programaci\u00f3n funcional con Haskell<\/h3>\n<div id=\"text-2-1\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/blog.poisson.chat\/posts\/2020-02-24-quickcheck-higherorder.html\">Testing higher-order properties with QuickCheck<\/a>. ~ Li-yao Xia (@lysxia). #Haskell #FunctionalProgramming #QuickCheck<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2020-02-20-final-bft.html\">Another breadth-first traversal<\/a>. ~ Donnacha Ois\u00edn Kidney (@oisdk). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/essay.utwente.nl\/80680\/1\/Staal_BA_EEMCS.pdf\">An analysis of programming paradigms in high-level synthesis tools<\/a>. ~ Pieter Staal. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fenix.tecnico.ulisboa.pt\/downloadFile\/563568428791213\/or-????-separation.pdf\">Revisiting separation: Algorithms and complexity<\/a>. ~ Daniel Oliveira, and Jo\u00e3o Rasga. #Logic #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/drdo\/logic-translation\/raw\/master\/doc\/Thesis.pdf\">Linear temporal logic: separation and translation<\/a>. ~ Daniel Oliveira. #MSc_Thesis #Logic #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/drdo\/logic-translation\">Translation from FOL to LTL+Past and LTL, via separation of LTL+Past<\/a>. ~ Daniel Oliveira. #Logic #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/iohk.io\/en\/research\/library\/papers\/marloweimplementing-and-analysing-financial-contracts-on-blockchain\/\">Marlowe: implementing and analysing financial contracts on blockchain<\/a>. ~ Pablo Lamela Seijas et als. #Haskell #ITP #IsabelleHOL #Blockchain #Cardano<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2020-02-26-monad-bayes-3.html\">Probabilistic programming with monad\u2011bayes, Part 3: A bayesian neural network<\/a>. ~ Siddharth Bhat, Simeon Carstens, Matthias Meschede. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/JboZel47XU0\">Type-based formal verification<\/a>. ~ Alejandro Serrano (@trupill). #Haskell #Verification<\/li>\n<li><a href=\"https:\/\/youtu.be\/UwYLaGzhDb4\">Category theory as a tool for thought<\/a>. ~ Daniel Beskin. #CategoryTheory #FunctionalProgramming #Haskell<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org64b7568\" class=\"outline-3\">\n<h3 id=\"org64b7568\"><span class=\"section-number-3\">2.2<\/span> Programaci\u00f3n l\u00f3gica con Prolog<\/h3>\n<div id=\"text-2-2\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?ThEdu19.1\">Automating the generation of high school geometry proofs using Prolog in an educational context<\/a>. ~ Ludovic Font et als. #Prolog #LogicProgramming #Math<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-org27c7d03\" class=\"outline-2\">\n<h2 id=\"org27c7d03\"><span class=\"section-number-2\">3<\/span> L\u00f3gica<\/h2>\n<div id=\"text-3\" class=\"outline-text-2\">\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?ThEdu19.3\">A mobile application for self-guided study of formal reasoning<\/a>. ~ David M. Cerna, Rafael P.D. Kiesel, Alexandra Dzhiganskaya. #Logic #Teaching #Android<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?ThEdu19.4\">Tools in term rewriting for education<\/a>. ~ Sarah Winkler, Aart Middeldorp. #Logic #Teaching<\/li>\n<li><a href=\"https:\/\/github.com\/Alastair-Carr\/Natural-Deduction-Pack\/raw\/master\/Natural%20Deduction%20Pack.pdf\">The natural deduction pack<\/a>. ~ Alastair Carr. #Logic<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgcc0752d\" class=\"outline-2\">\n<h2 id=\"orgcc0752d\"><span class=\"section-number-2\">4<\/span> Otros<\/h2>\n<div id=\"text-4\" class=\"outline-text-2\">\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/math.chapman.edu\/~jipsen\/structures\/doku.php\/\">Mathematical structures<\/a>. ~ Contributors of math.chapman.edu. #Math<\/li>\n<li><a href=\"https:\/\/bartoszmilewski.com\/2020\/02\/24\/math-is-your-insurance-policy\/\">Math is your insurance policy<\/a>. ~ Bartosz Milewski (@BartoszMilewski). #Programming<\/li>\n<li><a href=\"https:\/\/rjlipton.wordpress.com\/2020\/02\/28\/reductions-and-jokes\/\">Reductions and jokes<\/a>. ~ R.J. Lipton &amp; K.W. Regan. #CompSci #Math<\/li>\n<li><a href=\"https:\/\/sicp.comp.nus.edu.sg\/\">Structure and interpretation of computer programs \u2014 JavaScript adaptation<\/a>. #eBook #JavaScript #SICP<\/li>\n<li><a href=\"https:\/\/www.math.utah.edu\/~cherk\/mathjokes.html\">Mathematical humor<\/a>. ~ Andrej and Elena Cherkaev. #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2002.04803\">Machine Learning in Python: Main developments and technology trends in data science, machine learning, and artificial intelligence<\/a>. ~ Sebastian Raschka, Joshua Patterson, Corey Nolet. #MachineLearning #AI #Python<\/li>\n<li><a href=\"https:\/\/github.com\/jrjohansson\/scientific-python-lectures\">Lectures on scientific computing with Python<\/a>. ~ Robert Johansson (2017). #Python<\/li>\n<\/ul>\n<\/div>\n<\/div>\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, del 22 al 29 de febrero, en Twitter fundamentalmente sobre programaci\u00f3n funcional y demostraci\u00f3n asistida por ordenador. Al final de cada art\u00edculo se encuentran etiquetas relativas a los sistemas que usa o a su contenido. Una recopilaci\u00f3n de todas las lecturas compartidas se encuentra en GitHub.<\/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":[177],"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\/7065"}],"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=7065"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7065\/revisions"}],"predecessor-version":[{"id":7066,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7065\/revisions\/7066"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7065"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7065"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7065"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}