{"id":6952,"date":"2020-01-25T09:09:20","date_gmt":"2020-01-25T08:09:20","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6952"},"modified":"2020-01-25T09:09:20","modified_gmt":"2020-01-25T08:09:20","slug":"resumen-de-lecturas-compartidas-del-19-al-24-de-enero-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-del-19-al-24-de-enero-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas del 19 al 24 de enero de 2020"},"content":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, del 19 al 24 de enero, 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-orgc496838\" class=\"outline-2\">\n<h2 id=\"orgc496838\"><span class=\"section-number-2\">1<\/span> Programaci\u00f3n declarativa<\/h2>\n<div id=\"text-1\" class=\"outline-text-2\"><\/div>\n<div id=\"outline-container-org01e58f6\" class=\"outline-3\">\n<h3 id=\"org01e58f6\"><span class=\"section-number-3\">1.1<\/span> Programaci\u00f3n funcional con Haskell<\/h3>\n<div id=\"text-1-1\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/www.stephendiehl.com\/posts\/decade.html\">Haskell problems for a new decade<\/a>. ~ Stephen Diehl (@smdiehl). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/argumatronic.com\/posts\/1970-01-01-beginners.html\">For beginners<\/a>. ~ Julie Moronuki (@argumatronic). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.ploeh.dk\/2020\/01\/20\/algebraic-data-types-arent-numbers-on-steroids\/\">Algebraic data types aren&#8217;t numbers on steroids<\/a>. Mark Seemann (@ploeh). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cvlad.info\/profunctor\/\">The Functor family: Profunctor<\/a>. ~ Vladimir Ciobanu. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2020\/1\/20\/nicer-package-organization-with-stack\">Nicer package organization with Stack!<\/a> ~ James Bowen (@james_OWA). #Haskell #Stack<\/li>\n<li><a href=\"https:\/\/mutable.jle.im\/\">Beautiful mutable values<\/a>. ~ Justin Le (@mstk). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/typeclasses.com\/phrasebook\/folding-lists\">Folding lists<\/a>. ~ Chris Martin (@chris__martin), Julie Moronuki (@argumatronic). #Haskell #FunctionalProgramming<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org8dc3aa6\" class=\"outline-3\">\n<h3 id=\"org8dc3aa6\"><span class=\"section-number-3\">1.2<\/span> Programaci\u00f3n funcional con Lisp<\/h3>\n<div id=\"text-1-2\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/flownet.com\/gat\/jpl-lisp.html\">Lisping at JPL<\/a>. ~ Ron Garret. #Programming #CommonLisp<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org82690a3\" class=\"outline-3\">\n<h3 id=\"org82690a3\"><span class=\"section-number-3\">1.3<\/span> Programaci\u00f3n l\u00f3gica con Prolog<\/h3>\n<div id=\"text-1-3\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.08133\">Drawing Prolog search trees: A manual for teachers and students of logic programming<\/a>. ~ Johan Bos. #Prolog #LogicProgramming<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-org8b97d5e\" class=\"outline-2\">\n<h2 id=\"org8b97d5e\"><span class=\"section-number-2\">2<\/span> DAO: Demostraci\u00f3n asistida por ordenador<\/h2>\n<div id=\"text-2\" class=\"outline-text-2\"><\/div>\n<div id=\"outline-container-org0b6634a\" class=\"outline-3\">\n<h3 id=\"org0b6634a\"><span class=\"section-number-3\">2.1<\/span> DAO con Isabelle\/HOL<\/h3>\n<div id=\"text-2-1\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"ftp:\/\/ceur-ws.org\/pub\/publications\/rwth\/informatik\/2020\/2020-02.pdf\">Towards an Isabelle Theory for distributed, interactive systems-the untimed case<\/a>. ~ Jens Christoph B\u00fcrger et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/eprints.whiterose.ac.uk\/155734\/1\/hybrid_kat.pdf\">Differential Hoare logics and refinement calculi for hybrid systems with Isabelle\/HOL<\/a>. ~ Simon Foster, Jonathan Juli\u00e1n Huerta y Munive, and Georg Struth. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.04314\">Formal specification of a security framework for smart contracts<\/a>. ~ M. Mandrykin et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Mersenne_Primes.html\">Mersenne primes and the Lucas\u2013Lehmer test in Isabelle\/HOL<\/a>. ~ Manuel Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/EipOEWKlSBQ\">Proof pearl: Braun trees<\/a>. ~ Tobias Nipkow. #ITP #IsabelleHOL<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org94a6edc\" class=\"outline-3\">\n<h3 id=\"org94a6edc\"><span class=\"section-number-3\">2.2<\/span> DAO con Coq<\/h3>\n<div id=\"text-2-2\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_boldo.pdf\">A Coq formalization of Lebesgue integration of nonnegative functions<\/a>. ~ Sylvie Boldo et als. #ITP #Coq #Math<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_keller.pdf\">SMTCoq: Coq automation and its application to formal mathematics<\/a>. ~ Chantal Keller. #ITP #Coq #SMT #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/8542Cw7DdYY\">Undecidability of higher-order unification formalised in Coq<\/a>. ~ Simon Spies. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/youtu.be\/F35yA6EHrAo\">A functional proof pearl: Inverting the Ackermann heirarchy<\/a>. ~ Linh Tran. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/youtu.be\/HKrIMvC4xTA\">Verified programming of Turing machines in Coq<\/a>. ~ Fabian Kunze. #ITP #Coq<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org0829ae1\" class=\"outline-3\">\n<h3 id=\"org0829ae1\"><span class=\"section-number-3\">2.3<\/span> DAO con Lean<\/h3>\n<div id=\"text-2-3\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.04301\">Tabled typeclass resolution<\/a>. ~ D. Selsam, S. Ullrich, L. de Moura. #ITP #LeanProver<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgd01c2ed\" class=\"outline-3\">\n<h3 id=\"orgd01c2ed\"><span class=\"section-number-3\">2.4<\/span> DAO con Agda<\/h3>\n<div id=\"text-2-4\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/is.muni.cz\/th\/vhz48\/thesis.pdf\">Coinductive formalization of SECD machine in Agda<\/a>. ~ Adam Krupi\u010dka. #MsC_Thesis #ITP #Agda<\/li>\n<li><a href=\"https:\/\/niccoloveltri.github.io\/cpp20.pdf\">Formalizing \u03c0-calculus in Guarded Cubical Agda<\/a>. ~ Niccol\u00f2 Veltri, Andrea Vezzosi. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/youtu.be\/Rt2OrG3IHkU\">Three equivalent ordinal notation systems in cubical Agda<\/a>. ~ Fredrick Nordvall Forsberg. #ITP #Agda #Math<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org56f1f6f\" class=\"outline-3\">\n<h3 id=\"org56f1f6f\"><span class=\"section-number-3\">2.5<\/span> DAO en general<\/h3>\n<div id=\"text-2-5\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_buzzard.pdf\">The future of Mathematics?<\/a> ~ Kevin Buzzard. #Math #ITP<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_carneiro.pdf\">Metamath Zero (or: how to verify a verifier)<\/a>. ~ Mario Carneiro. #ITP #MetamathZero<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_lisitsa.pdf\">First-order theorem (dis)proving for reachability problems in verification and experimental mathematics<\/a>. ~ Alexei Lisitsa. #ATP #Prover9 #Mace4 #Math<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgd3b3c60\" class=\"outline-2\">\n<h2 id=\"orgd3b3c60\"><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:\/\/tedsider.org\/teaching\/higher_order_20\/higher_order_crash_course.pdf\">Crash course on higher-order logic, type theory, etc<\/a>. ~ Theodore Sider. #Logic via @RrrichardZach<\/li>\n<li><a href=\"https:\/\/books.google.es\/books?id=0el8pO27BPoC&amp;lpg=PP1\">A modern perspective on type theory: From its origins until today<\/a>. ~ Fairouz Kamareddine, Twan Laan, and Rob Nederpelt. #eBook #TypeTheory<\/li>\n<\/ul>\n<\/div>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, del 19 al 24 de enero, 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\/6952"}],"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=6952"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6952\/revisions"}],"predecessor-version":[{"id":6953,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6952\/revisions\/6953"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6952"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6952"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6952"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}