{"id":6935,"date":"2020-01-12T10:51:12","date_gmt":"2020-01-12T09:51:12","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6935"},"modified":"2020-01-25T09:32:26","modified_gmt":"2020-01-25T08:32:26","slug":"resumen-de-lecturas-compartidas-del-1-al-11-de-enero-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-del-1-al-11-de-enero-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas del 1 al 11 de enero de 2020"},"content":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, del 1 al 11 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>.<br \/>\n<!--more--><\/p>\n<div id=\"outline-container-orga902764\" class=\"outline-2\">\n<h2 id=\"orga902764\"><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-orgda8317b\" class=\"outline-3\">\n<h3 id=\"orgda8317b\"><span class=\"section-number-3\">1.1<\/span> Programaci\u00f3n funcional con Haskell (#FunctionalProgramming #Haskell)<\/h3>\n<div id=\"text-1-1\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/blog.sigplan.org\/2019\/12\/30\/defunctionalization-everybody-does-it-nobody-talks-about-it\/\">Defunctionalization: Everybody does it, nobody talks about it<\/a>. ~ James Koppel. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/cswithbaddrawings.wordpress.com\/2020\/01\/10\/gain-confidence-with-haskell\/\">Gain confidence with Haskell!<\/a> ~ Brandon Chinn. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dixonary.co.uk\/blog\/haskell\/small\">Generating small binaries in Haskell<\/a>. ~ Alex Dixon (@dixonary_). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371121?download=true\">Kind inference for datatypes<\/a>. ~ N. Xie, R.A. Eisenberg, B.C.d.S. Oliveira. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/gist.github.com\/mightybyte\/6c469c125eb50e0c2ebf4ae26b5adfff\">Haskell language extension taxonomy<\/a>. ~ Doug Beardsley. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/bolt12\/laop\">Linear algebra of programming &#8211; Algebraic matrices in Haskell<\/a>. ~ Armando Santos (@_bolt12). #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/github.com\/bolt12\/master-thesis\">Selective applicative functors &amp; probabilities<\/a>. ~ Armando Santos (@_bolt12). #MSc_Thesis #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/github.com\/saurabhkukade\/Haskell_Study\">Collections of papers and books about Haskell, type theory and category theory<\/a>. ~ Saurabh Kukade. #Haskell #TypeTheory #CategoryTheory<\/li>\n<li><a href=\"https:\/\/her.esy.fun\/posts\/0010-Haskell-Now\/index.html\">Learn Haskell now!<\/a> ~ Yann Esposito (@yogsototh). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/jaspervdj.be\/posts\/2020-01-04-mandelbrot-lovejoy-rain.html\">Mandelbrot &amp; Lovejoy&#8217;s rain fractals<\/a>. ~ Jasper Van der Jeugt (@jaspervdj). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2020\/1\/6\/organizing-our-package\">Organizing our package!<\/a> ~ James Bowen (@james_OWA). #Haskell #Cabal #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.logicmatters.net\/2020\/01\/09\/programming-with-categories\/\">Programming with categories<\/a>. ~ Peter Smith. #Programming #CategoryTheory<\/li>\n<li><a href=\"https:\/\/www.simplehaskell.org\/\">The simple Haskell initiative<\/a>. #Haskell #FunctionalProgramming<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org8a18ea9\" class=\"outline-3\">\n<h3 id=\"org8a18ea9\"><span class=\"section-number-3\">1.2<\/span> Programaci\u00f3n l\u00f3gica con Prolog (#LogicProgramming #Prolog)<\/h3>\n<div id=\"text-1-2\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/arxiv.org\/abs\/1909.07479\">On correctness of an n queens program<\/a>. ~ W\u0142odzimierz Drabent. #LogicProgramming #Prolog #Verification<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgcc3f6db\" class=\"outline-2\">\n<h2 id=\"orgcc3f6db\"><span class=\"section-number-2\">2<\/span> DAO: Demostraci\u00f3n asistida por ordenador (#ITP)<\/h2>\n<div id=\"text-2\" class=\"outline-text-2\"><\/div>\n<div id=\"outline-container-orgb91e04e\" class=\"outline-3\">\n<h3 id=\"orgb91e04e\"><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:\/\/www21.in.tum.de\/~nipkow\/pubs\/cpp20.pdf\">Proof pearl: Braun trees<\/a>. ~ T. Nipkow, T. Sewell. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Bicategory.html\">Bicategories in Isabelle\/HOL<\/a> ~ Eugene W. Stark. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Gauss_Sums.html\">Gauss sums and the P\u00f3lya\u2013Vinogradov inequality<\/a>. ~ R. Raya, M. Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Hybrid_Logic.html\">Formalizing a Seligman-style tableau system for hybrid logic in Isabelle\/HOL<\/a>. ~ Asta Halkj\u00e6r. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Skip_Lists.html\">Skip lists in Isabelle\/HOL<\/a>. ~ M.W. Haslbeck, M. Eberl. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Zeta_3_Irrational.html\">The irrationality of \u03b6(3) in Isabelle\/HOL<\/a>. ~ Manuel Eberl. #ITP #IsabelleHOL #Math<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org3b0191e\" class=\"outline-3\">\n<h3 id=\"org3b0191e\"><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=\"https:\/\/arxiv.org\/abs\/1912.06611\">A formal proof of the irrationality of \u03b6(3)<\/a>. ~ Assia Mahboubi, Thomas Sibut-Pinote. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/artagnon.com\/articles\/leancoq#main\">Lean versus Coq: The cultural chasm<\/a>. ~ Ramkumar Ramachandra. #ITP #LeanProver #Coq<\/li>\n<li><a href=\"https:\/\/jfr.unibo.it\/article\/view\/9757\">LF+ in Coq for &#8220;fast and loose&#8221; reasoning<\/a>. ~ F. Alessi. #ITP #Coq<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org32b3f5b\" class=\"outline-3\">\n<h3 id=\"org32b3f5b\"><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:\/\/artagnon.com\/articles\/leancoq#main\">Lean versus Coq: The cultural chasm<\/a>. ~ Ramkumar Ramachandra. #ITP #LeanProver #Coq<\/li>\n<li><a href=\"https:\/\/agentultra.github.io\/lean-for-hackers\/\">Lean 3 for hackers<\/a>. ~ J Kenneth King. #LeanProver #FunctionalProgramming<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org435f4ce\" class=\"outline-3\">\n<h3 id=\"org435f4ce\"><span class=\"section-number-3\">2.4<\/span> DAO con HOL<\/h3>\n<div id=\"text-2-4\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/t.co\/8IZttMkU33\">Design and verification of parity checking circuit using HOL4 theorem proving<\/a>. ~ E. Deni\u0307z, K. Aksoy, S. Tahar, Y. Zeren. #ITP #HOL4<\/li>\n<li><a href=\"http:\/\/www.eds.yildiz.edu.tr\/AjaxTool\/GetArticleByPublishedArticleId?PublishedArticleId=3936\">Introduction to HOL4 theorem prover<\/a>. ~ K. Aksoy, S. Tahar, Y. Zeren. #ITP #HOL4<\/li>\n<li><a href=\"https:\/\/tqft.net\/web\/research\/students\/YimingXu\/thesis.pdf\">Formalizing modal logic in HOL<\/a>. ~ Yiming Xu. #PhD_Thesis #ITP #HOL #Logic<\/li>\n<li><a href=\"http:\/\/save.seecs.nust.edu.pk\/pubs\/2020\/SAC_2020_1.pdf\">Proof searching in HOL4 with genetic algorithm<\/a>. ~ M.Z. Nawaz et als #ITP #HOL4<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-org9be2e27\" class=\"outline-2\">\n<h2 id=\"org9be2e27\"><span class=\"section-number-2\">3<\/span> L\u00f3gica (#Logic)<\/h2>\n<div id=\"text-3\" class=\"outline-text-2\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/arxiv.org\/abs\/1804.05495\">Constructive reverse mathematics<\/a>. ~ Hannes Diener. #Logic #Math<\/li>\n<li><a href=\"http:\/\/www.ams.org\/journals\/notices\/202001\/rnoti-p77.pdf\">Different problems, common threads: Computing the difficulty of mathematical problems<\/a>. ~ Karen Lange. #Logic #Math #CompSci<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.02657\">Motivated proofs: what they are, why they matter and how to write them<\/a>. ~ Rebecca Lea Morris. #Logic #Math<\/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 11 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\/6935"}],"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=6935"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6935\/revisions"}],"predecessor-version":[{"id":6955,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6935\/revisions\/6955"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6935"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6935"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6935"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}