{"id":7031,"date":"2020-02-16T18:20:19","date_gmt":"2020-02-16T17:20:19","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7031"},"modified":"2020-02-16T18:20:19","modified_gmt":"2020-02-16T17:20:19","slug":"resumen-de-lecturas-compartidas-del-9-al-15-de-febrero-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-del-9-al-15-de-febrero-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas del 9 al 15 de febrero de 2020"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, del 9 al 15 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-org1bb430c\" class=\"outline-2\">\n<h2 id=\"org1bb430c\"><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-org8f49437\" class=\"outline-3\">\n<h3 id=\"org8f49437\"><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:\/\/armkeh.github.io\/blog\/EqualityOfFunctions.html\">Equality of functions in Agda<\/a>. ~ Mark Armstrong. #ITP #Agda #FunctionalProgramming via @armk_eh<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org9941516\" class=\"outline-3\">\n<h3 id=\"org9941516\"><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:\/\/www.cse.chalmers.se\/~rjmh\/tfp\/proceedings\/TFP_2020_paper_20.pdf\">A proof assistant based formalisation of core Erlang<\/a>. ~ P\u00e9ter Bereczky, D\u00e1niel Horp\u00e1csi and Simon Thompson. #ITP #Coq #Erlang<\/li>\n<li><a href=\"https:\/\/github.com\/coq-community\/awesome-coq\">Awesome Coq Awesome (A curated list of awesome Coq libraries, plugins, tools, and resources)<\/a>. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/pedroabreu0\/pedroabreu0.github.io\/raw\/master\/docs\/POPL20-poster.pdf\">How small can we make a useful type theory?<\/a> ~ Pedro Abreu (@etapedro). #ITP #Coq #Cedille #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/pedrotst\/coquedille\">Coquedille: A Coq to Cedille transpiler written in Coq<\/a>. ~ Pedro Abreu (@etapedro). #ITP #Coq #Cedille #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/339129400_Mac_Lane%27s_Comparison_Theorem_for_the_Kleisli_Construction_Formalized_in_Coq\">Mac Lane\u2019s comparison theorem for the Kleisli construction formalized in Coq<\/a>. ~ Burak Ekici, and Cezary Kaliszyk. #ITP #Coq<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org68abb7a\" class=\"outline-3\">\n<h3 id=\"org68abb7a\"><span class=\"section-number-3\">1.3<\/span> DAO con HOL Light<\/h3>\n<div id=\"text-1-3\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/www.mdpi.com\/1996-1073\/13\/3\/712\/pdf\">Formalization of cost and utility in Microeconomics<\/a>. ~ Asad Ahmed, Osman Hasan, Falah Awwad, and Nabil Bastaki. #ITP HOL_Light<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org1e44f86\" class=\"outline-3\">\n<h3 id=\"org1e44f86\"><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=\"https:\/\/wdi.centralesupelec.fr\/boulanger\/Enseignement\/Niklaus\">Cours: S\u00e9mantique des langages<\/a>. ~ Fr\u00e9d\u00e9ric Boulanger. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/wdi.centralesupelec.fr\/boulanger\/Enseignement\/TutoIsabelle\">Tutoriel: types de donn\u00e9es, fonctions et preuves en Isabelle<\/a>. ~ Fr\u00e9d\u00e9ric Boulanger. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.cs.vu.nl\/~jhl890\/pub\/hoelzl2013typeclasses.pdf\">Type classes and filters for mathematical analysis in Isabelle\/HOL<\/a>. ~ Johannes H\u00f6lzl, Fabian Immler, Brian Huffman. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Arith_Prog_Rel_Primes.html\">Arithmetic progressions and relative primes<\/a>. ~ Jos\u00e9 Manuel Rodr\u00edguez Caballero. #ITP #IsabelleHOL #Math<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org755c622\" class=\"outline-3\">\n<h3 id=\"org755c622\"><span class=\"section-number-3\">1.5<\/span> DAO con Lean<\/h3>\n<div id=\"text-1-5\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2020\/02\/09\/lean-is-better-for-proper-maths-than-all-the-other-theorem-provers\/\">Lean is better for proper maths than all the other theorem provers<\/a>. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2020\/02\/09\/where-is-the-fashionable-mathematics\/\">Where is the fashionable mathematics? ~ Kevin Buzzard (@XenaProject)<\/a>. #Math #ITP #LeanProver #Coq #IsabelleHOL<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orga0f2a43\" class=\"outline-3\">\n<h3 id=\"orga0f2a43\"><span class=\"section-number-3\">1.6<\/span> DAO en general<\/h3>\n<div id=\"text-1-6\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/rg1-teaching.mpi-inf.mpg.de\/autrea-ws19\/script.pdf\">Automated reasoning I<\/a>. ~ Uwe Waldmann. #eBook #ATP #Logic<\/li>\n<li><a href=\"http:\/\/rg1-teaching.mpi-inf.mpg.de\/autrea2-ss18\/script.pdf%20\">Automated reasoning II<\/a>. ~ Sophie Tourret, Uwe Waldmann. #eBook #ATP #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2002.00423\">An experimental study of formula embeddings for automated theorem proving in first-order logic<\/a>. ~ Ibrahim Abdelaziz et als. #ATP #MachineLearning<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-org1091e23\" class=\"outline-2\">\n<h2 id=\"org1091e23\"><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-orgfaab020\" class=\"outline-3\">\n<h3 id=\"orgfaab020\"><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:\/\/cleilaclo2018.mackenzie.br\/docs\/SIESC\/182970.pdf\">MateFun: Functional Programming and Math with adolescents<\/a>. ~ Alejandra Carboni et als. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"http:\/\/oleg.fi\/gists\/posts\/2020-02-09-compiling-haskell-to-javascript.html\">Compiling Haskell to JavaScript, not in the way you&#8217;d expect<\/a>. ~ Oleg Grenrus (@phadej). #Haskell #FunctionalProgramming #JavaScript<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~rjmh\/tfp\/proceedings\/TFP_2020_paper_16.pdf\">State will do<\/a>. ~ Willem Seynaeve, Koen Pauwels and Tom Schrijvers. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~rjmh\/tfp\/proceedings\/TFP_2020_paper_17.pdf\">A DSL for fluorescence microscopy<\/a>. Birthe van den Berg, Peter Dedecker, Tom Schrijvers. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~rjmh\/tfp\/proceedings\/TFP_2020_paper_2.pdf\">An equational modeling of asynchronous concurrent programming<\/a>. ~ David Janin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~rjmh\/tfp\/proceedings\/TFP_2020_paper_7.pdf\">PaSe: An extensible and inspectable DSL for micro-animations<\/a>. ~ Ruben P. Pieters and Tom Schrijvers. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~rjmh\/tfp\/proceedings\/TFP_2020_paper_8.pdf\">Generating next step hints for task oriented programs using symbolic execution<\/a>. ~ Nico Naus and Tim Steenvoorden. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~rjmh\/tfp\/proceedings\/TFP_2020_paper_9.pdf\">BinderAnn: Automated reification of source annotations for monadic EDSLs<\/a>. ~ Agust\u00edn Mista and Alejandro Russo. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/andre.tips\/wmh\/generalized-algebraic-data-types-and-data-kinds\/\">Generalized Algebraic Data Types and Data Kinds<\/a>. ~ Andre Popovitch (@PopovitchAndre). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.functorial.com\/posts\/2015-12-06-Counterexamples.html\">Counterexamples of type classes<\/a>. ~ Phil Freeman. #Haskell #Purescript #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.sumtypeofway.com\/posts\/introduction-to-recursion-schemes.html\">An introduction to recursion schemes<\/a>. ~ Patrick Thomson. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/chrisdone.com\/posts\/data-typeable\/\">Typeable and Data in Haskell<\/a>. ~ Chris Done (@christopherdone). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/markkarpov.com\/tutorial\/th.html\">Template Haskell tutorial<\/a>. ~ Mark Karpov (@mrkkrp). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2020\/2\/10\/converting-cabal-to-nix\">Converting Cabal to Nix!<\/a> ~ James Bowen (@james_OWA). #Haskell #Cabal #Nix<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/haskell-in-industry-riskbook\">Haskell in production: Riskbook (an interview with Jezen Thomas)<\/a>. ~ Gints Dreimanis. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/physics-history-haskell-interview\">Physics, History and Haskell<\/a>. (Interview with Rinat Stryungis). ~ Denis Oleynikov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/two-wrongs.com\/how-laziness-works\">How laziness works<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/vaibhavsagar.com\/blog\/2017\/05\/29\/imperative-haskell\/\">Imperative Haskell<\/a>. ~ Vaibhav Sagar. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.colibri.udelar.edu.uy\/jspui\/bitstream\/20.500.12008\/23002\/1\/PI%c3%9119.pdf\">Verificaci\u00f3n de estructura de redes neuronales profundas en tiempo de compilaci\u00f3n (Proyecto TensorSafe)<\/a>. ~ Leonardo Pi\u00f1eyro. #Haskell #DeepLearning<\/li>\n<li><a href=\"https:\/\/www.colibri.udelar.edu.uy\/jspui\/bitstream\/20.500.12008\/23006\/1\/VAZ19.pdf\">Mejoras al int\u00e9rprete MateFun<\/a>. ~ Nicol\u00e1s V\u00e1zquez. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/www.slideshare.net\/paulszulc\/maintainable-software-architecture-in-haskell-with-polysemy\">Maintainable software architecture in Haskell (with Polysemy)<\/a>. ~ Pawe\u0142 Szulc (@EncodePanda). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/qhB1Q4v6TEA\">Liquidate your assets (Reasoning about resource usage in Liquid Haskell)<\/a>. ~ Niki Vazou (@nikivazou). #Haskell<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org552c71b\" class=\"outline-3\">\n<h3 id=\"org552c71b\"><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=\"http:\/\/www.gigamonkeys.com\/book\/\">Practical Common Lisp<\/a>. ~ Peter Seibel. #eBook #CommonLisp<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org4ab3c27\" class=\"outline-3\">\n<h3 id=\"org4ab3c27\"><span class=\"section-number-3\">2.3<\/span> Programaci\u00f3n funcional con OCaml<\/h3>\n<div id=\"text-2-3\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/www.cs.cornell.edu\/courses\/cs3110\/2020sp\/textbook\">Functional programming in OCaml<\/a>. ~ Michael R. Clarkson. #eBook #OCaml #FunctionalProgramming<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-org7843f81\" class=\"outline-2\">\n<h2 id=\"org7843f81\"><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:\/\/logiccourse.com\/textbook\/logic-course-adventure\/\">The Logic course adventure (An active learning textbook for formal logic)<\/a>. ~ Ian Schnee. #eBook #Logic<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, del 9 al 15 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\/7031"}],"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=7031"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7031\/revisions"}],"predecessor-version":[{"id":7032,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7031\/revisions\/7032"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7031"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7031"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7031"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}