{"id":6986,"date":"2020-02-09T06:00:07","date_gmt":"2020-02-09T05:00:07","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6986"},"modified":"2020-02-08T17:06:05","modified_gmt":"2020-02-08T16:06:05","slug":"resumen-de-lecturas-compartidas-del-1-al-8-de-febrero-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-del-1-al-8-de-febrero-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas del 1 al 8 de febrero de 2020"},"content":{"rendered":"<div id=\"content\">\nEsta entrada es una recopilaci\u00f3n de lecturas compartidas, del 1 al 8 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-orgd2c1b75\" class=\"outline-2\">\n<h2 id=\"orgd2c1b75\"><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-orgc2ee7f7\" class=\"outline-3\">\n<h3 id=\"orgc2ee7f7\"><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\/1911.00580\">Introduction to univalent foundations of mathematics with Agda<\/a>. ~ Mart\u00edn H\u00f6tzel Escard\u00f3. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.11560\">Toward a mechanized compendium of gradual typing<\/a>. ~ Jeremy G. Siek. #ITP #Agda<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org84bfd31\" class=\"outline-3\">\n<h3 id=\"org84bfd31\"><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.ps.uni-saarland.de\/~smolka\/drafts\/icl2019.pdf\">Computational type theory and interactive theorem proving with Coq (Version of August 2, 2019)<\/a>. ~ Gert Smolka. #eBook #ITP #Coq #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/ejgallego\/jscoq\">jsCoq: A port of Coq to Javascript (Run Coq in your browser)<\/a>. ~ Emilio Jes\u00fas Gallego Arias. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/ieeexplore.ieee.org\/stamp\/stamp.jsp?tp=&amp;arnumber=8970457\">A formal system of axiomatic set theory in Coq<\/a>. ~ Tianyu Sun, Wensheng Yu. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/res.mdpi.com\/d_attachment\/electronics\/electronics-09-00255\/article_deploy\/electronics-09-00255.pdf\">A formal verification framework for security issues of blockchain smart contracts<\/a>. ~ Tianyu Sun, Wensheng Yu. #ITP #Coq #Blockchain<\/li>\n<li><a href=\"https:\/\/soap.coffee\/~lthms\/posts\/MiniHTTPServer\/\">Implementing and certifying a Web server in Coq<\/a>. ~ Thomas Letan. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/staff.aist.go.jp\/reynald.affeldt\/fipc\/main.pdf\">Formalizing functional analysis structures in dependent type theory<\/a>. ~ Reynald Affeldt et als. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/Publications\/details\/Larchey-WendlingForster:2019:H10_in_Coq.html\">Hilbert&#8217;s tenth problem in Coq<\/a>. ~ Dominique Larchey-Wendling, Yannick Forster. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/Publications\/documents\/ForsterEtAl_2019_Completeness.pdf\">Completeness theorems for first-order logic analysed in constructive type theory<\/a>. ~ Yannick Forster, Dominik Kirst, Dominik Wehr. #ITP #Coq #Logic<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/Publications\/documents\/ForsterEtAl_2019_VerifiedTMs.pdf\">Verified programming of Turing machines in Coq<\/a>. ~ Yannick Forster, Fabian Kunze, Maximilian Wuttke. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/Publications\/documents\/ForsterKunzeRoth_2019_wcbv-Reasonable.pdf\">The weak call-by-value \u03bb-calculus is reasonable for both time and space<\/a>. ~ Yannick Forster, Fabian Kunze, Marc Roth. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/Publications\/documents\/ForsterKunze_2019_Certifying-extraction.pdf\">A certifying extraction with time bounds from Coq to call-by-value \u03bb-calculus<\/a>. ~ Yannick Forster, Fabian Kunze. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/extras\/fol-trakh\/\">Trakhtenbrot\u2019s theorem in Coq (A constructive approach to finite model theory)<\/a>. ~ Dominik Kirst, Dominique Larchey-Wendling. #ITP #Coq #Logic<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org9e5382e\" class=\"outline-3\">\n<h3 id=\"org9e5382e\"><span class=\"section-number-3\">1.3<\/span> DAO con Isabelle\/HOL<\/h3>\n<div id=\"text-1-3\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/matryoshka.gforge.inria.fr\/pubs\/satur_report.pdf\">A comprehensive framework for saturation theorem proving (Technical report)<\/a>. ~ Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.08983\">A formal development cycle for security engineering in Isabelle<\/a>. ~ Florian Kamm\u00fcller. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.11142\">VERONICA: Expressive and precise concurrent information flow security (Extended version with technical appendices)<\/a>. ~ Daniel Schoepe, Toby Murray, Andrei Sabelfeld. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/mediatum.ub.tum.de\/doc\/1484146\/1484146.pdf\">Formal specification, monitoring, and verification of autonomous vehicles in Isabelle\/HOL<\/a>. ~ Albert Rizaldi. #PhD_Thesis #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Subset_Boolean_Algebras.html\">A hierarchy of algebras for boolean subsets<\/a>. ~ Walter Guttmann, Bernhard M\u00f6ller. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/Christoph_Benzmueller\/publication\/338829452_Computer-supported_Analysis_of_Arguments_in_Climate_Engineering\/links\/5e2d5775a6fdcc70a14bf745\/Computer-supported-Analysis-of-Arguments-in-Climate-Engineering.pdf\">Computer-supported analysis of arguments in climate engineering<\/a>. ~ David Fuenmayor, Christoph Benzm\u00fcller. #ITP #IsabelleHOL.<\/li>\n<li><a href=\"https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1571066103000215\/pdf?md5=bcacb89b9fed98564eccf67546b89243&amp;pid=1-s2.0-S1571066103000215-main.pdf\">Towards a readable formalisation of category theory<\/a>. ~ Greg O\u2019Keefe. #ITP #IsabelleHOL #CategoryTheory<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-org6bf08fc\" class=\"outline-3\">\n<h3 id=\"org6bf08fc\"><span class=\"section-number-3\">1.4<\/span> DAO con Lean<\/h3>\n<div id=\"text-1-4\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.10490\">Beyond notations: Hygienic macro expansion for theorem proving languages<\/a>. ~ Sebastian Ullrich, Leonardo de Moura. #ITP #LeanProver<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgef576a2\" class=\"outline-3\">\n<h3 id=\"orgef576a2\"><span class=\"section-number-3\">1.5<\/span> DAO y DAT en general<\/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.10512\">Automated proof of Bell-LaPadula security properties<\/a>. ~ Maximiliano Cristi\u00e1, Gianfranco Rossi. #ATP #SetLog<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-02457240\/document\">MOIN: A nested sequent theorem prover for intuitionistic modal logics (system description)<\/a>. ~ Marianna Girlando, Lutz Stra\u00dfburger. #ATP #Prolog #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/aep\/zz\/blob\/master\/README.md\">ZZ (drunk octopus) is a modern formally provable dialect of C, inspired by Rust<\/a>. ~ Arvid E. Picciani. #ZZ #Programming #SMT #FormalVerification<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-org522c222\" class=\"outline-2\">\n<h2 id=\"org522c222\"><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-orgecc0e35\" class=\"outline-3\">\n<h3 id=\"orgecc0e35\"><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:\/\/kenta.blogspot.com\/2020\/02\/ozjcrzwx-ulam-spirals.html\">Ulam spirals<\/a>. ~ Ken T Takusagawa. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2020\/02\/07\/competitive-programming-in-haskell-primes-and-factoring\/\">Competitive Programming in Haskell: primes and factoring<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/chrispenner.ca\/posts\/kaleidoscopes\">Intro to Kaleidoscopes: Optics for aggregating data through Applicatives<\/a>. ~ Chris Penner. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/finkel-lang\/finkel%20\">Finkel: Haskell in S-expression<\/a>. #Haskell #Lisp #Finkel_lang<\/li>\n<li><a href=\"https:\/\/medium.com\/heavenlyx\/functional-programming-the-simple-version-63fe10678f6e\">Functional programming: The simple version<\/a>. ~ Muhammad Tabaza. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/odone.io\/posts\/2020-02-03-monad-composes-sequentially.html\">Why monad composes operations sequentially<\/a>. ~ Riccardo Odone. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/lorentz-implementing-smart-contract-edsl-in-haskell\">Lorentz: Implementing smart contract eDSL in Haskell<\/a>. ~ Kostya Ivanov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/slides.com\/dervism\/java-haskell?token=c5PXw4i\">Java &amp; Haskell: Similarities and differences<\/a>. ~ Dervis Mansuroglu. #Java #Haskell<\/li>\n<li><a href=\"https:\/\/thoughtbot.com\/blog\/thinking-in-types\">Thinking in types<\/a>. ~ Pat Brisbin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2020-02-06-safe-inline-java.html\">Safe memory management in inline-java using linear types<\/a>. ~ Facundo Dominguez. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/dDtZLm7HIJs\">Functional or combinator parsing<\/a>. ~ Graham Hutton. #Haskell #FunctionalProgramming<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<div id=\"outline-container-orgd18787e\" class=\"outline-3\">\n<h3 id=\"orgd18787e\"><span class=\"section-number-3\">2.2<\/span> Programaci\u00f3n l\u00f3gica con Prolog<\/h3>\n<div id=\"text-2-2\" class=\"outline-text-3\">\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/hal.inria.fr\/hal-02457240\/document\">MOIN: A nested sequent theorem prover for intuitionistic modal logics (system description)<\/a>. ~ Marianna Girlando, Lutz Stra\u00dfburger. #ATP #Prolog #Logic<\/li>\n<\/ul>\n<\/div>\n<\/div>\n<\/div>\n<div id=\"outline-container-org6c0e61c\" class=\"outline-2\">\n<h2 id=\"org6c0e61c\"><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:\/\/www.cis.upenn.edu\/~cis262\/notes\/proofslambda.pdf\">Proofs, computability, complexity, and the lambda calculus (An introduction)<\/a>. ~ Jean Gallier, Jocelyn Quaintance. #eBook #Logic #CompSci #LambdaCalculus<\/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 1 al 8 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\/6986"}],"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=6986"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6986\/revisions"}],"predecessor-version":[{"id":6988,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6986\/revisions\/6988"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6986"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6986"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6986"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}