{"id":7080,"date":"2020-03-09T13:18:38","date_gmt":"2020-03-09T12:18:38","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7080"},"modified":"2020-03-09T13:18:38","modified_gmt":"2020-03-09T12:18:38","slug":"resumen-de-lecturas-compartidas-del-1-al-7-de-marzo-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-del-1-al-7-de-marzo-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas del 1 al 7 de marzo de 2020"},"content":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, del 1 al 7 de marzo, 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-org95c73e8\" class=\"outline-2\">\n<h2 id=\"org95c73e8\"><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-orgbc45c6b\" class=\"outline-3\">\n<h3 id=\"orgbc45c6b\"><span class=\"section-number-3\">1.1<\/span> DAO con Coq<\/h3>\n<div id=\"text-1-1\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/perso.ens-lyon.fr\/damien.pous\/apmep\/\">First steps with Coq (for primary and secondary school teachers, APMEP, Grenoble, 2011)<\/a>. ~ Damien Pous. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/perso.ens-lyon.fr\/nicolas.brisebarre\/M2R\/CoqApprox\">Course: Approximation theory and proof assistants: certified computations<\/a>. ~ Nicolas Brisebarre, Damien Pous.\/#coqsessions #ITP #Coq #Math<\/li>\n<li><a href=\"http:\/\/users.ece.utexas.edu\/~gligoric\/papers\/PalmskogETAL20Chip.pdf\">Practical machine-checked formalization of change impact analysis<\/a>. ~ Karl Palmskog, Ahmet Celik, Milos Gligoric. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3377555.3377884\">Postcondition-preserving fusion of postorder tree transformations<\/a>. ~ Eleanor Davies, Sara Kalvala. #ITP #Coq<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orga6cecfa\" class=\"outline-3\">\n<h3 id=\"orga6cecfa\"><span class=\"section-number-3\">1.2<\/span> DAO en general<\/h3>\n<div id=\"text-1-2\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/philsci-archive.pitt.edu\/16976\/\">Audience role in mathematical proof development<\/a>. ~ Zoe Ashton. #Logic #Math #ITP<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgf29faf7\" class=\"outline-2\">\n<h2 id=\"orgf29faf7\"><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-org96fa73a\" class=\"outline-3\">\n<h3 id=\"org96fa73a\"><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=\"http:\/\/neilmitchell.blogspot.com\/2020\/03\/how-to-get-haskell-job.html\">How to get a Haskell job<\/a>. ~ Neil Mitchell (@ndm_haskell). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/apfelmus.nfshost.com\/articles\/lazy-eval-intro.html\">How does lazy evaluation work in Haskell?<\/a> ~ Heinrich Apfelmus. #Haskell #FunctionalProgramming via @etorreborre<\/li>\n<li><a href=\"https:\/\/apfelmus.nfshost.com\/articles\/lazy-eval-modular-code.html\">Writing more modular code with lazy evaluation<\/a>. ~ Heinrich Apfelmus. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2003.00032\">Declarative stream runtime verification (hLola)<\/a>. ~ Mart\u0131\u0301n Ceresa, Felipe Gorostiaga, C\u00e9sar S\u00e1nchez. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.shaynefletcher.org\/2020\/03\/ghc-haskell-pats-and-lpats.html\">GHC Haskell Pats and LPats<\/a>. ~ Shayne Fletcher. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2020\/03\/03\/competitive-programming-in-haskell-modular-arithmetic-part-2\/\">Competitive programming in Haskell: modular arithmetic, part 2<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/free.cofree.io\/2020\/02\/29\/dsl\/\">Building a friendly and safe EDSL with IxState and TypeLits<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/@cdsmithus\/optimizing-a-maze-with-graph-theory-genetic-algorithms-and-haskell-e3702dd6439f\">Optimizing a maze with graph theory, genetic algorithms, and Haskell<\/a>. ~ Chris Smith (@cdsmithus). #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/nbviewer.jupyter.org\/github\/Anabra\/grin\/blob\/fd9de6d3b9c7ec5f4aa7d6be41285359a73494e3\/papers\/stcs-2019\/article\/tex\/main.pdf\">A modern look at GRIN, an optimizing functional language back end<\/a>. ~ Csaba Hruska, P\u00e9ter D\u00e1vid Podlovics, Andor P\u00e9nzes. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/research.chalmers.se\/publication\/515535\/file\/515535_Fulltext.pdf\">Automated derivation of random generators for algebraic data types<\/a>. ~ Agust\u00edn Mista. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/scm.iis.sinica.edu.tw\/pub\/2020-monadic-sort.pdf\">Declarative pearl: Deriving monadic quicksort<\/a>. ~ Shin-Cheng Mu, Tsung-Ju Chiang. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/utdemir.com\/posts\/ann-distributed-dataset.html\">distributed-dataset: A distributed data processing framework in Haskell<\/a>. ~ Utku Demir. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.michaelburge.us\/2017\/08\/17\/rolling-your-own-blockchain.html\">Create blockchain in Haskell (Rolling your own blockchain in Haskell)<\/a>. ~ Michael Burge (2017). #Haskell #Blockchain<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgddbd2df\" class=\"outline-3\">\n<h3 id=\"orgddbd2df\"><span class=\"section-number-3\">2.2<\/span> Programaci\u00f3n funcional con Lisp<\/h3>\n<div id=\"text-2-2\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/github.com\/norvig\/paip-lisp\">Lisp code for the textbook &#8220;Paradigms of Artificial Intelligence Programming&#8221;<\/a>. ~ Peter Norvig. #CommonLisp #AI<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org5c57e49\" class=\"outline-3\">\n<h3 id=\"org5c57e49\"><span class=\"section-number-3\">2.3<\/span> Programaci\u00f3n funcional con Miranda<\/h3>\n<div id=\"text-2-3\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/www.cs.kent.ac.uk\/people\/staff\/dat\/ccount\/click.php?id=4\">Church&#8217;s thesis and functional programming<\/a>. ~ David Turner (2006). #Logic #FunctionalProgramming #Miranda<\/li>\n<li><a href=\"http:\/\/www.cs.ucl.ac.uk\/teaching\/3C11\/book\/book.html\">Programming with Miranda<\/a>. ~ C. Clack, C. Myers, and E. Poon (1995). #eBook #Miranda #FunctionalProgramming<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org69f603c\" class=\"outline-3\">\n<h3 id=\"org69f603c\"><span class=\"section-number-3\">2.4<\/span> Programaci\u00f3n funcional en general<\/h3>\n<div id=\"text-2-4\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/www.cs.kent.ac.uk\/people\/staff\/dat\/tfp12\/tfp12.pdf\">Some history of functional programming languages<\/a>. ~ David Turner (2012). #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/lamport.azurewebsites.net\/pubs\/lamport-types.pdf\">Should your specification language be typed?<\/a>. ~ Leslie Lamport, Lawrence C. Paulson (1999). #ITP #FunctionalProgramming<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgaa9db44\" class=\"outline-3\">\n<h3 id=\"orgaa9db44\"><span class=\"section-number-3\">2.5<\/span> Programaci\u00f3n l\u00f3gica con Prolog<\/h3>\n<div id=\"text-2-5\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/arxiv.org\/abs\/2003.01422\">The Prolog debugger and declarative programming. Examples<\/a>. ~ W\u0142odzimierz Drabent. #Prolog #LogicProgramming<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-org75bd0a6\" class=\"outline-2\">\n<h2 id=\"org75bd0a6\"><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=\"https:\/\/arxiv.org\/abs\/2003.01935\">Intuitionistic mathematics and logic<\/a>. ~ Joan R. Moschovakis, Garyfallia Vafeiadou. #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/220531947_Seventy-Five_Problems_for_Testing_Automatic_Theorem_Provers\">Seventy-five problems for testing automatic theorem provers<\/a>. ~ Francis Jeffry Pelletier (1986). #Logic<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2020-03-05-peirce.html\">Code is engineering, types are science<\/a>. ~ Juan Raphael Diaz Sim\u00f5es. #Programming #Logic<\/li>\n<\/ul>\n<\/div>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, del 1 al 7 de marzo, 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\/7080"}],"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=7080"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7080\/revisions"}],"predecessor-version":[{"id":7081,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7080\/revisions\/7081"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7080"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7080"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7080"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}