{"id":6961,"date":"2020-02-01T12:09:23","date_gmt":"2020-02-01T11:09:23","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6961"},"modified":"2020-02-01T12:09:23","modified_gmt":"2020-02-01T11:09:23","slug":"resumen-de-lecturas-compartidas-del-25-al-31-de-enero-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-del-25-al-31-de-enero-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas del 25 al 31 de enero de 2020"},"content":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, del 25 al 31 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-org359c8a4\" class=\"outline-2\">\n<h2 id=\"org359c8a4\"><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-org0eb2062\" class=\"outline-3\">\n<h3 id=\"org0eb2062\"><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=\"http:\/\/www.staff.science.uu.nl\/~swier004\/publications\/2020-msfp-submission.pdf\">Combining predicate transformer semantics for effects: a case study in parsing regular languages<\/a>. ~ Tim Baanen, Wouter Swierstra. #Agda #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/homotopytypetheory.org\/2020\/01\/26\/the-cantor-schroder-bernstein-theorem-for-%E2%88%9E-groupoids\/\">The Cantor-Schr\u00f6der-Bernstein theorem for \u221e-groupoids<\/a>. ~ Martin Escardo. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/www.cambridge.org\/core\/journals\/journal-of-functional-programming\/article\/elaborating-dependent-copattern-matching-no-pattern-left-behind\/F13CECDAB2B6200135D45452CA44A8B3\">Elaborating dependent (co)pattern matching: No pattern left behind<\/a>. ~ Jesper Cockx, Andreas Abel. #ITP #Agda<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org2520480\" class=\"outline-3\">\n<h3 id=\"org2520480\"><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=\"https:\/\/cass.pleiad.cl\/jscoq\/examples\/funext\/lecture1.html\">First steps with Coq<\/a>. ~ Assia Mahboubi. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/Coq-Andes-Summer-School\/CASS2020\/raw\/master\/assia-intro\/slides.pdf\">Introduction to Coq<\/a>. ~ Assia Mahboubi. #ITP<\/li>\n<li><a href=\"https:\/\/github.com\/Coq-Andes-Summer-School\/CASS2020\/raw\/master\/matthieu\/depelim.pdf\">Programming with dependent types in Coq: inductive families and dependent patter-matching<\/a>. ~ Matthieu Sozeau. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/Coq-Andes-Summer-School\/CASS2020\/raw\/master\/slides_tabareau.pdf\">Homotopy Type Theory<\/a>. ~ Nicolas Tabareau. #ITP #Coq #HoTT<\/li>\n<li><a href=\"https:\/\/hal.laas.fr\/hal-02088529v2\/document\">A certificate-based approach to formally verified approximations<\/a>. ~ Florent Br\u00e9hard, Assia Mahboubi, Damien Pous. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/ruor.uottawa.ca\/bitstream\/10393\/39876\/1\/Eaman_Amir_2019_thesis.pdf\">TEpla: A certified type enforcement access-control policy language<\/a>. ~ Amir Eaman. #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/ruor.uottawa.ca\/bitstream\/10393\/39994\/1\/Lu_Weiyun_2019_thesis.pdf\">Formally verified code obfuscation in the Coq Proof Assistant<\/a>. ~ Weiyun Lu. #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/stackoverflow.com\/a\/59719944\/5157338\">Show that a monic (injective) and epic (surjective) function has an inverse in Coq<\/a>. ~ Arthur Azevedo De Amorim. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/~gaeher\/files\/3SATClique.pdf\">A formalised polynomial-time reduction from 3SAT to Clique<\/a>. ~ Lennard G\u00e4her. #ITP #Coq<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org829ff2f\" class=\"outline-3\">\n<h3 id=\"org829ff2f\"><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:\/\/arxiv.org\/abs\/2001.06702\">FASiM: A framework for automatic formal analysis of simulink models of linear analog circuits<\/a>. ~ Adnan Rashid, Ayesha Gauhar and Osman Hasan. #ITP #HOL_Light<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgf4f8d01\" class=\"outline-3\">\n<h3 id=\"orgf4f8d01\"><span class=\"section-number-3\">1.4<\/span> DAO con Idris<\/h3>\n<div id=\"text-1-4\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/arxiv.org\/abs\/1912.10961\">Formalizing the Curry-Howard correspondence<\/a>. ~ Juan Ferrer Meleiro, Hugo Luiz Mariano. #ITP #Idris #Logic<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org6be4141\" class=\"outline-3\">\n<h3 id=\"org6be4141\"><span class=\"section-number-3\">1.5<\/span> DAO con Isabelle\/HOL<\/h3>\n<div id=\"text-1-5\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.10834\">Smart induction for Isabelle\/HOL (System description)<\/a>. ~ Yutaka Nagashima. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/era.ed.ac.uk\/bitstream\/handle\/1842\/22936\/Raggi2016.pdf\">Searching the space of representations: reasoning through transformations for mathematical problem solving<\/a>. ~ Daniel Raggi. #PhD_Thesis #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.09715\">Formalization of forcing in Isabelle\/ZF<\/a>. ~ Emmanuel Gunther, Miguel Pagano, Pedro S\u00e1nchez Terraf. #ITP #IsabelleZF #Logic<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org9183075\" class=\"outline-3\">\n<h3 id=\"org9183075\"><span class=\"section-number-3\">1.6<\/span> DAO con Lean<\/h3>\n<div id=\"text-1-6\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.07655\">Coherence via wellfoundedness<\/a>. ~ Nicolai Kraus, Jakob von Raumer. #ITP #LeanProver #Math<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgf25a05f\" class=\"outline-3\">\n<h3 id=\"orgf25a05f\"><span class=\"section-number-3\">1.7<\/span> DAO en general<\/h3>\n<div id=\"text-1-7\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.05970\">HolPy: Interactive theorem proving in Python<\/a>. ~ Bohua Zhan. #ITP #HolPy #Logic #Python<\/li>\n<li><a href=\"https:\/\/blog.sigplan.org\/2020\/01\/29\/mechanized-proofs-for-pl-past-present-and-future\/\">Mechanized proofs for PL: Past, present, and future<\/a>. ~ Talia Ringer. #ITP<\/li>\n<li><a href=\"https:\/\/bor0.wordpress.com\/2020\/01\/31\/introduction-and-formalization-of-boolean-algebra\/\">Introduction and formalization of Boolean algebra<\/a>. ~ Boro Sitnikovski (@BSitnikovski). #ITP #Metamath #Math<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-org77af97c\" class=\"outline-2\">\n<h2 id=\"org77af97c\"><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-org03e0b58\" class=\"outline-3\">\n<h3 id=\"org03e0b58\"><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:\/\/blog.ezyang.com\/2020\/01\/vmap-in-haskell\">vmap in Haskell<\/a>. ~ Edward Z. Yang (@ezyang). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/oleg.fi\/gists\/posts\/2020-01-25-case-study-migration-from-lens-to-optics.html\">Case study: migrating from lens to optics<\/a>. ~ Oleg Grenrus (@phadej). #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.07488\">Profunctor optics, a categorical update<\/a>. ~ Bryce Clarke et als. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/bytes.yingw787.com\/posts\/2020\/01\/30\/a_review_of_haskell\/\">A Pythonista&#8217;s Review of Haskell<\/a>. ~ Ying Wang. #Haskell #Python<\/li>\n<li><a href=\"https:\/\/cs-syd.eu\/posts\/2020-01-28-property-testing-size\">Property testing in depth: The size parameter<\/a>. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2020-01-29-terminating-tricky-traversals.html\">Terminating tricky traversals<\/a>. ~ Donnacha Ois\u00edn Kidney (@oisdk). #Haskell #Agda #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/golem.ph.utexas.edu\/category\/2020\/01\/profunctor_optics_the_categori.html\">Profunctor optics: The categorical view<\/a>. ~ Emily Pillmore and Mario Rom\u00e1n. #Haskell #FunctionalProgramming #CategoryTheory<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/developing-ghc-for-a-living\">Developing GHC for a Living: Interview with Vladislav Zavialov<\/a>. ~ Denis Oleynikov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/haskell-in-production-centralapp\">Haskell in production: CentralApp<\/a>. ~ Ashesh Ambasta (@AsheshAmbasta), Gints Dreimanis. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/tech.fpcomplete.com\/blog\/transformations-on-applicative-concurrent-computations\">Transformations on applicative concurrent computations<\/a>. ~ Rom\u00e1n Gonz\u00e1lez. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.research-collection.ethz.ch\/bitstream\/handle\/20.500.11850\/392353\/1\/Hossle_Nora.pdf\">Multiple address spaces in a distributed capability system<\/a>. ~ Nora Hossle. #MsC_Thesis #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2020-01-30-haskell-profiling.html\">Locating performance bottlenecks in large Haskell codebases<\/a>. ~ Juan Raphael Diaz Sim\u00f5es. #Haskell #FunctionalProgramming<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-org5a70bc8\" class=\"outline-2\">\n<h2 id=\"org5a70bc8\"><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:\/\/github.com\/Coq-Andes-Summer-School\/CASS2020\/raw\/master\/typesets.pdf\">Set Theory vs. Type Theory<\/a>. Alexandre Miquel. #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/www.irif.fr\/~emiquey\/content\/banner.pdf\">Realizabilidad cl\u00e1sica y efectos colaterales: Extendiendo la correspondencia de Curry-Howard<\/a>. ~ \u00c9tienne Miquey. #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/www.irif.fr\/~emiquey\/content\/imerl18.pdf\">Curry-Howard: unveiling the computational content of proofs<\/a>. ~ \u00c9tienne Miquey. #CompSci<\/li>\n<li><a href=\"https:\/\/www.irif.fr\/~emiquey\/content\/lmw19.pdf\">The benefits of sequent calculus<\/a>. ~ \u00c9tienne Miquey. #Logic #CompSci<\/li>\n<\/ul>\n<\/div>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, del 25 al 31 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\/6961"}],"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=6961"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6961\/revisions"}],"predecessor-version":[{"id":6962,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6961\/revisions\/6962"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6961"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6961"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6961"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}