{"id":7593,"date":"2020-12-01T19:08:04","date_gmt":"2020-12-01T18:08:04","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7593"},"modified":"2021-08-30T19:09:44","modified_gmt":"2021-08-30T17:09:44","slug":"resumen-de-lecturas-compartidas-durante-noviembre-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-noviembre-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas durante noviembre de 2020"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante noviembre 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:\/\/raw.githubusercontent.com\/jaalonso\/Logica_con_Lean\/master\/Ejercicios_de_logica_proposicional_con_Lean.pdf\">#ForMatUS: Libro &#8220;Ejercicios de l\u00f3gica proposicional con Lean&#8221;<\/a>. #DAO #LeanProver #L\u00f3gica #Matem\u00e1tica #Programaci\u00f3nFuncional<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/browser_info\/current\/AFP\/Isabelle_Marries_Dirac\/document.pdf\">Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information<\/a>. ~ Anthony Bordg, Hanna Lachnitt, Yijun He. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2011.13218\">Formalising ordinal partition relations using Isabelle\/HOL<\/a>. ~ Mirna D\u017eamonja, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/bindthegap.news\/issues\/BindTheGap-01Nov2020.pdf\">Bind the gap (Pilot issue, November 2020)<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.ams.org\/journals\/notices\/202011\/rnoti-p1791.pdf\">Proving theorems with computers<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/github.com\/jdan\/compiler.lean\">A formally verified compiler for a simple language with numbers and sums<\/a>. ~ Jordan Scales. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/hackage.haskell.org\/package\/nuha-0.3.0.0\">nuha: Multidimensional arrays, linear algebra, numerical analysis<\/a>. ~ Johannes Kropp. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/raw.githubusercontent.com\/dcernst\/IBL-IntroToProof\/master\/Spring2020\/IntroToProof.pdf\">An introduction to proof via inquiry-based learning<\/a>. ~ Dana C. Ernst. #eBook #Logic #Math<\/li>\n<li><a href=\"https:\/\/dzackgarza.com\/introduction-to-infinity-categories\/\">Introduction to infinity categories<\/a>. (Some notes on a short introductory video on some foundational aspects of infinity categories). ~ Zack Garza. #CategoryTheory<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2011.10618\">Gradualizing the Calculus of Inductive Constructions<\/a>. ~ Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, \u00c9ric Tanter. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/seminar\/2020.11.09-kwan.pdf\">A brief introduction to Smtlink<\/a>. ~ Carl Kwan. #ITP #ACL2 #SMT #Z3<\/li>\n<li><a href=\"https:\/\/hazel.org\/hazeltutor-hatra2020.pdf\">Hazel tutor: Guiding novices through type-driven development strategies<\/a>. ~ Hannah Potter, Cyrus Omar. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/hazel.org\/\">Hazel: a live functional programming environment featuring typed holes<\/a>. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/346399483_Formalising_Ordinal_Partition_Relations_Using_IsabelleHOL\">Formalising ordinal partition relations using Isabelle\/HOL<\/a>. ~ Mirna Dzamonja, Angeliki Koutsoukou-Argyraki, Lawrence Paulson. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/T_IINWzQhow\">Program correctness<\/a>. ~ Graham Hutton. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.logicmatters.net\/2020\/11\/27\/logic-a-study-guide-first-order-logic\/\">Logic: A study guide \u2014 First order logic<\/a>. ~ Peter Smith. #Logic<\/li>\n<li><a href=\"https:\/\/books.google.es\/books?id=xq7DDwAAQBAJ&amp;lpg=PP1&amp;dq=Mathematics%20for%20Human%20Flourishing&amp;pg=PR1#v=onepage&amp;q&amp;f=false\">Mathematics for human flourishing<\/a>. ~ Francis Su. #Book #Math<\/li>\n<li><a href=\"https:\/\/matryoshka-project.github.io\/pubs\/satur_isa_paper.pdf\">A modular Isabelle framework for verifying saturation provers<\/a>. ~ Sophie Tourret, Jasmin Blanchette. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/chrispenner.ca\/posts\/virtual-fields\">Virtual record fields using lenses<\/a>. ~ Chris Penner. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.sumtypeofway.com\/posts\/existential-haskell.html\">Existential Haskell<\/a>. ~ Patrick Thomson. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/reasonablypolymorphic.com\/blog\/3d-printing\/index.html\">Haskell in the Real World<\/a>. ~ Sandy Maguire. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/smlfamily.github.io\/history\/SML-history.pdf\">The history of Standard ML<\/a>. ~ David Macqueen, Robert Harper, John Reppy. #SML #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/kqueue.org\/blog\/2020\/10\/15\/arithcc\/\">Correctness of a compiler for arithmetic expressions in Lean<\/a>. ~ Xi Wang. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2020-11-23-applicative-queue.html\">A queue for effectful breadth-first traversals (Part 10 of a 10-part series on breadth-first traversals)<\/a>. ~ Donnacha Ois\u00edn Kidney. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.poisson.chat\/posts\/2020-11-23-hs-to-coq-containers-sequence.html\">hs-to-coq and Data<\/a>.Sequence. ~ Li-yao Xia. #Haskell #Coq #FunctionalProgramming #ITP<\/li>\n<li><a href=\"https:\/\/ivanbakel.github.io\/posts\/intuitionistic-logic-in-haskell\/\">Intuitionistic logic in Haskell<\/a>. ~ Isaac van Bakel. #Logic #Haskell<\/li>\n<li><a href=\"https:\/\/ivanbakel.github.io\/posts\/theorem-proving-in-haskell\/\">Theorem proving in Haskell<\/a>. ~ Isaac van Bakel. #Logic #Haskell #ITP<\/li>\n<li><a href=\"http:\/\/www.ben-sherman.net\/aux\/curry-howard.pdf\">Haskell and the Curry-Howard isomorphism (Part 1)<\/a>. ~ Ben Sherman. #Haskell #Logic<\/li>\n<li><a href=\"https:\/\/web.archive.org\/web\/20080819185521\/http:\/\/www.thenewsh.com\/~newsham\/formal\/curryhoward\/\">The Curry-Howard correspondence in Haskell<\/a>. ~ Tim Newsham. #Logic #Haskell<\/li>\n<li><a href=\"https:\/\/wiki.haskell.org\/wikiupload\/1\/14\/TMR-Issue6.pd\">Adventures in Classical-Land<\/a>. ~ Dan Piponi.f#page=17 #Logic #Haskell<\/li>\n<li><a href=\"https:\/\/wiki.ifs.hsr.ch\/SemProgAnTr\/files\/Curry-Howard_Isomorphism_Down-to-Earth.pdf\">Curry-Howard isomorphism down-to-earth<\/a>. ~ Jannis Grimm. #Logic #Haskell<\/li>\n<li><a href=\"https:\/\/www.ccs.neu.edu\/home\/mates\/pubs\/mates_ugrad_thesis.pdf\">A survey into the Curry-Howard isomorphism &amp; type systems<\/a>. ~ Phillip Mates. #Logic #Haskell<\/li>\n<li><a href=\"https:\/\/www.pinterest.es\/vseloved\/lisp-books\/\">Lisp books (Most of Lisp books in one place)<\/a>. ~ Vsevolod Dyomkin. #Lisp #Programming<\/li>\n<li><a href=\"http:\/\/www.lix.polytechnique.fr\/Labo\/Dale.Miller\/papers\/lp-coq.pdf\">Two applications of logic programming to Coq<\/a>. ~ M. Manighetti, D. Miller, A. Momigliano. #ITP #Coq #LogicProgramming<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3426425.3426940\">Untangling mechanized proofs<\/a>. ~ Cl\u00e9ment Pit-Claude. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2011.07653\">Coming to terms with your choices: An existential take on dependent types<\/a>. ~ Georg Stefan Schmid, Olivier Blanvillain, Jad Hamza, Viktor Kun\u010dak. #ITP #Coq #Scala<\/li>\n<li><a href=\"http:\/\/tydeworkshop.org\/2020-abstracts\/paper11.pdf\">Shallowly embedding type theories as presheaf models in Agda<\/a>. ~ J. Ceulemans, D. Devriese. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/en.wikipedia.org\/wiki\/List_of_important_publications_in_mathematics\">List of important publications in mathematics<\/a>. #Books #Math<\/li>\n<li><a href=\"http:\/\/www.stumblingrobot.com\/best-math-books\/\">Best math books (A comprehensive reading list)<\/a>. #Book #Math<\/li>\n<li><a href=\"https:\/\/github.com\/nasa\/pvslib\">Release of the NASA PVS Library (NASALib) v7<\/a>.1. #ITP #PVS<\/li>\n<li><a href=\"https:\/\/openreview.net\/pdf?id=yDOqCwuvUb2\">BioShake: a Haskell EDSL forbioinformatics workflows<\/a>. ~ Justin Bedo. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/raw.githubusercontent.com\/ashok-khanna\/common-lisp-by-example\/main\/Common%20Lisp%20by%20Example.pdf\">Common Lisp by Example (A compilation of notes from various sources)<\/a>. ~ Ashok Khanna. #CommonLisp<\/li>\n<li><a href=\"https:\/\/interstices.info\/le-probleme-des-8-reines\/\">Le probl\u00e8me des 8 reines<\/a>. ~ Maxime Amblard. #Algorithms via @interstices_eu<\/li>\n<li><a href=\"https:\/\/www.cl.cam.ac.uk\/~jdy22\/papers\/certified-optimisation-of-stream-operations-using-heterogeneous-staging.pdf\">Certified optimisation of stream operations using heterogeneous staging<\/a>. ~ J. Lowenthal, J. Yallop. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428284\">Verifying replicated data types with typeclass refinements in Liquid Haskell<\/a>. ~ Yiyun Liu et als. #Haskell #FuncBl%C3%B6ndal.pdf #MSc_Thesis #Haskell #FunctionalProgramming #LiquidHaskelltionalProgramming #LiquidHaskell<\/li>\n<li><a href=\"https:\/\/odr.chalmers.se\/bitstream\/20.500.12380\/302035\/1\/CSE%2020-86%20Bl%C3%B6ndal.pdf\">Deriving Via (Type-directed instances)<\/a>. ~ Baldur Bl\u00f6ndal. #MSc_Thesis #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.kovach.me\/Superpowered_keyword_args_in_Haskell.html\">Superpowered keyword args in Haskell<\/a>. ~ Ben Kovach. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.doc.ic.ac.uk\/~rak\/papers\/LPOP.pdf\">Logical English<\/a>. ~ Robert Kowalski. #LogicProgramming #Prolog<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/shuffling-things-up.htm\">Shuffling things up: Applying Group Theory in Advent of Code<\/a>. ~ Justin Le.l#.X7Vk_XYPDuk.twitter #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/github.com\/digama0\/lean-type-theory\/releases\/download\/v1.0\/main.pdf\">The type theory of Lean<\/a>. ~ Mario Carneiro. #ITP #LeanProver #Logic #Math #TypeTheory<\/li>\n<li><a href=\"https:\/\/lean-forward.github.io\/internships\/arithmetic_and_casting_in_lean.pdf\">Arithmetic and casting in Lean<\/a>. ~ Paul-Nicolas Madelaine. #MSc_Thesis #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/matryoshka-project.github.io\/pubs\/lehenaff_report.pdf\">Meta-programming with the Lean proof assistant<\/a>. ~ Pablo Le H\u00e9naff. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/raw.githubusercontent.com\/filipmaric\/IMO\/master\/IMO_files\/output\/document.pdf\">Formulations and solutions of IMO problemsin Isabelle\/HOL<\/a>. Filip Mari\u0107, Sana Stojanovi\u0107-\u00d0ur\u0111evi\u0107. #ITP #IsabelleHOL #Math #IMO<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/browser_info\/current\/AFP\/IMO2019\/document.pdf%20\">Selected problems from the International Mathematical Olympiad 2019<\/a>. ~ Manuel Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Bibliografia_de_Lean\">Bibliograf\u00eda sobre Lean<\/a>. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/richardzach.org\/2019\/11\/01\/the-significance-of-the-curry-howard-isomorphism\/\">The significance of the Curry-Howard isomorphism<\/a>. ~ Richard Zach. #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/github.com\/azzamsa\/awesome-lisp-companies\">Awesome-Lisp-companies: A list of companies using Lisp in production<\/a>. #CommonLisp<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/logic-combinatory\/\">#SEP: Combinatory logic<\/a>. ~ Katalin Bimb\u00f3. #Logic<\/li>\n<li><a href=\"http:\/\/wld.cipsh.international\/wld.html\">List of events for World Logic Day 2021<\/a>. #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1912.02250\">A verified optimizer for quantum circuits<\/a>. ~ Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=243\">Formas prenex, de Skolem y teorema de Herbrand<\/a>. ~ Fernando Sancho. #L\u00f3gica<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/logic-ai\/\">Logic and Artificial Intelligence<\/a>. ~ Richmond Thomason. #Logic #AI<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2010.14648\">Formally verified SAT-based AI planning<\/a>. ~ Mohammad Abdulaziz, Friedrich Kurz. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.logicmatters.net\/2020\/11\/16\/philosophy-of-mathematics-a-reading-list\/\">Philosophy of mathematics \u2014 a reading list<\/a>. ~ Peter Smith. #Math<\/li>\n<li><a href=\"https:\/\/pit-claudel.fr\/clement\/papers\/alectryon-SLE20.pdf\">Untangling mechanized proofs<\/a>. ~ Cl\u00e9ment Pit-Claudel. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/youtu.be\/f8CKGoP3_us\">Video: Untangling mechanized proofs<\/a>. ~ Cl\u00e9ment Pit-Claudel. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/devanla.com\/posts\/de-mystifying-emacs-haskell-language-server-setup.html\">De-mystifying Emacs, lsp-haskell and haskell-language-server Setup<\/a>. ~ Guru Devanla. #Haskell #Emacs<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/browser_info\/current\/AFP\/AI_Planning_Languages_Semantics\/document.pdf\">AI planning languages semantics (in Isabelle\/HOL)<\/a>. ~ Mohammad Abdulaziz, Peter Lammich. #ITP #IsabelleHOL #AI<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/browser_info\/current\/AFP\/Verified_SAT_Based_AI_Planning\/document.pdf\">Verified SAT-based AI planning<\/a>. ~ Mohammad Abdulaziz, Friedrich Kurz. #ITP #IsabelleHOL #AI<\/li>\n<li><a href=\"https:\/\/project-archive.inf.ed.ac.uk\/ug4\/20201778\/ug4_proj.pdf\">A formalisation of biochemical process languages in Lean<\/a>. ~ Jonathan Coates. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/project-archive.inf.ed.ac.uk\/ug4\/20201833\/ug4_proj.pdf\">Mechanizing hyperdual numbers in Isabelle\/HOL<\/a>. ~ Filip Smola. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2011.03463\">Extending equational monadic reasoning with monad transformers<\/a>. ~ Reynald Affeldt, David Nowak. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/contribute\/naming.html\">Mathlib naming conventions<\/a>. ~ Jeremy Avigad. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/6b3a2d1d07abe083e281b3617f376cabc6043e66\/archive\/imo\/imo1964_q1.lean\">IMO 1964 Q1 in Lean<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/bit.ly\/3nm70qc\">Ranas, p\u00e1jaros \u2026 y la hip\u00f3tesis de Riemann<\/a>. ~ Juan Arias de Reyna. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/www.stephendiehl.com\/posts\/exotic01.html\">Exotic programming ideas: Part 1 (Module systems)<\/a>. ~ Stephen Diehl. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/blog\/2020-11-11-linear-dps\/\">Pure destination-passing style in Linear Haskell<\/a>. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/raw.githubusercontent.com\/oscarsanchezromero\/Calculo-Cientifico-Octave\/master\/MNOctave2018.pdf\">M\u00e9todos num\u00e9ricos b\u00e1sicos con Octave<\/a>. ~ Antonia M. Delgado, Juanjo Nieto, Aureliano M. Robles, \u00d3scar S\u00e1nchez. #Octave #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/github.com\/oscarsanchezromero\/Calculo-Cientifico-Octave\">Algoritmos b\u00e1sicos de C\u00e1lculo Cient\u00edfico programados con Octave<\/a>. ~ \u00d3scar S\u00e1nchez. #Octave #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2010.16302\">Programming metamorphic algorithms: An experiment in type-driven algorithm design<\/a>. ~ Hsiang-Shang Ko. #ITP #Agda #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=242\">Formas normales, cl\u00e1usulas y algoritmo DPLL<\/a>. ~ Fernando Sancho. #L\u00f3gica<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/inside-the-secret-math-society-known-as-nicolas-bourbaki-20201109\/\">Inside the secret math society known simply as Nicolas Bourbaki<\/a>. ~ Kevin Hartnett. #Math<\/li>\n<li><a href=\"https:\/\/zoep.github.io\/thesis_final.pdf\">Verified optimizations for functional languages<\/a>. ~ Zoe Paraskevopoulou. #ITP #Coq #PhD_Thesis<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s40593-020-00222-2.pdf\">Generation and use of hints and feedback in a Hilbert-style axiomatic proof tutor<\/a>. ~ Josje Lodder, Bastiaan Heeren, Johan Jeuring, Wendy Neijenhuis. #Logic #Teaching<\/li>\n<li><a href=\"https:\/\/reasonablypolymorphic.com\/blog\/separate-your-views-reify-your-reasoning\/\">Separate your views; reify your reasoning<\/a>. ~ Sandy Maguire. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.haskellforall.com\/2020\/11\/pretty-print-syntax-trees-with-this-one.html\">Pretty-print syntax trees with this one simple trick<\/a>. ~ Gabriel Gonzalez. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/gist.github.com\/digikar99\/a1925ad3249a431c9eecf09af2fdef8a\">Opinionated Common Lisp resources 2020<\/a>. ~ Shubhamkar Ayare. #Programming #CommonLisp<\/li>\n<li><a href=\"https:\/\/blog.sulami.xyz\/posts\/writing-for-reasons\/index.html\">Writing for reasons<\/a>. ~ Robin Schroer.<\/li>\n<li><a href=\"https:\/\/medium.com\/cantors-paradise\/category-theory-the-math-behind-mathematics-7143af49f0ae\">Category theory: The math behind mathematics<\/a>. ~ Cole Persch. #Math #CategoryTheory<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2003.09993v3\">A trustful monad for axiomatic reasoning with probability and nondeterminism<\/a>. ~ Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2011.00720v1\">Towards a certified reference monitor of the Android 10 permission system<\/a>. ~ Guido De Luca, Carlos Luna. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/ifazk.com\/pubs\/idot-oopsla20.pdf\">\u03b9DOT: A DOT calculus with object initialization<\/a>. ~ Ifaz Kabir, Yufeng Li, Ond\u0159ej Lhot\u00e1k. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/www.csl.sri.com\/users\/rushby\/papers\/ontargbegsvac20.pdf\">A mechanically assisted examinationof vacuity and question beggingin Anselm\u2019s ontological argument<\/a>. ~ John Rushby. #ITP #PVS<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/Joosep_Jaeaeger\/publication\/344905880_Implementation_of_affine_arithmetic_in_Haskell\/links\/5f987a87a6fdccfd7b84a8a9\/Implementation-of-affine-arithmetic-in-Haskell.pdf\">Implementation of affine arithmetic in Haskell<\/a>. ~ Joosep J\u00e4\u00e4ger. #BSc_Thesis #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/www.michaelpj.com\/blog\/2020\/10\/29\/your-orphans-are-fine.html\">Your orphan instances are probably fine<\/a>. ~ Michael Peyton Jones. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/iokasimov.github.io\/posts\/2020\/10\/arrow-and-comma\">A story of an arrow and a comma<\/a>. ~ Murat Kasimov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=241\">Construir un buscador (en espacios de estados) desde cero<\/a>. ~ Fernando Sancho. #Algoritmos #IA<\/li>\n<li><a href=\"https:\/\/htmlpreview.github.io\/?https:\/\/github.com\/effectfully\/inference-in-agda\/blob\/master\/InferenceInAgda.html\">Inference in Agda (a tutorial on how Agda infers things)<\/a>. ~ Andreas Abel. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/mcorbin.fr\/pdf\/slides\/clojure_snowcamp.pdf\">Clojure en production<\/a>. ~ Mathieu Corbin. #Clojure<\/li>\n<li><a href=\"https:\/\/www.lambdabetaeta.eu\/talks\/domains-logsem-2020.pdf\">How to define things by recursion<\/a>. ~ Alex Kavvos. #Logic #Math<\/li>\n<li><a href=\"https:\/\/dpt-info.u-strasbg.fr\/~narboux\/slides\/slides_toulouse.pdf\">Les assistants de preuve et applications \u00e0 l\u2019apprentissage du raisonnement math\u00e9matique<\/a>. ~ Julien Narboux. #Logic #Math #ITP<\/li>\n<li><a href=\"https:\/\/haskell.foundation\/whitepaper\/\">A new chapter for Haskell: The Haskell Foundation<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.proofsociety.org\/the-proof-manifesto\/\">The Proof Manifesto<\/a>. #Logic<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/quantification\/\">Quantifiers and quantification<\/a>. ~ Gabriel Uzquiano. #Logic<\/li>\n<li><a href=\"https:\/\/culturacientifica.com\/2020\/11\/04\/mas-rompecabezas-matematicos-con-numeros\/\">M\u00e1s rompecabezas matem\u00e1ticos con n\u00fameros<\/a>. ~ Ra\u00fal Ib\u00e1\u00f1ez. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/adventofhaskell.com\/\">Advent of Haskell 2020 (Call for participation)<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/cantors-paradise\/the-nature-of-infinity-and-beyond-a05c146df02c\">The nature of infinity \u2014 and beyond (An introduction to Georg Cantor and his transfinite paradise)<\/a>. ~ J\u00f8rgen Veisdal. #Logic #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2010.14648\">Formally verified SAT-based AI planning<\/a>. ~ Mohammad Abdulaziz, Friedrich Kurz. #ITP #IsabelleHOL #AI<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/344864795_An_Analysis_of_Implementing_PVS_in_SPARK_Ada\">An analysis of implementing PVS in SPARK Ada<\/a>. ~ A. Benjamin Hocking, Jonathan C. Rowanhill, Ben L Di Vito. #ITP #PVS<\/li>\n<li><a href=\"https:\/\/fenix.tecnico.ulisboa.pt\/downloadFile\/1689244997260666\/tese_maria_ribeiro.pdf\">Formal verification of Ethereum smart contracts using Isabelle\/HOL<\/a>. ~ Maria Saraiva de Campos Mendes Ribeiro. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/semantic.org\/post\/whole-haskell-is-best-haskell\/\">Whole Haskell is best Haskell<\/a>. ~ Ashley Yakeley. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2002.07019\">Learning to prove theorems by learning to generate theorems<\/a>. ~ Mingzhe Wang, Jia Deng. #ATP #ITP #MachineLearning<\/li>\n<li><a href=\"https:\/\/dev.to\/moniquelive\/haskell-lsp-bonus-for-vim-4nlj\">Haskell LSP (bonus: for Vim)<\/a>. ~ Monique Oliveira. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/people.cs.umass.edu\/~brun\/pubs\/pubs\/First20oopsla.pdf\">TacTok: Semantics-aware proof synthesis<\/a>. ~ Emily First, Yuriy Brun, Arjun Guha. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/link.springer.com\/article\/10.1007\/s00283-020-10006-0\">Big Math and the one-brain barrier: The tetrapod model of mathematical knowledge<\/a>. ~ Jacques Carette, William M. Farmer, Michael Kohlhase, Florian Rabe. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/eprint.iacr.org\/2020\/1331.pdf\">Efficient mixing of arbitrary ballots with everlasting privacy: How to verifiably mix the PPATC scheme <\/a>. ~ Kristian Gj\u00f8steen, Thomas Haines, Morten Rotvold Solberg. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/bergsans\/glossy-haskell-game\">Glossy Haskell game<\/a>. ~ Claes-Magnus Berg. #Haskell #FunctionalProgramming #Game<\/li>\n<li><a href=\"https:\/\/chrispenner.ca\/posts\/witherable-optics\">Composable filters using Witherable optics<\/a>. ~ Chris Penner. #Haskell #FunctionalProgramming<\/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 noviembre 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\/7593"}],"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=7593"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7593\/revisions"}],"predecessor-version":[{"id":7594,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7593\/revisions\/7594"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7593"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7593"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7593"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}