{"id":7603,"date":"2021-05-01T19:28:56","date_gmt":"2021-05-01T17:28:56","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7603"},"modified":"2021-08-30T19:30:04","modified_gmt":"2021-08-30T17:30:04","slug":"resumen-de-lecturas-compartidas-durante-abril-de-2021","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-abril-de-2021\/","title":{"rendered":"Resumen de lecturas compartidas durante abril de 2021"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante abril de 2021, 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>Las lecturas est\u00e1n ordenadas seg\u00fan su fecha de publicaci\u00f3n en <a href=\"https:\/\/twitter.com\/Jose_A_Alonso\">Twitter<\/a>.<\/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<ul class=\"org-ul\">\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.14445\">Trakhtenbrot&#8217;s theorem in Coq: Finite model theory through the constructive lens<\/a>. ~ Dominik Kirst, Dominique Larchey-Wendling. #ITP #Coq #Logic #Math<\/li>\n<li><a href=\"https:\/\/github.com\/youtakaoka\/topos\">Topos: Programming language which can treat set and topology<\/a>. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/notes.srid.ca\/ema-announce\">Announcing Ema &#8211; Static sites in Haskell<\/a>. ~ Sridhar Ratnakumar. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/z.haskell.world\/design\/2021\/04\/20\/introduce-BIO-a-simple-streaming-abstraction.html\">Introduce BIO: A simple streaming abstraction<\/a>. ~ Dong Han. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/bit.ly\/3344TyV\">We are happy being poor: El problema de Erd\u00f6s-Faber-Lov\u00e1sz<\/a>. ~ Juan Arias de Reyna. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.13792\">A mechanised proof of G\u00f6del&#8217;s incompleteness theorems using Nominal Isabelle<\/a>. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.13851\">Verified approximation algorithms<\/a>. ~ Robin E\u00dfmann, Tobias Nipkow, Simon Robillard. #ITP #IsabelleHOL #Algorithms<\/li>\n<li><a href=\"https:\/\/iwilare.com\/bsc-thesis.pdf\">Formalizations of the Church-Rosser theorem in Agda<\/a>. ~ Andrea Laretto. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.13645\">Learning from \u0141ukasiewicz and Meredith: Investigations into proof structures (Extended version)<\/a>. ~ Christoph Wernhard, Wolfgang Bibel. #ATP #Prover9 #Logic<\/li>\n<li><a href=\"https:\/\/www.educative.io\/blog\/haskell-tutorial\">Haskell tutorial: Get started with functional programming<\/a>. ~ Ryan Thelin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.math.umd.edu\/~jda\/seminarNotes\/carneiro.pdf\">Mathematics in the computer<\/a>. ~ Mario Carneiro. #Math #ITP #LeanProver #Metamath #Metamath_Zero<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.13117\">A verified decision procedure for orders in Isabelle\/HOL<\/a>. ~ Lukas Stevens, Tobias Nipkow. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/GaleStewart_Games.html\">Gale-Stewart games (in Isabelle\/HOL)<\/a>. ~ Sebastiaan Joosten. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/youtu.be\/N7orNWIur-c\">Induction and collection up to definable elements: calibrating the strength of parameter-free \u0394n-minimization<\/a>. ~ Andr\u00e9s Cord\u00f3n. #Logic #Math<\/li>\n<li><a href=\"https:\/\/novo.manzano.pro.br\/wp\/download\/logica-de-programacao-funcional-programe-em-hope\/\">L\u00f3gica de programa\u00e7\u00e3o funcional: Programe em Hope<\/a>. ~ Jos\u00e9 Augusto N. G. Manzano, Jos\u00e9 A. Alonso. #Hope #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/J-AugustoManzano\/hope_programe\">C\u00f3digo fonte do livro &#8220;L\u00f3gica de programa\u00e7\u00e3o funcional: Programe em Hope&#8221;<\/a>. ~ Jos\u00e9 Augusto N. G. Manzano. #Hope #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www21.in.tum.de\/~rosskops\/papers\/metalogic_pre.pdf\">Isabelle&#8217;s metalogic: Formalization and proof checker<\/a>. ~ Tobias Nipkow, Simon Ro\u00dfkopf. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/youtu.be\/1SCvFDZDLgQ\">Mathematical structures in dependent type theory<\/a>. ~ Assia Mahboubi. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/academic.oup.com\/iwc\/advance-article\/doi\/10.1093\/iwcomp\/iwab012\/6232199\">Balancing the formal and the informal in user-centred design<\/a>. ~ M.D. Harrison, P. Masci, J.C. Campos. #ITP #PVS<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/magazines\/2021\/5\/252165-a-satisfying-result\/fulltex\">A satisfying result<\/a>. ~ Don Monroe.t#.YIeLaVxXfk0.twitter #Math #CompSci #SATSolvers<\/li>\n<li><a href=\"https:\/\/www.investigacionyciencia.es\/noticias\/el-producto-de-matrices-en-pos-de-una-meta-mtica-19718\">El producto de matrices, en pos de una meta m\u00edtica<\/a>. ~ Kevin Hartnett. #Matem\u00e1ticas #Computaci\u00f3n<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.11613\">A formalised theorem in the partition calculus<\/a>. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/BenOr_Kozen_Reif.html\">The BKR decision procedure for univariate real arithmetic (in Isabelle\/HOL)<\/a>. ~ Katherine Cordwell, Yong Kiam Tan, Andr\u00e9 Platzer. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/44fb3tI2Cak\">Grandes ideas de la Filosof\u00eda: L\u00f3gica<\/a>. #L\u00f3gica<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/2ecd65e6de2939f09df9d964782f8ec7ba4aeb5c\/archive\/imo\/imo2001_q2.lean\">Formalization in Lean of IMO 2001 Q2<\/a>. ~ Tian Chen. #ITP #LeanProver #Math #IMO<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2002.09282\">Homotopy Type Theory in Isabelle<\/a>. ~ Joshua Chen. #ITP #IsabelleHOL #HoTT<\/li>\n<li><a href=\"https:\/\/pp.ipd.kit.edu\/uploads\/publikationen\/dieterichs21masterarbeit.pdf\">Formal verification of pattern matching analyses<\/a>. ~ Henning Dieterichs. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/~smolka\/drafts\/icl2021.pdf\">Modeling and proving in computational type theory using the Coq proof assistant<\/a>. ~ Gert Smolka. #eBook #ITP #Coq<\/li>\n<li><a href=\"https:\/\/tel.archives-ouvertes.fr\/tel-03202580\/document\">Formalisation en Coq des algorithmes de filtre num\u00e9rique calcul\u00e9s en pr\u00e9cision finie<\/a>. ~ Diane Gallois-Wong. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/lmcs.episciences.org\/7383\/pdf\">Logic for exact real arithmetic<\/a>. ~ Helmut Schwichtenberg, Franziskus Wiesnet. #ITP #MinLog #Haskell<\/li>\n<li><a href=\"https:\/\/home.sandiego.edu\/~shulman\/papers\/induction.pdf\">Induction on equality<\/a>. #Logic #Math #CompSci<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.11157\">Ackermann&#8217;s function in iterative form: A proof assistant experiment<\/a>. ~ Lawrence C Paulson. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.danielbrice.net\/blog\/of-function-instances-and-abstract-syntax\/\">Of function instances and abstract syntax<\/a>. ~ Daniel Brice. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/type-families-haskell\">Type families in Haskell: The definitive guide<\/a>. ~ Vladislav Zavialov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.poberezkin.com\/posts\/2021-04-21-what-i-wish-somebody-told-me-when-i-was-learning-Haskell.html\">What I wish somebody told me when I was learning Haskell<\/a>. ~ Evgeny Poberezkin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/spectrum.ieee.org\/tech-talk\/artificial-intelligence\/machine-learning\/the-state-of-ai-in-15-graphs\">15 graphs you need to see to understand AI in 2021<\/a>. ~ Eliza Strickland. #AI<\/li>\n<li><a href=\"https:\/\/www.pointedset.ca\/blog\/2020\/02\/06\/proptype.html\">A practical difference between Props and Types in Lean<\/a>. ~ Mathieu Guay-Paquet. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/afa6b72e20728cf46912ef9333d0f08ccebf7a6f\/src\/geometry\/euclidean\/sphere.lean\">Product of segments of chords in Lean<\/a>. ~ Manuel Candales. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.haskellforall.com\/2021\/04\/the-end-of-history-for-programming.html\">The end of history for programming<\/a>. ~ Gabriel Gonzalez. #Programming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.09366\">Simple type theory is not too simple: Grothendieck&#8217;s schemes without dependent types<\/a>. ~ Anthony Bordg, Lawrence Paulson, Wenda Li. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/github.com\/mirefek\/sokoban.lean\">Sokoban implementation in Lean for proving solvability \/ unsolvability<\/a>. ~ Miroslav Ol\u0161\u00e1k. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/cdsmithus.medium.com\/continued-fractions-haskell-equational-reasoning-property-testing-and-rewrite-rules-in-action-77a16d750e3f\">Continued fractions: Haskell, equational reasoning, property testing, and rewrite rules in action<\/a>. ~ Chris Smith. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/geekculture\/a-random-tour-of-typeclass-in-haskell-87a5a2125e1a\">A random tour of typeclass in Haskell<\/a>. ~ Ong Yi Ren. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/alpha2phi.medium.com\/writing-technical-documentation-with-emacs-276f13284e54\">Writing technical documentation with Emacs<\/a>. #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2021\/04\/18\/induction-on-equality\/\">Induction on equality<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.05256\">A Coq formalization of Lebesgue integration of nonnegative functions<\/a>. ~ Sylvie Boldo, Fran\u00e7ois Cl\u00e9ment, Florian Faissole, Vincent Martin, Micaela Mayero. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.cs.columbia.edu\/~rgu\/publications\/oakland21-li.pdf\">A secure and formally verified Linux KVM hypervisor<\/a>. ~ Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, John Zhuang Hui. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.05516\">Machine-checked ZKP for NP-relations: Formally verified security proofs and implementations of MPC-in-the-head<\/a>. ~ Jos\u00e9 Carlos Bacelar Almeida et als. #EasyCrypt<\/li>\n<li><a href=\"https:\/\/www.easycrypt.info\">EasyCrypt: Computer-aided cryptographic proofs<\/a>. #EasyCrypt<\/li>\n<li><a href=\"https:\/\/www.easycrypt.info\/downloads\/tutorial\/tutorial-prg.pdf\">EasyCrypt: A tutorial<\/a>. ~ Gilles Barthe et als. #EasyCrypt<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.05207\">Online machine learning techniques for Coq: A comparison<\/a>. ~ Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop \u010cern\u00fd, Cezary Kaliszyk, Josef Urban. #ITP #Coq #MachineLearning<\/li>\n<li><a href=\"https:\/\/turcomat.org\/index.php\/turkbilmat\/article\/download\/2435\/2138\">Balanced Academic Curriculum: Looking for an optimal solution with metaheuristics and functional programming<\/a>. ~ Jos\u00e9 Miguel Rubio, Cristian Vidal-Silva, Luis Carter, Miguel Tupac-Yupanqui. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/gallais.github.io\/blog\/poltergeist-types\">Poltergeist types<\/a>. ~ G. Allais. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/ec-jones.github.io\/flocking.html\">Functional flocks<\/a>. ~ Eddie Jones. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/aadaa-fgtaa.github.io\/blog\/optionally\/\">Checking for uncheckable: optional constraints<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/type-theory\/\">Type theory<\/a>. ~ Thierry Coquand. #TypeTheory<\/li>\n<li><a href=\"https:\/\/functional.works-hub.com\/learn\/more-on-types-typeclasses-and-the-foldable-typeclass-e1862\">More on types, typeclasses and the foldable typeclass<\/a>. ~ Marty Stumpf. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/chrisdone.com\/posts\/the-movement-principle\/\">The movement principle<\/a>. ~ Chris Done. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/blog\/2021-04-15-arrows-through-a-different-lens\/\">Arrows, through a different lens<\/a>. ~ Juan Raphael Diaz Sim\u00f5es. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/blog\/2021-04-08-capabilities-ad-hoc-interpreters\/\">Ad-hoc interpreters with capability<\/a>. ~ Ga\u00ebl Deest, Andreas Herrmann. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.math.dev\/lisp-the-web-4c00c88d11f9\">Lisp &amp; the Web (Introductory reference guide to creating Web applications with Common Lisp &amp; Google Compute Engine)<\/a>. ~ Ashok Khanna. #CommonLisp #Programming<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/mathematician-disproves-group-algebra-unit-conjecture-20210412\/\">Mathematician disproves 80-year-old algebra conjecture<\/a>. ~ Erica Klarreich. #Math<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/8d3e8b5b2635fc20a27922893cdf852bd0bd5706\/archive\/imo\/imo1977_q6.lean\">Formalization in Lean of IMO 1977 Q6<\/a>. ~ Tian Chen. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/3379f3ed992a6bce819a030178082efb6f6a92b4\/archive\/100-theorems-list\/57_herons_formula.lean\">Heron&#8217;s Formula (in Lean)<\/a>. ~ Matt Kempster. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/culturacientifica.com\/2013\/04\/24\/para-que-sirven-las-matematicas\/\">\u00bfPara qu\u00e9 sirven las matem\u00e1ticas?<\/a> ~ Marta Macho Stadler. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/David-Fuenmayor\/publication\/349043183_Topological_semantics_for_paraconsistent_and_paracomplete_logics_in_IsabelleHOL\/links\/606c0941458515614d3a53c9\/Topological-semantics-for-paraconsistent-and-paracomplete-logics-in-Isabelle-HOL.pdf\">Topological semantics for paraconsistent and paracomplete logics in Isabelle\/HOL<\/a>. ~ David Fuenmayor. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/jonascarpay.com\/posts\/2021-01-28-haskell-project-template.html\">The working programmer\u2019s guide to setting up Haskell projects<\/a>. ~ Jonas Carpay. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/jrsinclair.com\/articles\/2019\/what-i-wish-someone-had-explained-about-functional-programming\/\">Things I wish someone had explained about functional programming (Part 1: Faulty assumptions)<\/a>. ~ James Sinclair. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/jrsinclair.com\/articles\/2019\/algebraic-structures-what-i-wish-someone-had-explained-about-functional-programming\/\">Things I wish someone had explained about functional programming (Part 2: Algebraic structures)<\/a>. ~ James Sinclair. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/jrsinclair.com\/articles\/2019\/type-classes-what-i-wish-someone-had-explained-about-functional-programming\/\">Things I wish someone had explained about functional programming (Part 3: Type classes)<\/a>. ~ James Sinclair. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/jrsinclair.com\/articles\/2019\/algebraic-data-types-what-i-wish-someone-had-explained-about-functional-programming\/\">Things I wish someone had explained about functional programming (Part 4: Algebraic data types)<\/a>. ~ James Sinclair. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/quchen\/generative-art\">Generative art using Haskell<\/a>. ~ David Luposchainsky. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blogs.elconfidencial.com\/tecnologia\/tribuna\/2021-04-13\/programador-software-consultoria-producto-universidad_3030868\/\">Programar es de pobres: por qu\u00e9 el mundo del &#8216;software&#8217; est\u00e1 roto en Espa\u00f1a<\/a>. ~ Eduardo Manch\u00f3n. #Programaci\u00f3n #Inform\u00e1tica<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/e269dbc17a978dfabe57975b84d0b0250b78a2db\/src\/tactic\/itauto.lean\">Intuitionistic tautology (`itauto`) decision procedure in Lean<\/a>. ~ Mario Carneiro. #ITP #LeanProver #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.04095\">First-order natural deduction in Agda<\/a>. ~ Louis Warren. #ITP #Agda #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/BartoszMilewski\/Publications\/tree\/master\/TheDaoOfFP\">The Dao of functional programming<\/a>. ~ Bartosz Milewski. #Haskell #FunctionalProgramming #CategoryTheory<\/li>\n<li><a href=\"https:\/\/www.brynmawr.edu\/cs\/resources\/beauty-of-programming\">The beauty of programming<\/a>. ~ Linus Torvalds. #Programming<\/li>\n<li><a href=\"https:\/\/www.vidal-rosset.net\/gnus_emacs_as_email_client_in_imap_with_protonmail.html\">Gnus Emacs as email client in IMAP with ProtonMail<\/a>. ~ Joseph Vidal-Rosset. #Emacs #ProtonMail<\/li>\n<li><a href=\"https:\/\/osa1.net\/posts\/2021-04-10-sums-and-products.html\">Products and sums, named and anonymous<\/a>. ~ \u00d6mer Sinan A\u011facan. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.02549\">Connecting constructive notions of ordinals in Homotopy Type Theory<\/a>. ~ Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. #ITP #Agda #Logic #Math #HoTT<\/li>\n<li><a href=\"https:\/\/49jaiio.sadio.org.ar\/pdfs\/saei\/SAEI-12.pdf\">Propuesta de ense\u00f1anza de la formalizaci\u00f3n de la Matem\u00e1tica utilizando un asistente de pruebas en estudiantes de la Licenciatura en Ciencias de la Computaci\u00f3n<\/a>. ~ Daniel Sever\u0131n, Alejandro Hern\u00e1ndez. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/c6b06369392473fe9ebc480fbcfed1695db3e554\/archive\/imo\/imo2008_q3.lean\">Formalization in Lean of IMO 2008 Q3<\/a>. ~ Manuel Candales. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.01112\">NaturalProofs: Mathematical theorem proving in natural language<\/a>. ~ Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, Kyunghyun Cho. #ATP #MachineLearning<\/li>\n<li><a href=\"https:\/\/youtu.be\/79ymkGQW3b4\">Type theory from the perspective of Artificial Intelligence<\/a>. ~ David McAllester. #TypeTheory #AI<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.02466\">A review of formal methods applied to machine learning<\/a>. ~ Caterina Urban, Antoine Min\u00e9. #MachineLearning #FormalMethods<\/li>\n<li><a href=\"https:\/\/youtu.be\/nmBkU-l1zyc\">Prolog meta-interpreters<\/a>. ~ Markus Triska. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Grothendieck_Schemes.html\">Grothendieck&#8217;s Schemes in Algebraic Geometry<\/a>. ~ Anthony Bordg, Lawrence Paulson, Wenda Li. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/code.world\/haskel\">Continued fractions in Haskell<\/a>. ~ Chris Smith.l#P7oZc6pbWBK6wRaBBMm0goA #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/bor0.wordpress.com\/2021\/04\/09\/algorithmic-puzzle-continuous-increasing-subsequences\/\">Algorithmic puzzle: Continuous increasing subsequences<\/a>. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.haskellforall.com\/2021\/04\/how-to-replace-proxy-with.html\">How to replace Proxy with AllowAmbiguousTypes<\/a>. ~ Gabriel Gonzalez. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/a6024f10dde5322da06d1158221e1827d3ba4cfe\/archive\/imo\/imo2008_q4.lean\">Formalization in Lean of IMO 2008 Q4<\/a>. ~ Manuel Candales. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/gilmi.me\/blog\/post\/2021\/04\/06\/giml-type-inference\">Giml&#8217;s type inference engine<\/a>. ~ Gil Mizrahi. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/jimburton\/scrabble\">Scrabb\u03bbe: A one- or two-player implementation of Scrabble for teaching functional programming<\/a>. ~ Jim Burton. #eBook #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.00506v1\">Intuitionistic NF Set Theory<\/a>. ~ Michael Beeson. #Logic #Math #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/82fd6e1e1b9b35249e25d1e19af1df0eb7cf2a15\/src\/logic\/girard.lean\">Girard&#8217;s paradox<\/a>. ~ Mario Carneiro. #ITP #LeanProver #Logic #Math<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/89ea423d261b46c4e90e49362a6471a5ceb1d6d5\/archive\/imo\/imo2005_q3.lean\">Formalization in Lean of IMO 2005 Q3<\/a>. ~ Manuel Candales. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/1e1eaae6ad91319c1f3cc2f414a0f763b8f15641\/archive\/imo\/imo2008_q2.lean\">Formalization in Lean of IMO 2008 Q2<\/a>. ~ Manuel Candales. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/1e1eaae6ad91319c1f3cc2f414a0f763b8f15641\/archive\/imo\/imo2011_q5.lean\">Formalization in Lean of IMO 2011 Q5<\/a>. ~ Alain Verberkmoes. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/bor0.wordpress.com\/2021\/04\/05\/capturing-number-theory-in-haskell\/%20https:\/\/bor0.wordpress.com\/2021\/04\/05\/capturing-number-theory-in-haskell\/\">Capturing number theory in Haskell<\/a>. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/erick.navarro.io\/blog\/auto-build-and-publish-emacs-org-configuration-as-a-website\/\">Auto build and publish emacs org configuration as a website<\/a>. ~ Erick Navarro. #Emacs<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-03184956\/document\">Division by zero in Logic and Computing<\/a>. ~ Jan Bergstra. #Logic #Math #CompSci<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2021\/04\/03\/induction-and-inductive-types\/\">Induction, and inductive types<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/LZMtQNdqtvc\">Doing mathematics with simple types: Infinitary combinatorics in Isabelle\/HOL<\/a>. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.01052\">An evaluation of the Archive of Formal Proofs<\/a>. ~ Carlin MacKenzie, Jacques Fleuriot, James Vaughan. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/taylor.fausak.me\/2021\/04\/03\/default-exception-handler-in-haskell\/\">Default exception handler in Haskell<\/a>. ~ Taylor Fausak. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/home.fnal.gov\/~neilsen\/notebook\/orgExamples\/org-examples.html\">Emacs org-mode examples and cookbook<\/a>. ~ Eric H. Neilsen, Jr. #Emacs<\/li>\n<li><a href=\"https:\/\/repositorioaberto.uab.pt\/bitstream\/10400.2\/9925\/1\/TD_IvoRobert.pdf\">ProverX: Rewriting and extending Prover9<\/a>. ~ Ivo Robert. #PhDThesis #ATP #Prover9<\/li>\n<li><a href=\"https:\/\/eprint.iacr.org\/2021\/397.pdf\">SSProve: A foundational framework for modular cryptographic proofs in Coq<\/a>. ~ Carmine Abate et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/J-AugustoManzano\/hope\">C\u00f3digo fonte do livro &#8220;L\u00f3gica de programa\u00e7\u00e3o funcional: Pense em Hope&#8221;<\/a>. ~ Jos\u00e9 Augusto N. G. Manzano. #Hope #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/gallais.github.io\/pdf\/draft_sigbovik21.pdf\">Dependent stringly-typed programming<\/a>. ~ @anormalform. #Agda #FunctionalProgramming #ITP<\/li>\n<li><a href=\"https:\/\/www.stephanschiffels.de\/posts\/2021-03-24-Haskell-CLI\/\">Designing command line interfaces in Haskell<\/a>. ~ Stephan Schiffels. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/boris-marinov.github.io\/category-theory-illustrated\/04_order\/\">Category theory illustrated<\/a>. ~ Boris Marinov. #CategoryTheory<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/category-theory\">#SEP: Category theory<\/a>. ~ Jean-Pierre Marquis. #CategoryTheory #Logic #Math<\/li>\n<\/ul>\n<\/div>\n<div id=\"postamble\" class=\"status\"><\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante abril de 2021, en Twitter fundamentalmente sobre programaci\u00f3n funcional y demostraci\u00f3n asistida por ordenador. Las lecturas est\u00e1n ordenadas seg\u00fan su fecha de publicaci\u00f3n en Twitter. Al final de cada art\u00edculo se encuentran etiquetas relativas a los sistemas que usa o a su contenido. Una recopilaci\u00f3n de&#8230;<\/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":[6],"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\/7603"}],"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=7603"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7603\/revisions"}],"predecessor-version":[{"id":7604,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7603\/revisions\/7604"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7603"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7603"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7603"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}