{"id":7207,"date":"2020-05-01T18:17:07","date_gmt":"2020-05-01T16:17:07","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7207"},"modified":"2020-08-01T18:18:49","modified_gmt":"2020-08-01T16:18:49","slug":"resumen-de-lecturas-compartidas-durante-abril-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-abril-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas durante abril de 2020"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante abril de 2020, 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:\/\/humanreadablemag.com\/issues\/2\/articles\/theres-a-mathematician-in-your-compiler\">There&#8217;s a mathematician in your compiler<\/a>. ~ James Phillips. #Logic #Math #CompSci #Scala #FunctionalProgramming via @FunctorFact<\/li>\n<li><a href=\"http:\/\/www.joachim-breitner.de\/blog\/768-Animations_in_Kaleidogen\">Animations in Kaleidogen<\/a>. ~ Joachim Breitner (@nomeata). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/psmu_VAuiag\">Curried functions<\/a>. ~ Graham Hutton (@haskellhutt). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/frasertweedale.github.io\/blog-fp\/posts\/2020-03-31-quickcheck-hedgehog.html\">Migrating from QuickCheck to Hedgehog: mixed results<\/a>. ~ Fraser Tweedale (@hackuador). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.lix.polytechnique.fr\/Labo\/Dale.Miller\/papers\/icdcit-2020.pdf\">A distributed and trusted web of formal proofs<\/a>. ~ Dale Miller. #ITP #Logic #Math #CompSci<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2004.00055\">Explosive proofs of mathematical truths<\/a>. ~ Scott Viteri, Simon DeDeo. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/blanchette\/logical_verification_2020\/raw\/master\/hitchhikers_guide.pdf\">The Hitchhiker\u2019s Guide to Logical Verification<\/a>. ~ Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes H\u00f6lzl. #eBook #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/staff.aist.go.jp\/reynald.affeldt\/documents\/cproba_preprint.pdf\">Reasoning with conditional probabilities and joint distributions in Coq<\/a>. ~ Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/rubenpieters.github.io\/assets\/papers\/JFP20-handlers.pdf\">Generalized monoidal effects and handlers<\/a>. ~ Ruben P. Pieters, Tom Schrijvers, Exequiel Rivas. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/h2.jaguarpaw.co.uk\/posts\/refactoring-neural-network\/\">Refactoring a neural network implementation in Haskell<\/a>. ~ The H2 Wiki. #Haskell #FunctionalProgramming #NeuralNetwork<\/li>\n<li><a href=\"https:\/\/lispnews.wordpress.com\/2020\/04\/02\/acm-open-access-to-lfp\/\">ACM Open access to LFP (Conference on LISP and Functional Programming)<\/a>. #Lisp #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/jackkelly.name\/blog\/archives\/2020\/04\/03\/the_power_of_tiny_dsls\/index.html\">The power of tiny DSLs<\/a>. ~ Jack Kelly. #Haskell #CodeWorld<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/doi\/book\/10.1145\/2841316\">Verified functional programming in Agda<\/a>. ~ Aaron Stump. #eBook #ITP #Agda<\/li>\n<li><a href=\"https:\/\/youtu.be\/wvXZn4OdExU\">El problema de Basilea<\/a>. ~ Urtzi Buijs (@UrtziBuijs). #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/www.bates.edu\/mathematics\/resources\/latex-manual\/\">The Bates LaTeX Manual<\/a>. #LaTeX<\/li>\n<li><a href=\"https:\/\/github.com\/fp-works\/function-composition-cheatsheet\">Composition of functions cheatsheet<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/ahelwer.ca\/post\/2020-04-05-lean-assignment\/\">Doing a math assignment with the Lean theorem prover<\/a>. ~ Andrew Helwer (@ahelwer). #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/rgoswami.me\/posts\/jupyter-orgmode\/\">Replacing Jupyter with Orgmode<\/a>. ~ Rohit Goswami (@rg0swami). #Emacs #OrgMode #Python<\/li>\n<li><a href=\"https:\/\/www.mimuw.edu.pl\/~lukaszcz\/sauto.pdf\">Practical proof search for Coq by type inhabitation<\/a>. ~ Lukasz Czajka. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/youtu.be\/cHfZEdxtVjU\">Haskell: Why monad composes operations sequentially<\/a>. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/chrisdornan.com\/posts\/2020-04-06-pointless.html\">Pointless style<\/a>. ~ Chris Dornan (@CDornan). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/jessewarden.com\/2020\/03\/write-unbreakable-python.html\">Write unbreakable Python<\/a>. ~ Jesse Warden (@jesterxl). #Python #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/chrisdornan.com\/posts\/2020-04-05-sr-Functor.html\">Functor (expanded)<\/a>. ~ Chris Dornan (@CDornan). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.freecodecamp.org\/news\/projecteuler100-coding-challenge-competitive-programming\/\">Introducing the #ProjectEuler100 challenge: the &#8220;dark souls&#8221; of coding achievements<\/a>. ~ Quincy Larson (@ossia). #Programming #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2004.03673\">Maintaining a library of formal mathematics<\/a>. ~ Floris van Doorn, Gabriel Ebner, Robert Y. Lewis. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.youtube.com\/playlist?list=PLvROQ_RldgC8KYmkQsF_zKqAXD_Xphr9n\">Coursework: The power and limits of Logic<\/a>. ~ Greg Restall (@consequently). #Logic<\/li>\n<li><a href=\"https:\/\/youtu.be\/wA4WLJFjGrE\">Key benefits of working in Haskell<\/a>. ~ Sreenidhi Nair (@ersran9). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/people.irisa.fr\/Jean-Christophe.Lechenet\/files\/IJCAR_2020.pdf\">A fast verified liveness analysis in SSA form<\/a>. ~ Jean-Christophe L\u00e9chenet, Sandrine Blazy, David Pichardie. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/ilyasergey.net\/papers\/ceramist-draft.pdf\">Certifying certainty and uncertainty in approximate membership query structures<\/a>. ~ Kiran Gopinathan, Ilya Sergey. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/bit.ly\/34tY6yH\">The interplay between logic and computation<\/a>. ~ Zena M. Ariola. #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/joshbradley.me\/understanding-the-power-of-lisp\/\">Understanding the power of LISP<\/a>. ~ @josh_b_rad. #Lisp<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Saturation_Framework.html\">A comprehensive framework for saturation theorem proving<\/a>. ~ Sophie Tourret. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/www.youtube.com\/playlist?list=PLIb_io8a5NB2DddFf-PwvZDCOUNT1GZoA\">Esencia del \u00e1lgebra lineal<\/a>. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/bit.ly\/2UZum9I\">Fundamentals of Artificial Intelligence<\/a>. ~ K.R. Chowdhary. #AI #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2004.02983\">Integrating Owicki-Gries for C11-style memory models into Isabelle\/HOL<\/a>. ~ Sadegh Dalvandi, Brijesh Dongol, Simon Doherty. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1909.01743\">Verifying the DPLL algorithm in Dafny<\/a>. ~ Cezar-Constantin Andrici, \u015etefan Ciob\u00e2c\u0103. #Dafny #Verification<\/li>\n<li><a href=\"https:\/\/bit.ly\/3c9CcmF\">Herramientas de razonamiento autom\u00e1tico en GeoGebra: qu\u00e9 son y para qu\u00e9 sirven<\/a>. ~ M. Pilar V\u00e9lez, Tom\u00e1s Recio, Steven Van Vaerenbergh. #Razonamiento_autom\u00e1tico #GeoGebra<\/li>\n<li><a href=\"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/CC82B2E79DC5CCAD57E0AC5DF0D43DEC\/S0956796820000064a.pdf\/div-class-title-heterogeneous-binary-random-access-lists-div.pdf\">Functional Pearls: Heterogeneous binary random-access lists<\/a>. ~ Wouter Swierstra. #Agda #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/czp3OUmcIYg\">On beyond Prolog<\/a>. ~ Anne Ogborn (@AnnieTheObscure). #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/blog.josephmorag.com\/posts\/zip-tree1\/\">Zipping trees<\/a>. Part 1. ~ Joseph Morag. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.josephmorag.com\/posts\/zip-tree2\/\">Zipping trees<\/a>. Part 2. ~ Joseph Morag. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Sliding_Window_Algorithm.html\">Formalization of an algorithm for greedily computing associative aggregations on sliding windows<\/a>. ~ Lukas Heimes, Dmitriy Traytel, Joshua Schneider. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/williamyaoh.com\/posts\/2020-04-12-software-engineer-hangups.html\">Things software engineers trip up on when learning Haskell<\/a>. ~ William Yao (@williamyaoh). #Haskell #FuncionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/POHVMMG7pqE\">10 minute Lean tutorial: proving logical propositions<\/a>. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Logic<\/li>\n<li><a href=\"https:\/\/www.ideallearning.fi\/index.php\/blogi\/95-chicken-jerky-flavoured-introduction-to-functional-programming-is-out-in-english\">Doglike programming book (Chicken jerky flavoured introduction to functional programming)<\/a>. ~ Juuso Vuorinen. #eBook #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2004.05631\">At the interface of algebra and statistics<\/a>. ~ Tai-Danae Bradley. #PhD_Thesis #Math<\/li>\n<li><a href=\"https:\/\/haskellfortypescriptdevs.fission.codes\/appendix\/haskell-wizards\">Haskell Wizards (Character illustrations of Haskell users)<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1904.13203\">Computable analysis and notions of continuity in Coq<\/a>. ~ Florian Steinberg, Laurent Thery, Holger Thies. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/blog.poisson.chat\/posts\/2020-04-13-safe-head-tail.html\">Programming totally with head and tail<\/a>. ~ Li-yao Xia (@lysxia). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2004.06997\">Prolog technology reinforcement learning prover<\/a>. ~ Zsolt Zombori, Josef Urban, Chad E. Brown. #ATP #MachineLearning #Prolog<\/li>\n<li><a href=\"https:\/\/leanpub.com\/progalgs\/read\">Programming algorithms<\/a>. ~ Vsevolod Domkin #eBook #CommonLisp #Programming #Algorithms<\/li>\n<li><a href=\"https:\/\/golem.ph.utexas.edu\/category\/2020\/04\/online_seminar_lists.html\">Online seminar lists<\/a>. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/blog.sumtypeofway.com\/posts\/fast-iteration-with-haskell.html\">Towards faster iteration in industrial Haskell<\/a>. ~ Patrick Thomson (@importantshock). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2004.07390\">Trakhtenbrot&#8217;s theorem in Coq, a constructive approach to finite model theory<\/a>. ~ Dominik Kirst, Dominique Larchey-Wendling. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2020-04-16-exceptions-in-haskell.html\">The three kinds of Haskell exceptions and how to use them<\/a>. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/thma\/WhyHaskellMatters\">Why Haskell matters<\/a>. ~ Thomas Mahler. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www21.in.tum.de\/~traytel\/papers\/incompleteness\/incompleteness.pdf\">Distilling the requirements of G\u00f6del\u2019s Incompleteness theorems with a proof assistant<\/a>. ~ Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/~gaeher\/files\/thesis-gaeher.pdf\">Towards a formal proof of the Cook-Levin theorem<\/a>. ~ Lennard G\u00e4her. #ITP #Coq #Logic #Math<\/li>\n<li><a href=\"http:\/\/group-mmm.org\/~ayamada\/TBDHJY20.pdf\">Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle\/HOL<\/a>. ~ Ren\u00e9 Thiemann et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/hackernoon.com\/what-is-haskell-who-uses-it-and-where-can-you-learn-to-code-it-7xme32d0\">What Is Haskell, who uses it, and where can you learn to code it<\/a>. ~ Alexander Sechin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/mb-qDG5-05Y\">The mechanization of Mathematics<\/a>. ~ Jeremy Avigad. #ITP #Math<\/li>\n<li><a href=\"https:\/\/www.andrew.cmu.edu\/user\/avigad\/Talks\/mechanization_talk.pdf\">The mechanization of Mathematics<\/a>. ~ Jeremy Avigad. #ITP #Math<\/li>\n<li><a href=\"https:\/\/typeclasses.com\/timeline\">Great moments in Haskell history<\/a>. ~ Chris Martin (@chris__martin), Julie Moronuki (@argumatronic). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/pauloedevilhena.com\/wp-content\/uploads\/2020\/03\/de-vilhena-paulson-algebraically-closed-fields-2020.pdf\">Algebraically closed fields in Isabelle\/HOL<\/a>. ~ Paulo Em\u0131\u0301lio de Vilhena, Lawrence C. Paulson. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/qwAmiJ5M_zM\">Introduction to relude an alternative Haskell prelude<\/a>. ~ Dmitrii Kovanikov (@ChShersh). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Lucas_Theorem.html\">Lucas&#8217;s theorem in Isabelle\/HOL<\/a>. ~ Chelsea Edmonds. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/www.haskellforall.com\/2020\/04\/blazing-fast-fibonacci-numbers-using.html\">Blazing fast Fibonacci numbers using Monoids<\/a>. ~ G. Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2004.07761\">Deep generation of Coq lemma names using elaborated terms<\/a>. ~ Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric. #ITP #Coq #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2004.10655\">Formal verification of flow equivalence in desynchronized designs<\/a>. ~ Jennifer Paykin, Brian Huffman, Daniel M. Zimmerman, Peter A. Beerel. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2004.10263\">The Imandra automated reasoning system (system description)<\/a>. ~ Grant Olneya Passmore et als. #ITP<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2020-04-23-deriving-isomorphically.html\">Deriving isomorphically<\/a>. ~ Hans Hoeglund. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/wwwf.imperial.ac.uk\/~buzzard\/xena\/computers.pdf\">When will computers prove theorems?<\/a> ~ Kevin Buzzard. #ITP #Math<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/recursive-functions\/\">Recursive functions<\/a>. ~ Walter Dean. #Logic #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/q5-pykbfViA\">Is HoTT the way to do mathematics?<\/a> ~ Kevin Buzzard. #Math #HoTT #ITP<\/li>\n<li><a href=\"https:\/\/www.abc.es\/ciencia\/abci-metodo-moore-o-como-aprender-matematicas-estilo-tejano-202004270153_noticia.html\">El m\u00e9todo Moore o c\u00f3mo aprender matem\u00e1ticas al estilo tejano<\/a>. ~ Pedro Alegr\u00eda. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/scholarworks.gvsu.edu\/books\/20\/\">Active Prelude to Calculus<\/a>. ~ Matthew Boelkins. #Math<\/li>\n<li><a href=\"https:\/\/scholarworks.gvsu.edu\/books\/18\/\">Active Calculus 2<\/a>.1. ~ Matthew Boelkins. #Math<\/li>\n<li><a href=\"https:\/\/scholarworks.gvsu.edu\/books\/19\/\">Active Calculus Multivariable: 2018 Edition<\/a>. ~ Steve Schlicker, David Austin, Matt Boelkins. #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2004.12330\">Detecting fake news for the new coronavirus by reasoning on the Covid-19 ontology<\/a>. ~ Adrian Groza. #ATP #Racer<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Attack_Trees.html\">Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems<\/a>. ~ Florian Kamm\u00fcller. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.mdpi.com\/1999-4893\/13\/5\/106\">Diagnosis in tennis serving technique<\/a>. ~ Eugenio Roanes-Lozano et als. #KBS #CAS #GroebnerBases #Logic #Math #CompSci<\/li>\n<li><a href=\"https:\/\/alvinalexander.com\/downloads\/scala-book\/ScalaBook.pdf\">Scala book (Learn Scala fastwith small, easy lessons)<\/a>. ~ Alvin Alexander, et al. #eBook #Scala #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/guilhermehas.github.io\/crypto-agda\/thesis.pdf\">A simplified version of Bitcoin, implemented in Agda<\/a>. ~ Guilherme Horta Alvares da Silva. #ITP #Agda #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/gilmi.me\/blog\/post\/2020\/04\/28\/consider-haskell\">Consider Haskell<\/a>. ~ Gil Mizrahi (@_gilmi). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Lambert_W.html\">The Lambert W function on the reals<\/a>. ~ Manuel Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/link.springer.com\/book\/10.1007\/978-3-319-58487-4\">Introduction to Artificial Intelligence<\/a>. ~ Wolfgang Ertel. #eBook #Logic #AI<\/li>\n<li><a href=\"https:\/\/open.umn.edu\/opentextbooks\">Open Textbook Library<\/a>: Open textbooks are textbooks that have been funded, published, and licensed to be freely used, adapted, and distributed. #eBooks<\/li>\n<li><a href=\"https:\/\/link.springer.com\/book\/10.1007\/978-3-319-97298-5\">Mathematical logic (On numbers, sets, structures, and symmetry)<\/a>. ~ Romana Kossak. #eBook #Logic #Math<\/li>\n<li><a href=\"https:\/\/link.springer.com\/book\/10.1007\/978-3-030-03255-5\">Philosophical and mathematical logic<\/a>. ~ Harrie de Swart. #eBook #Logic #Math<\/li>\n<li><a href=\"https:\/\/link.springer.com\/book\/10.1007\/978-3-319-70790-7\">Foundations of programming languages<\/a>. ~ Kent D. Lee. #eBook #Programming #CompSci<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2020\/04\/30\/the-invisible-map\/\">The invisible map<\/a>. ~ Kevin Buzzard (@XenaProject). #Logic #Math #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/link.springer.com\/book\/10.1007\/978-3-662-57265-8\">Proofs from THE BOOK<\/a>. ~ Martin Aigner, G\u00fcnter M. Ziegler #FreeEbook #Math<\/li>\n<\/ul>\n<\/div>\n<div id=\"postamble\" class=\"status\">\n<p class=\"date\">\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante abril de 2020, 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\/7207"}],"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=7207"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7207\/revisions"}],"predecessor-version":[{"id":7208,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7207\/revisions\/7208"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7207"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7207"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7207"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}