{"id":6946,"date":"2020-01-19T10:28:22","date_gmt":"2020-01-19T09:28:22","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6946"},"modified":"2020-01-19T10:31:07","modified_gmt":"2020-01-19T09:31:07","slug":"resumen-de-lecturas-compartidas-del-12-al-18-de-enero-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-del-12-al-18-de-enero-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas del 12 al 18 de enero de 2020"},"content":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, del 12 al 18 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-org7bc5030\" class=\"outline-2\">\n<h2 id=\"org7bc5030\"><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-org7fe1984\" class=\"outline-3\">\n<h3 id=\"org7fe1984\"><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=\"https:\/\/vrom911.github.io\/blog\/common-stanzas\">Common stanzas<\/a>. ~ Veronika Romashkina (@vronnie911). #Haskell #Cabal<\/li>\n<li><a href=\"http:\/\/brendanfong.com\/programmingcats_files\/C4P-chapter1.pdf\">Is Haskell a category?<\/a> ~ B. Fong, B. Milewski, D. Spivak. #FunctionalProgramming #CategoryTheory<\/li>\n<li><a href=\"http:\/\/brendanfong.com\/programmingcats_files\/cats4progs-DRAFT.pdf\">Programming with categories (Draft)<\/a>. ~ B. Fong, B. Milewski, D.I. Spivak. #FunctionalProgramming #Haskell #CategoryTheory<\/li>\n<li><a href=\"https:\/\/alexnixon.github.io\/2020\/01\/14\/static-types-are-dangerous.html\">Static types are dangerously interesting<\/a>. ~ Alex Nixon (@alexnixon_uk). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/foldl-adjunction.html\">Adjunctions in the wild: foldl<\/a>. ~ Justin Le (@mstk). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/deontologician.com\/wiki\/lenses\/\">Digging into Lenses<\/a>. ~ Josh Kuhn (@deontologician). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/digitalcommons.wpi.edu\/cgi\/viewcontent.cgi?article=1457&amp;context=etd-dissertations\">A framework for exploring finite models<\/a>. ~ Salman Saghafi. #PhD_Thesis #Logic #Haskell<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2020\/1\/13\/using-cabal-on-its-own\">Using Cabal on its own<\/a>. ~ James Bowen (@james_OWA). #Haskell #Cabal<\/li>\n<li><a href=\"https:\/\/williamyaoh.com\/posts\/2020-01-11-road-to-proficient.html\">The road to proficient Haskell<\/a>. ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2020-01-16-data-vs-control.html\">A tale of two functors (or: how I learned to stop worrying and love Data and Control)<\/a>. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org5309abe\" class=\"outline-3\">\n<h3 id=\"org5309abe\"><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:\/\/lisp-univ-etc.blogspot.com\/2020\/01\/programming-algorithms-approximation.html\">Programming algorithms: approximation<\/a>. ~ Vsevolod Dyomkin. #CommonLisp #Algorithms<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org8697442\" class=\"outline-3\">\n<h3 id=\"org8697442\"><span class=\"section-number-3\">1.3<\/span> Programaci\u00f3n l\u00f3gica con Prolog<\/h3>\n<\/div>\n<\/div>\n<div id=\"outline-container-org444452f\" class=\"outline-2\">\n<h2 id=\"org444452f\"><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-orgc4bfdeb\" class=\"outline-3\">\n<h3 id=\"orgc4bfdeb\"><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=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_eberl.pdf\">Automating asymptotics in a theorem prover<\/a>. ~ Manuel Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_gouezel.pdf\">On a mathematician&#8217;s attempts to formalize his own research in proof assistants<\/a>. ~ S\u00e9bastien Gou\u00ebzel. #ITP #IsabelleHOL #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_immler.pdf\">ODEs and the Poincar\u00e9-Bendixson theorem in Isabelle\/HOL<\/a>. ~ Fabian Immler, Yong Kiam Tan. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_li.pdf\">Reasoning with non-linear formulas in Isabelle\/HOL<\/a>. ~ Wenda Li. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1910.08955\">Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of G\u00f6del&#8217;s ontological argument<\/a>. ~ C. Benzm\u00fcller, D. Fuenmayor. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1910.12863\">Computer-supported exploration of a categorical axiomatization of modeloids<\/a>. ~ L. Tiemens, D.S. Scott, C. Benzm\u00fcller, M. Benda. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Approximation_Algorithms.html\">Verified approximation algorithms in Isabelle\/HOL<\/a>. ~ R. E\u00dfmann, T. Nipkow, S. Robillard. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Closest_Pair_Points.html\">Closest pair of points algorithms<\/a>. ~ M. Rau, T. Nipkow. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Complex_Geometry.html\">Complex geometry in Isabelle\/HOL<\/a>. ~ F. Mari\u0107, D. Simi\u0107. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Poincare_Disc.html\">Poincar\u00e9 disc model in Isabelle\/HOL<\/a>. ~ D. Simi\u0107, F. Mari\u0107, P. Boutry. #ITP #IsabelleHOL #Math<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgff71640\" class=\"outline-3\">\n<h3 id=\"orgff71640\"><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_cohen.pdf\">Generating mathematical structure hierarchies using Coq-ELPI<\/a>. ~ C. Cohen, K. Sakaguchi, E. Tassi. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/github.com\/math-comp\/hierarchy-builder\">High level commands to declare a hierarchy based on packed classes<\/a>. ~ C. Cohen, K. Sakaguchi, E. Tassi. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.cs.rit.edu\/~mtf\/student-resources\/20191_huang_mscourse.pdf\">A mechanized formalization of the WebAssembly specification in Coq<\/a>. ~ X. Huang. #ITP #Coq<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org0a6897a\" class=\"outline-3\">\n<h3 id=\"org0a6897a\"><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=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_massot.pdf\">Formalizing a sophisticated definition<\/a>. ~ Patrick Massot, Kevin Buzzard, Johan Commelin. #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_strickland.pdf\">Using Lean for new research<\/a>. ~ Neil Strickland. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.07801\">Iterated chromatic localisation<\/a>. ~ Neil Strickland, Nicola Bellumat. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/github.com\/NeilStrickland\/itloc\">Lean code formalising many of the proofs from the paper &#8220;Iterated chromatic localisation&#8221;<\/a>. ~ Neil Strickland, Nicola Bellumat. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/github.com\/NeilStrickland\/lean_primes\">Proof in Lean that there are infinitely many primes<\/a>. ~ Neil Strickland. #ITP #LeanProver #Math<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org8e5c871\" class=\"outline-3\">\n<h3 id=\"org8e5c871\"><span class=\"section-number-3\">2.4<\/span> DAO con PVS<\/h3>\n<div id=\"text-2-4\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.02981\">Automatic generation and verification of test-stable floating-point code<\/a>. ~ L. Titolo, M. Moscato, C.A. Mu\u00f1oz. #ITP<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.04457\">A verified packrat parser interpreter for parsing expression grammars<\/a>. ~ C. Blaudeau, N. Shankar. #ITP #PVS<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org0840c70\" class=\"outline-3\">\n<h3 id=\"org0840c70\"><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=\"https:\/\/kwarc.info\/people\/mkohlhase\/submit\/tetrapod-survey.pdf\">The space of mathematical software systems<\/a>. ~ J. Carette, W.M. Farmer, Y. Sharoda. #ATP #ITP #Math #CompSci<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-org1b006c4\" class=\"outline-2\">\n<h2 id=\"org1b006c4\"><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:\/\/dailynous.com\/2018\/11\/20\/randomly-generated-self-correcting-logic-exercises-site\/\">Randomly generated and self-correcting logic exercises site<\/a>. ~ Justin Weinberg. #Logic #WorldLogicDay<\/li>\n<li><a href=\"http:\/\/www.cl.cam.ac.uk\/~jrh13\/papers\/joerg.pdf\">History of interactive theorem proving<\/a>. ~ J. Harrison, J. Urban, F. Wiedijk. #ITP #Logic #CompSci #WorldLogicDay<\/li>\n<li><a href=\"http:\/\/www.cs.cornell.edu\/courses\/cs4860\/2019fa\/lectures\/L2-A-Story-of-Logic.pdf\">The story of Logic<\/a>. ~ Robert L. Constable. #Logic #CompSci #WorldLogicDay<\/li>\n<li><a href=\"http:\/\/www.informatics-europe.org\/images\/ECSS\/ECSS2009\/slides\/Gottlob.pdf\">Computer Science as the continuation of Logic by other means<\/a>. ~ Georg Gottlob. #Logic #CompSci #WorldLogicDay<\/li>\n<li><a href=\"http:\/\/www.ru.is\/faculty\/luca\/SLIDES\/logic-and-cs.pdf\">Computer Science and Logic (a match made in heaven)<\/a>. ~ Luca Aceto. #Logic #CompSci #WorldLogicDay<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1802.03292\">Mathematical Logic in Computer Science<\/a>. ~ Assaf Kfoury. #Logic #CompSci #WorldLogicDay<\/li>\n<li><a href=\"https:\/\/github.com\/salmans\/rusty-razor\">Rusty Razor is a tool for constructing finite models for first-order theories<\/a>. ~ Salman Saghafi. #Logic<\/li>\n<li><a href=\"https:\/\/www.cadeinc.org\/Data\/HerbrandAwardSlidesConstable.pdf\">Automated reasoning: From bold dreams to Computer Science methodology<\/a>. ~ Robert L. Constable. #ATP #CompSci #WorldLogicDay<\/li>\n<li><a href=\"https:\/\/www.conicet.gov.ar\/taut-el-software-desarrollado-por-un-filosofo-del-conicet-para-ensenar-logica\/\">TAUT: el software desarrollado por un fil\u00f3sofo del CONICET para ense\u00f1ar L\u00f3gica<\/a>. #L\u00f3gica #WorldLogicDay<\/li>\n<li><a href=\"https:\/\/www.cs.ru.nl\/~herman\/ictopen.pdf\">Can the computer really help us to prove theorems? ~ Herman Geuvers<\/a>. #ITP #Logic #CompSci #WorldLogicDay<\/li>\n<li><a href=\"https:\/\/www.cs.upc.edu\/~roberto\/EffectivenessOfLogic.pdf\">On the unusual effectiveness of Logic in Computer Science<\/a>. ~ J.Y. Halpern et als. #Logic #CompSci #WorldLogicDay<\/li>\n<li><a href=\"https:\/\/www.logicmatters.net\/wp-content\/uploads\/2019\/12\/TeachYourselfLogic2020.pdf\">Teach yourself Logic 2020: A study guide<\/a>. ~ Peter Smith. #Logic<\/li>\n<li><a href=\"https:\/\/www.taut-logic.com\/index.html\">TAUT: A website that contains randomly-generated, self-correcting logic excercises<\/a>. ~ Ariel Roff\u00e9. #Logic<\/li>\n<\/ul>\n<\/div>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, del 12 al 18 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\/6946"}],"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=6946"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6946\/revisions"}],"predecessor-version":[{"id":6948,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6946\/revisions\/6948"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6946"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6946"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6946"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}