{"id":7591,"date":"2020-11-01T19:04:42","date_gmt":"2020-11-01T18:04:42","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7591"},"modified":"2021-08-30T19:05:57","modified_gmt":"2021-08-30T17:05:57","slug":"resumen-de-lecturas-compartidas-durante-octubre-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-octubre-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas durante octubre de 2020"},"content":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante octubre 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>.<br \/>\n<!--more--><\/p>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/herebeseaswines.net\/essays\/2020-10-23-wireworld%20\">Cellular automaton in Haskell (II)<\/a>. WireWorld. ~ Claes-Magnus Berg. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/jackkelly.name\/blog\/archives\/2020\/10\/16\/accidentally-quadratic_hashmaps\/index.html\">Accidentally-quadratic HashMaps<\/a>. ~ Jack Kelly. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/uncaught-exception-handling\">Handling of uncaught exceptions in Haskell<\/a>. ~ Ivan Gromakovsky. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.parsonsmatt.org\/2020\/10\/27\/plucking_in_plucking_out.html\">Plucking In, Plucking Out<\/a>. ~ Matt Parsons. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.ensiie.fr\/wp-content\/uploads\/2020\/10\/poster_dubois-1.pdf\">Formally verified constraints solvers (A guided tour)<\/a>. ~ Catherine Dubois. #ITP #Coq #CSP<\/li>\n<li><a href=\"https:\/\/books.google.es\/books?id=JA0FEAAAQBAJ&amp;lpg=PP1&amp;pg=PP\">Competitive programming in Python (128 algorithms to develop your coding skills)<\/a>. ~ Christoph D\u00fcrr, Jill-J\u00eann Vie.1#v=onepage&amp;q&amp;f=false #Programming #Python<\/li>\n<li><a href=\"https:\/\/youtu.be\/17gfCTnw6uE\">Efficient automatic differentiation made easy via category theory<\/a>. ~ Conal Elliott. #Haskell #CategoryTheory<\/li>\n<li><a href=\"https:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?thedu2020.1.pdf\">Teaching interactive proofs to mathematicians<\/a>. ~ M. Ayala-Rinc\u00f3n, T.A. de Lima. #ITP #PVS #Math<\/li>\n<li><a href=\"https:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?thedu2020.2.pdf\">Isabelle\/HOL as a meta-language for teaching logic<\/a>. ~ Asta Halkj\u00e6r From, J\u00f8rgen Villadsen, Patrick Blackburn. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?thedu2020.3.pdf\">Formalizing IMO problems and solutions in Isabelle\/HOL<\/a>. ~ Filip Mari\u0107, Sana Stojanovi\u0107-\u0110ur\u0111evi\u0107. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/github.com\/filipmaric\/IMO\">Formalization of IMO solutions in Isabelle\/HOL<\/a>. ~ Filip Mari\u0107. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/ihp.digitallyinduced.com\/ShowPost?postId=14ed1d41-5ea4-4608-9c96-465443cd6e55\">Haskell: The good parts<\/a>. ~ Marc Scholten. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/culturacientifica.com\/2020\/10\/21\/rompecabezas-matematicos-con-numeros\/\">Rompecabezas matem\u00e1ticos con n\u00fameros<\/a>. ~ Ra\u00fal Ib\u00e1\u00f1ez. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/qnikst.github.io\/posts\/2020-10-18-quicksort.html\">Quicksort in Haskell<\/a>. ~ Alexander Vershilov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/her.esy.fun\/posts\/0015-how-i-use-org-mode\/index.html\">How I use org-mode<\/a>. ~ Yann Esposito. #Emacs #OrgMode<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=240\">Tableros sem\u00e1nticos en l\u00f3gica de primer orden<\/a>. ~ Fernando Sancho. #L\u00f3gica<\/li>\n<li><a href=\"http:\/\/www.haskellforall.com\/2020\/10\/why-i-prefer-functional-programming.html\">Why I prefer functional programming<\/a>. ~ G. Gonzalez. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Physical_Quantities.html\">A sound type system for physical quantities, units, and measurements in Isabelle\/HOL<\/a>. ~ Simon Foster, Burkhart Wolff. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/ceur-ws.org\/Vol-2710\/paper21.pdf\">Tautology checkers in Isabelle and Haskell<\/a>. ~ J\u00f8rgen Villadsen. #ITP #IsabelleHOL #Haskell #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/dfa85b54bbba02433e0cb924547808ff5120f78c\/archive\/imo\/imo1981_q3.lean\">IMO 1981 Q3 in Lean<\/a>. ~ Kevin Lacker. #ITP #LeanProver #Math #IMO<\/li>\n<li><a href=\"https:\/\/www.snoyman.com\/blog\/2020\/10\/haskell-bad-parts-1\">Haskell: The bad parts, part 1<\/a>. ~ Michael Snoyman. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.site.uottawa.ca\/~afelty\/dist\/vecos20.pdf\">Formal verification of a certified policy language<\/a>. ~ Amir Eaman, Amy Felty. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/itu.dk\/people\/jkas\/papers\/actris2.pdf\">Actris 2<\/a>.0: Asynchronous session-type based reasoning in separation logic. ~ Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/qrs20.techconf.org\/QRS2020_FULL\/pdfs\/QRS2020-4LGdOos7NAbR8M2s6S6ezE\/891300a254\/891300a254.pdf\">Development method of three kinds of typical tree structure algorithms and Isabelle-based machine assisted verification<\/a>. ~ Changjing Wang et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/how-the-towering-p-adic-numbers-work-20201019\/\">An infinite universe of number systems<\/a>. ~ Kelsey Houston-Edwards. #Math<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=239\">Tableros sem\u00e1nticos en l\u00f3gica proposicional<\/a>. ~ Fernando Sancho. #L\u00f3gica #Matem\u00e1tica<\/li>\n<li><a href=\"https:\/\/easychair.org\/publications\/preprint_download\/T98x\">Automated theorem proving, fast and slow<\/a>. ~ Michael Rawson, Giles Reger. #ATP #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2010.10296\">SeLFiE: Modular semantic reasoning for induction in Isabelle\/HOL<\/a>. ~ Yutaka Nagashima. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/the-map-of-mathematics-20200213\/\">The Map of Mathematics<\/a>. #Math<\/li>\n<li><a href=\"https:\/\/github.com\/xiw\/arithcc\">A formalization of &#8220;Correctness of a compiler for arithmetic expressions&#8221; (McCarthy and Painter 1967) using the Lean theorem prover<\/a>. ~ Xi Wang. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/functional-programming-in-fintech\">Why fintech companies use Haskell<\/a>. ~ Roman Alterman. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/@aronwith1a\/the-coin-change-problem-in-haskell-bc1fa89cd09c\">The coin change problem in Haskell<\/a>. ~ Aron. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/0O_boW9YA7I\">The greatest mathematician that never lived<\/a>. ~ Pratik Aghor. #Math<\/li>\n<li><a href=\"https:\/\/emanuelpeg.blogspot.com\/2020\/10\/quien-utiliza-haskell.html?spref=tw\">Quien utiliza Haskell??<\/a> ~ Emanuel Goette. #Haskell #Programaci\u00f3nFuncional<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/a249c9a4ee252ad64171fa779883d48c3a0fe93a\/archive\/imo\/imo1998_q2.lean\">IMO 1998 Q2 in Lean<\/a>. ~ Oliver Nash. #ITP #LeanProver #Math #IMO<\/li>\n<li><a href=\"https:\/\/www.microsiervos.com\/archivo\/mundoreal\/coleccion-falacias-logicas-ilustradas-ejemplos.html\">Una colecci\u00f3n de falacias l\u00f3gicas ilustradas con ejemplos<\/a>. ~ @Alvy. #L\u00f3gica<\/li>\n<li><a href=\"https:\/\/www.cardsoflogic.com\/\">Common logical fallacies (A handy collection of the most common logical fallacies for you to bookmark)<\/a>. #Logic<\/li>\n<li><a href=\"https:\/\/sol.sbc.org.br\/index.php\/semish\/article\/view\/11331\/11194\">EvoLogic: Sistema tutor inteligente para ensino de L\u00f3gica<\/a>. ~ Cristiano Galafassi, Fabiane F.P. Galafassi, Eliseo B. Reategui, Rosa M. Vicari. #Logic #AI<\/li>\n<li><a href=\"https:\/\/emacssurvey.org\/\">Emacs user survey<\/a>. #Emacs<\/li>\n<li><a href=\"https:\/\/code.librehq.com\/qhong\/crdt.el\/\">crdt<\/a>.el: a real-time collaborative editing environment for Emacs using Conflict-free Replicated Data Types. #Emacs<\/li>\n<li><a href=\"https:\/\/github.com\/dickmao\/nntwitter\">nntwitter: A Gnus backend for Twitter<\/a>. #Emacs #Twitter<\/li>\n<li><a href=\"https:\/\/github.com\/p3r7\/awesome-elisp\">Awesome Elisp: a list of resources linked to Emacs LISP (Elisp) development<\/a>. #Emacs #Elisp<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-59152-6_2\">Verified textbook algorithms (A biased survey)<\/a>. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.philipzucker.com\/theorem-proving-for-catlab-2-lets-try-z3-this-time-nope\/\">Theorem proving for Catlab 2: Let&#8217;s try Z3 this time<\/a>. Nope. ~ Philip Zucker #CategoryTheory #JuliaLang<\/li>\n<li><a href=\"https:\/\/blog.cofree.coffee\/2020-10-17-bounded-space-automata\/\">Implementing cellular automata with comonads and dependent types<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/stopa.io\/post\/263\">Fun with Lambda Calculus<\/a>. ~ Stepan Parunashvili. #Clojure #FunctionalProgramming #LambdaCalculus<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/c83c28a1ef16790f62c893379b75f77d30ab068e\/archive\/imo\/imo2019_q4.lean\">IMO 2019 problem 4 in Lean<\/a>. ~ Floris van Doorn. #ITP #LeanProver #Math #IMO<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2020-10-17-ski.html\">Fun with combinators<\/a>. ~ Donnacha Ois\u00edn Kidney. #Logic #CompSci #Combinators<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=238\">Sintaxis y sem\u00e1ntica de la l\u00f3gica de primer orden<\/a>. ~ Fernando Sancho. #L\u00f3gica #Matem\u00e1tica<\/li>\n<li><a href=\"https:\/\/ir.canterbury.ac.nz\/bitstream\/handle\/10092\/101132\/Robinson-O%27Brien%2c%20Nicolas_Master%27s%20Thesis.pdf?sequence=1&amp;isAllowed=y\">A formal correctness proof of Boruvka&#8217;s minimum spanning tree algorithm<\/a>. ~ Nicolas Robinson-O&#8217;Brien. #MSc_Thesis #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/repositum.tuwien.at\/bitstream\/20.500.12708\/1084\/2\/Formalizing%20Graph%20Trail%20Properties.pdf\">Formalizing graph trail properties<\/a>. ~ Hanna Elif Lachnitt. #Thesis #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/BB3F7C0A0DACE740AE110D43414E0DEC\/S0960129520000213a.pdf\/model_structure_on_the_universe_of_all_types_in_interval_type_theory.pdf\">Model structure on the universe of all types in interval type theory<\/a>. ~ Simon Boulier, Nicolas Tabareau. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/perso.telecom-paristech.fr\/bloch\/OptionIA\/IA301-Lecture1-IntroDL-OWL.pdf\">Symbolic Artificial Intelligence (Lecture 1: Introduction to description logics and ontologies)<\/a>. ~ Natalia D\u00edaz Rodr\u00edguez. #AI #Logic<\/li>\n<li><a href=\"https:\/\/perso.telecom-paristech.fr\/bloch\/OptionIA\/IntroSymbAI.pdf\">Logics and symbolic AI: Knowledge representation and reasoning<\/a>. ~ Isabelle Bloch, Natalia D\u0131\u0301az Rodr\u0131\u0301guez. #AI #Logic<\/li>\n<li><a href=\"https:\/\/perso.telecom-paristech.fr\/bloch\/OptionIA\/Logics-SymbolicAI.html\">Course: Logics and symbolic AI<\/a>. ~ Isabelle Bloch, Natalia D\u0131\u0301az Rodr\u0131\u0301guez. #AI #Logic<\/li>\n<li><a href=\"https:\/\/theconversation.com\/what-is-an-algorithm-how-computers-know-what-to-do-with-data-146665\">What is an algorithm? How computers know what to do with data<\/a>. ~ Jory Denny. #Algorithms<\/li>\n<li><a href=\"https:\/\/correl.phoenixinquis.net\/2015\/07\/12\/git-graphs.html\">Drawing Git Graphs with Graphviz and Org-Mode<\/a>. ~ Correl Roush. #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/blogs\/blog-cacm\/247225-things-to-do-to-an-algorithm\/fulltext\">Things to do to an algorithm<\/a>. ~ Bertrand Meyer. #Algorithms<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/blogs\/blog-cacm\/248046-the-pros-and-cons-of-online-lab-classes-for-computer-science-2020-pandemic-edition\/fulltext\">The pros and cons of online lab classes for Computer Science &#8211; 2020 pandemic edition<\/a>. ~ Philip Guo. #CompSci<\/li>\n<li><a href=\"https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1571066120300463\">Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda<\/a>. ~ Sebasti\u00e1n Urciuoli, \u00c1lvaro Tasistro Nora Szasz. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/youtu.be\/Mq9sHgXjsG4\">Resoluci\u00f3n de los 99 ejercicios de Prolog<\/a>. #Prolog #Programaci\u00f3nL\u00f3gica<\/li>\n<li><a href=\"https:\/\/github.com\/TheoWinterhalter\/phd-thesis\/releases\/download\/v1.2.1\/TheoWinterhalter-PhD-v1.2.1.pdf\">Formalisation and meta-theory of type theory<\/a>. ~ Th\u00e9o Winterhalter. #ITP #Coq #TypeTheory<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2010.07763v1\">Refinement types: A tutorial<\/a>. ~ Ranjit Jhala, Niki Vazou. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/leanpub.com\/production-haskell\">Production Haskell (Succeeding in industry with Haskell)<\/a>. ~ Matt Parsons. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/tech.channable.com\/posts\/2020-10-15-bottlenecked-on-haskells-text.html\">Bottlenecked on Haskell&#8217;s text library<\/a>. ~ Falco Peijnenburg. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=237\">Sintaxis y sem\u00e1ntica de la l\u00f3gica proposicional<\/a>. ~ Fernando Sancho. #L\u00f3gica #Matem\u00e1tica<\/li>\n<li><a href=\"https:\/\/raw.githubusercontent.com\/barry-jay-personal\/tree-calculus\/master\/tree_book.pdf\">Reflective programs in tree calculus<\/a>. ~ Barry Jay. #ITP #Coq #Logic<\/li>\n<li><a href=\"https:\/\/chrispenner.ca\/posts\/interview\">Silly job interview questions in Haskell<\/a>. ~ Chris Penner. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/raw.githubusercontent.com\/blanchette\/logical_verification_2020\/master\/hitchhikers_guide.pdf\">The Hitchhiker\u2019s Guide to Logical Verification (2020 Standard Edition (October 12, 2020))<\/a>. ~ Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes H\u00f6lzl. #eBook #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/arstechnica.com\/science\/2020\/10\/the-unreasonable-effectiveness-of-the-julia-programming-language\/\">The unreasonable effectiveness of the Julia programming language<\/a>. ~ Lee Phillips. #JuliaLang #Programming<\/li>\n<li><a href=\"https:\/\/reasonablypolymorphic.com\/blog\/towards-tactics\/\">Towards tactic metaprogramming in Haskell<\/a>. ~ Sandy Maguire. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/programmable.computer\/posts\/normal-forms.html\">Normal forms<\/a>. ~ Travis Whitaker. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dcabrejas.github.io\/software-development\/haskell\/2020\/10\/11\/haskell-adts.html\">What are algebraic data types? ~ @dicabrejas<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/liberationtech.net\/emacs-might-not-be-doomed-after-all\/\">Emacs might not be doomed after all<\/a>. ~ Oivvio Polite. #Emacs<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2008.07912\">Inductive logic programming at 30: a new introduction<\/a>. ~ Andrew Cropper, Sebastijan Duman\u010di\u0107. #ILP #MachineLearning #LogicProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/@fommil\/delivering-with-haskell-a347d8359597\">Delivering with Haskell<\/a>. ~ Sam Halliday. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/Christoph_Benzmueller\/publication\/344452246_Dyadic_Deontic_Logic_in_HOL_Faithful_Embedding_and_Meta-Theoretical_Experiments\/links\/5f7719a1a6fdcc0086506d5d\/Dyadic-Deontic-Logic-in-HOL-Faithful-Embedding-and-Meta-Theoretical-Experiments.pdf\">Dyadic deontic logic in HOL: Faithful embedding and meta-theoretical experiments<\/a>. ~ Christoph Benzm\u00fcller, Ali Farjami, Xavier Parent. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2010.00810v1\">Public announcement logic in HOL<\/a>. ~ Sebastian Reiche, Christoph Benzm\u00fcller. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/isabelle.in.tum.de\/~ballarin\/publications\/isabelle2020.pdf\">An antiquotation for locale graphs<\/a>. ~ Clemens Ballarin. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.cis.upenn.edu\/~plclub\/blog\/2020-10-09-hs-to-coq\/\">Tutorial: Verify Haskell programs with hs-to-coq<\/a>. ~ Li-yao Xia. #ITP #Coq #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/1NA6yV3cxNY\">Embracing a mechanized formalization<\/a>. ~ Li-yao Xia. #ITP #Coq #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02956858\/document\">Separation logic-based verification atop a binary-compatible filesystem model<\/a>. ~ Mihir Mehta, William Cook. #ITP #ACL2<\/li>\n<li><a href=\"https:\/\/medium.com\/cantors-paradise\/the-anarchist-abstractionist-who-was-alexander-grothendieck-cc396083d94e%20\">The anarchist abstractionist: Who was Alexander Grothendieck?<\/a> ~ J\u00f8rgen Veisdal. #Math<\/li>\n<li><a href=\"https:\/\/limperg.de\/paper\/cpp2021-induction\/draft.pdf\">A novice-friendly induction tactic for Lean (Draft)<\/a>. ~ Jannis Limperg. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2010.01240\">Proving quantum programs correct<\/a>. ~ Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, Michael Hicks. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1906.03930\">Formalization of the axiom of choice and its equivalent theorems<\/a>. ~ Tianyu Sun, Wensheng Yu. #ITP #Coq #Logic #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2010.01187v1\">On the Nielsen-Schreier theorem in homotopy type theory<\/a>. ~ Andrew W Swan. #ITP #Agda #Math #HoTT<\/li>\n<li><a href=\"http:\/\/cseweb.ucsd.edu\/~hpeleg\/hplus-oopsla20.pdf\">Digging for fold: Synthesis-aided API discovery for Haskell<\/a>. ~ Michael B. James et als. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dspace.mit.edu\/bitstream\/handle\/1721.1\/100853\/18-304-spring-2006\/contents\/projects\/fallacy_yuan.pdf\">Mathematical fallacy proofs<\/a>. ~ Xing Yuan. #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.qrg.northwestern.edu\/BPS\/readme.html\">Building problem solvers<\/a>. ~ Kenneth D. Forbus, Johan de Kleer. #eBook #AI #CommonLisp<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/computer-scientists-break-traveling-salesperson-record-20201008\/\">Computer scientists break traveling salesperson record<\/a>. ~ Erica Klarreich. #Algorithms #CompSci<\/li>\n<li><a href=\"https:\/\/users-cs.au.dk\/birke\/papers\/2021-monotone.pdf\">Reasoning about monotonicity in separation logic<\/a>. ~ Amin Timany, Lars Birkedal. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.algorithm-archive.org\/\">The Arcane Algorithm Archive (a collaborative effort to create a guide for all important algorithms in all languages)<\/a>. #Algorithms #Programming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2010.02595\">Formalizing the ring of Witt vectors<\/a>. ~ Johan Commelin, Robert Y. Lewis. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/boarders.github.io\/posts\/peano.html\">On characterizing Nat in Agda<\/a>. ~ Callan McGill. #ITP #Agda #Logic #Math<\/li>\n<li><a href=\"https:\/\/favonia.org\/courses\/hdtt2020\/\">Course: Higher-Dimensional Type Theory<\/a>. ~ Favonia. #TypeTheory #ITP #Agda<\/li>\n<li><a href=\"https:\/\/www.youtube.com\/playlist?list=PL0OBHndHAAZrGQEkOZGyJu7S7KudAJ8M9\">Higher-dimensional type theory (Lecture recordings)<\/a>. ~ Favonia. #TypeTheory<\/li>\n<li><a href=\"https:\/\/phys.org\/news\/2020-10-scientists-year-old-geometry-problem.amp\">Scientists solve 90-year-old geometry problem<\/a>. ~ Byron Spice. #Math #ATP #SAT_solver<\/li>\n<li><a href=\"https:\/\/github.com\/bobatkey\/CS316-2020\">Course &#8220;Functional Programming&#8221;<\/a>. ~ Bob Atkey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.fpcomplete.com\/blog\/collect-rust-traverse-haskell-scala\/\">Collect in Rust, traverse in Haskell and Scala<\/a>. Michael Snoyman. #Haskell #Rust #Scala #FunctionalProgramming via @FPComplete<\/li>\n<li><a href=\"https:\/\/rjlipton.wordpress.com\/2020\/10\/06\/knowledge-is-good\/\">Knowledge is good<\/a>. ~ R.J. Lipton. #Logic #Math<\/li>\n<li><a href=\"https:\/\/repositum.tuwien.at\/bitstream\/20.500.12708\/15528\/1\/32_Smart%20Induction%20for%20Isabelle_HOL%20%28Tool%20Paper%29.pdf\">Smart induction for Isabelle\/HOL (Tool paper)<\/a>. ~ Yutaka Nagashima. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/lopezacosta.net\/assets\/pdf\/iFM20.pdf\">Chain of events: Modular process models for the law<\/a>. ~ S\u00f8ren Debois et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.itu.dk\/people\/debois\/thys\/ifm20\/document.pdf\">Formalisation: Chain of events: Modular process models for the law<\/a>. ~ S\u00f8ren Debois #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/github.com\/adamtopaz\/comb_geom\">Combinatorial geometries in Lean<\/a>. ~ Adam Topaz. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2010.00774\">Proof repair across type equivalences<\/a>. ~ Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, Dan Grossman. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.fpcomplete.com\/blog\/2017\/09\/all-about-strictness\/\">All about strictness<\/a>. ~ Michael Snoyman. #Haskell #FunctionalProgramming via @FPComplete<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2020\/10\/5\/starting-haskellings\">Starting Haskellings!<\/a> ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/alhassy.github.io\/AlBasmala\">Blogging with Emacs &amp; Org-mode<\/a>. ~ Musa Al-hassy. #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/alhassy.github.io\/CalcCheck\/\">Calculational Mathematics and CalcCheck<\/a>. ~ Musa Al-hassy. #Math #CalcCheck<\/li>\n<li><a href=\"https:\/\/cs.au.dk\/~gregersen\/papers\/2021-tiniris.pdf\">Mechanized logical relations for termination-insensitive noninterference<\/a>. ~ S.O. Gregersen, J. Bay, A. Timany, L. Birkedal. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/b-mehta\/combinatorics\">Combinatorics in Lean<\/a>. ~ Bhavik Mehta. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/gist.github.com\/serras\/5152ec18ec5223b676cc67cac0e99b70\">Optics and Kleisli arrows<\/a>. ~ Alejandro Serrano. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/softech.cs.uni-kl.de\/homepage\/staff\/PeterZeller\/PeterZellerDissertation_preprint.pdf\">Tool supported specification and verification of highly available applications<\/a>. ~ Peter Zeller. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.13767v1\">Generating mutually inductive theorems from concise descriptions<\/a>. ~ Sol Swords. #ITP #ACL2<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.13769v1\">Ethereum&#8217;s recursive length prefix in ACL2<\/a>. ~ Alessandro Coglio. #ITP #ACL2 #Ethereum<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.13771v1\">Isomorphic data type transformations<\/a>. ~ Alessandro Coglio, Stephen Westfold. #ITP #ACL2<\/li>\n<li><a href=\"http:\/\/math.bu.edu\/people\/aki\/16.pdf\">Set theory from Cantor to Cohen<\/a>. ~ Akihiro Kanamori. #Logic #Math v\u00eda @logicians<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.13065v1\">Fixed points theorems for non-transitive relations<\/a>. ~ J\u00e9r\u00e9my Dubut, Akihisa Yamada. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.13764v1\">Computing and proving well-founded orderings through finite abstractions<\/a>. ~ Rob Sumners. #ITP #ACL2<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.13766v1\">Quadratic extensions in ACL2<\/a>. ~ Ruben Gamboa, John Cowles, Woodrow Gamboa. #ITP #ACL2 #Math<\/li>\n<li><a href=\"https:\/\/books.google.es\/books?id=0oCADwAAQBAJ&amp;lpg=PP1&amp;pg=PP\">Essential logic for computer science<\/a>. ~ Rex Page, Ruben Gamboa.1#v=onepage&amp;q&amp;f=true #eBook #Logic #ITP #ACL2<\/li>\n<li><a href=\"https:\/\/en.wikipedia.org\/wiki\/Grzegorczyk_hierarchy\">Grzegorczyk hierarchy<\/a>. #Logic #Math #CompSci<\/li>\n<li><a href=\"https:\/\/matematicascontraelcoronavirus.wordpress.com\/\">Matem\u00e1ticas vs Coronavirus: recursos matem\u00e1ticos para la docencia online<\/a>. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/notxor.nueva-actitud.org\/2020\/10\/02\/cambiando-el-blog-a-org-static-blog.html\">Cambiando el blog a org-static-blog<\/a>. #Emacs<\/li>\n<li><a href=\"https:\/\/doi.org\/10.1016\/j.jsc.2014.09.032\">Learning-assisted theorem proving with millions of lemmas<\/a>. ~ Cezary Kaliszyk, Josef Urban. #ITP #ATP #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2007.12737\">Build scripts with perfect dependencies<\/a>. ~ Sarah Spall, Neil Mitchell, Sam Tobin-Hochstadt. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/building-the-mathematical-library-of-the-future-20201001\/\">Building the mathematical library of the future<\/a>. ~ Kevin Hartnett. #ITP #LeanProver #Math<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante octubre 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\/7591"}],"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=7591"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7591\/revisions"}],"predecessor-version":[{"id":7592,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7591\/revisions\/7592"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7591"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7591"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7591"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}