{"id":7047,"date":"2020-02-22T08:05:21","date_gmt":"2020-02-22T07:05:21","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7047"},"modified":"2020-02-22T08:05:43","modified_gmt":"2020-02-22T07:05:43","slug":"resumen-de-lecturas-compartidas-del-16-al-21-de-febrero-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-del-16-al-21-de-febrero-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas del 16 al 21 de febrero de 2020"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, del 16 al 21 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>.<br \/>\n<!--more--><\/p>\n<div id=\"outline-container-org0daae7c\" class=\"outline-2\">\n<h2 id=\"org0daae7c\"><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-org28ae97c\" class=\"outline-3\">\n<h3 id=\"org28ae97c\"><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:\/\/arxiv.org\/abs\/1902.00297\">Signatures and induction principles for higher inductive-inductive types<\/a>. ~ Ambrus Kaposi, and Andr\u00e1s Kov\u00e1cs. #ITP #Agda #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2002.06047\">Flexible coinduction in Agda<\/a>. ~ Luca Ciccone. #MSc_Thesis #ITP #Agda<\/li>\n<li><a href=\"https:\/\/whatisrt.github.io\/dependent-types\/2020\/02\/18\/agda-vs-coq-vs-idris.html\">Agda vs. Coq vs. Idris<\/a>. #ITP #Agda #Coq #Idris<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgcbe33b2\" class=\"outline-3\">\n<h3 id=\"orgcbe33b2\"><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:\/\/users.ece.utexas.edu\/~gligoric\/papers\/JainETAL20mCoqTool.pdf\">mCoq: Mutation analysis for Coq verification projects<\/a>. ~ Kush Jain et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/artagnon.com\/articles\/equality\">Equality in mechanized mathematics<\/a>. ~ Ramkumar Ramachandra. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-02478907\/document\">Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi<\/a>. ~ Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/tel.archives-ouvertes.fr\/tel-01250842v1\/document\">Certifications of programs with computational effects<\/a>. ~ Burak Ekici. #PhD_Thesis #ITP #Coq<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgf069430\" class=\"outline-3\">\n<h3 id=\"orgf069430\"><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=\"http:\/\/cl-informatik.uibk.ac.at\/users\/cek\/docs\/19\/mfck-tableaux19.pdf\">Certification of nonclausal connection tableaux proofs<\/a>. ~ Michael F\u00e4rber, and Cezary Kaliszyk. #ITP #HOL_Light<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgc46f008\" class=\"outline-3\">\n<h3 id=\"orgc46f008\"><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:\/\/svhol.pbmichel.com\/\">Isabelle\/HOL and Proof General reference [Isabelle\/HOL support wiki<\/a>]. #ITP #IsabelleHOL<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-org4b896e3\" class=\"outline-2\">\n<h2 id=\"org4b896e3\"><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-org48385a3\" class=\"outline-3\">\n<h3 id=\"org48385a3\"><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=\"https:\/\/serokell.io\/blog\/haskell-type-level-witness\">Type witnesses in Haskell<\/a>. ~ Sandeep Chandrika. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/dev.stephendiehl.com\/hask\/\">What I wish I knew when learning Haskell (Version 2<\/a>.5). ~ Stephen Diehl (@smdiehl). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cs.nott.ac.uk\/~pszgmh\/fold.pdf\">A tutorial on the universality and expressiveness of fold<\/a>. ~ Graham Hutton (1999). #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/www.cs.um.edu.mt\/~svrg\/FormalMethods\/2012-2013\/QuickCheck.pdf\">QuickCheck testing for fun and profit<\/a>. ~ John Hughes (2007). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.07488\">Profunctor optics, a categorical update<\/a>. ~ Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregian, Bartosz Milewski, Emily Pillmore, and Mario Rom\u00e1n. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2020\/02\/15\/competitive-programming-in-haskell-modular-arithmetic-part-1\/\">Competitive programming in Haskell: modular arithmetic, part 1<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2020-02-15-taba.html\">Typing TABA (There and Back Again)<\/a>. ~ Donnacha Ois\u00edn Kidney (@oisdk). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/f.hypotheses.org\/wp-content\/blogs.dir\/4029\/files\/2018\/11\/cardone_slides.pdf\">From Curry to Haskell<\/a>. ~ Felice Cardone. #Haskell #FunctionalProgramming #Logic<\/li>\n<li><a href=\"https:\/\/medium.com\/swlh\/how-to-make-mondrian-art-in-haskell-a1a5d430ac32\">How to make mondrian art in Haskell (Unleash your inner functional artist)<\/a>. ~ Marc Fichtel (@mc_razzy). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/repository.upenn.edu\/cgi\/viewcontent.cgi?article=1773&amp;context=cis_papers\">Monoids: Theme and variations (Functional Pearl)<\/a>. ~ Brent A. Yorgey (2012). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.cs.bham.ac.uk\/~mhe\/papers\/exhaustive.pdf\">Infinite sets that admit fast exhaustive search<\/a>. ~ Mart\u0131\u0301n Escard\u00f3 (2007). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.cs.tufts.edu\/%7Enr\/cs257\/archive\/john-hughes\/quick.pdf\">QuickCheck: \u0391 lightweight tool for random testing of Haskell programs<\/a>. ~ Koen Claessen and John Hughes (2000). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.fosskers.ca\/blog\/rio-en.html\">Porting to Rio<\/a>. ~ Colin Woodbury (@fosskers). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2020-02-19-linear-type-exception.html\">On linear types and exceptions<\/a>. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orga77a935\" class=\"outline-3\">\n<h3 id=\"orga77a935\"><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:\/\/lisp-univ-etc.blogspot.com\/2020\/02\/programming-algorithms-compression.html\">Programming algorithms: Compression<\/a>. ~ Vsevolod Dyomkin. #Algorithms #CommonLisp<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgb1c27f8\" class=\"outline-2\">\n<h2 id=\"orgb1c27f8\"><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:\/\/logicae.usal.es\/TICTTL\/actas\/JamesCaldwell.pdf\">Teaching natural deduction as a subversive activity<\/a>. ~ James Caldwell. #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 16 al 21 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\/7047"}],"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=7047"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7047\/revisions"}],"predecessor-version":[{"id":7049,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7047\/revisions\/7049"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7047"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7047"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7047"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}