{"id":7597,"date":"2021-02-01T19:17:34","date_gmt":"2021-02-01T18:17:34","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7597"},"modified":"2021-08-30T19:18:47","modified_gmt":"2021-08-30T17:18:47","slug":"resumen-de-lecturas-compartidas-durante-enero-de-2021","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-enero-de-2021\/","title":{"rendered":"Resumen de lecturas compartidas durante enero de 2021"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante enero 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>.<br \/>\n<!--more--><\/p>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/www.bbc.com\/mundo\/noticias-55815156\">Paul Cohen, el matem\u00e1tico que por resolver un problema termin\u00f3 creando dos mundos<\/a>. ~ Dalia Ventura. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/kilthub.cmu.edu\/ndownloader\/files\/26180729\">HELIX: From math to verified code<\/a>. ~ Vadim Zaliva. #PhD_Thesis #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/repository.tudelft.nl\/islandora\/object\/uuid:54b01377-1f79-4758-b79b-4859df05dbd6\">Implementing the decomposition of soundness proofs of abstract interpreters in Coq<\/a>. ~ Jens de Waard. #MSc_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2101.09699\">Longest segment of balanced parentheses: an exercise in program inversion in a segment problem (Functional Pearl)<\/a>. ~ Shin-Cheng Mu, Tsung-Ju Chiang. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2101.09700\">A greedy algorithm for dropping digits (Functional Pearl)<\/a>. ~ Richard Bird, Shin-Cheng Mu. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2021\/01\/28\/formalising-mathematics-workshop-2\">Formalising mathematics: Workshop 2 (Groups and subgroups)<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/mjj.io\/2021\/01\/26\/building-a-passphrase-generator-in-haskell\/\">Building a passphrase generator in Haskell<\/a>. ~ Mathias Jean Johansen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/g2--VL2SkMo\">What do we mean by equality?<\/a> ~ Kevin Buzzard. #Logic #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/ehlXpfFuLvI\">\u00bfCu\u00e1ntos infinitos existen?\ufe0f El teorema de Cantor<\/a>. ~ Urtzi Buijs. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/6585eff99deca6bb21ae0c84c5c7b609c0406189\/archive\/imo\/imo2013_q5.lean\">IMO 2013 Q5 in Lean<\/a>. ~ David Renshaw. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2101.11501\">Evolution of artificial intelligence languages, a systematic literature review<\/a>. ~ Emmanuel Adetiba, Temitope John, Adekunle Akinrinmade, Funmilayo Moninuola, Oladipupo Akintade, Joke Badejo. #AI #Programming<\/li>\n<li><a href=\"https:\/\/tecdigital.tec.ac.cr\/revistamatematica\/Libros\/LaTeX\/LaTeX_2018.pdf\">Edici\u00f3n de textos cient\u00edficos con LaTeX<\/a>. (Composici\u00f3n, gr\u00e1ficos, Inkscape, Tikz y presentaciones Beamer). ~ Alex\u00e1nder Borb\u00f3n, Walter Mora. #LaTeX<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/1eb1293706c569ef94776d63fd4900923cc66270\/archive\/imo\/imo2011_q3.lean\">IMO 2011 Q3 in Lean<\/a>. ~ David Renshaw. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3437992.3439910\">Teaching algorithms and data structures with a proof assistant<\/a>. ~ Tobias Nipkow. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/lmcs.episciences.org\/7124\/pdf\">2-Adjoint equivalences in Homotopy Type Theory<\/a>. ~ Daniel Carranza, Jonathan Chang, Krzysztof Kapulkin, Ryan Sandford. #ITP #LeanProver #HoTT<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2101.10166\">The Agda universal algebra library and Birkhoff&#8217;s theorem in Martin-L\u00f6f dependent type theory<\/a>. ~ William DeMeo. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3437992.3439924\">Formal verification of authenticated, append-only skip lists in Agda<\/a>. ~ Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, Guy L. Steele Jr. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/atcm.mathandtech.org\/EP2020\/invited\/21810.pdf\">A Haskell implementation of the Lyness-Moler\u2019s numerical differentiation algorithm<\/a>. ~ Weng Kin Ho, Chu Wei Lim. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/magazines\/2021\/2\/250078-lets-not-dumb-down-the-history-of-computer-science\/fulltext\">Let&#8217;s not dumb down the history of computer science<\/a>. ~ Donald E. Knuth, Len Shustek. #CompSci<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2021\/01\/24\/formalising-mathematics-workshop-1\">Formalising mathematics: workshop 1<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.johndcook.com\/blog\/2021\/01\/23\/sums-of-consecutive-reciprocals\/\">Sums of consecutive reciprocals<\/a>. ~ John D. Cook. #Math<\/li>\n<li><a href=\"https:\/\/republicaweb.es\/podcast\/descubriendo-la-programacion-funcional-lisp-con-diego-sevilla\/\">Descubriendo la programaci\u00f3n funcional: Lisp con Diego Sevilla<\/a>. #Lisp #CommonLisp #Programaci\u00f3nFuncional12<\/li>\n<li><a href=\"https:\/\/youtu.be\/4d6B1C0wuaE\">Las bases matem\u00e1ticas de la programaci\u00f3n funcional<\/a>. ~ H\u00e9ctor Iv\u00e1n Patricio Moreno. #Programaci\u00f3nFuncional<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2101.06759\">Proceedings of the 2020 Scheme and Functional Programming Workshop<\/a>. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2101.06317\">Machine-learning mathematical structures<\/a>. ~ Yang-Hui He. #MachineLearning #Math<\/li>\n<li><a href=\"https:\/\/www.nature.com\/articles\/d41586-021-00075-2\">Ten computer codes that transformed science<\/a>. ~ Jeffrey M. Perkel. #CompSci via @vardi<\/li>\n<li><a href=\"https:\/\/notxor.nueva-actitud.org\/2021\/01\/22\/tablas-para-calculos-en-org-mode.html\">Tablas para c\u00e1lculos en org-mode<\/a>. #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/www.lambdabytes.io\/posts\/teachinghaskell\/\">Teaching Haskell means teaching important concepts<\/a>. ~ Jonathan Thaler. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2021\/01\/21\/formalising-mathematics-an-introduction\/\">Formalising mathematics: an introduction<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/maksbotan.github.io\/posts\/2021-01-20-callstacks.html\">Capturing call stack with Haskell exceptions<\/a>. ~ Maxim Koltsov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/lispcookbook.github.io\/cl-cookbook\">The Common Lisp Cookbook [in EPUB and PDF format<\/a>].\/#download-in-epub #eBook #CommonLisp<\/li>\n<li><a href=\"https:\/\/www.gaussianos.com\/el-numero-de-dottie\/\">El n\u00famero de Dottie<\/a>. ~ M.A. Morales. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/raw.githubusercontent.com\/DSLsofMath\/DSLsofMath\/master\/L\/snapshots\/DSLsofMathBook_snapshot_2021-01-17.pdf\">Domain-specific languages of Mathematics [Draft of January 17, 2021<\/a>]. ~ Patrik Jansson, Cezar Ionescu, Jean-Philippe Bernardy. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/github.com\/DSLsofMath\/DSLsofMath\">DSLsofMath: Domain-specific languages of Mathematics [Repo<\/a>]. ~ Patrik Jansson et als. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/S4xl0CtJIb4\">A novice-friendly induction tactic for Lean<\/a>. ~ Jannis Limperg. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/bor0.wordpress.com\/2021\/01\/18\/towards-hoare-logic-for-a-small-imperative-language-in-haskell\/\">Towards Hoare logic for a small imperative language in Haskell<\/a>. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.informatics-europe.org\/images\/ECSS\/ECSS2009\/slides\/Gottlob.pdf\">Computer Science as the continuation of Logic by other means<\/a>. ~ Georg Gottlob. #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/lt2021\/slides\/thomas-LT2021-Galois-Theory.pdf\">Formalizing Galois Theory in Lean [Slides<\/a>]. ~ Thomas Browning, Patrick Lutz. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/-6z6qTD_vv8\">Formalizing Galois Theory in Lean [V\u00eddeo<\/a>]. ~ Thomas Browning, Patrick Lutz. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/bit.ly\/2XPH8Iq\">Las Matem\u00e1ticas son suficientes para m\u00ed<\/a>. ~ Juan Arias de Reyna. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/alhassy.github.io\/org-special-block-extras\">org-special-block-extras (A unified interface for special blocks and links: defblock)<\/a>. ~ Musa Al-hassy.\/#Judgements-Inference-rules-and-proof-trees #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/youtu.be\/pMCZFrii4lA\">Model theory in Lean<\/a>. ~ Vaibhav Karve. #ITP #LeanProver #Logic<\/li>\n<li><a href=\"http:\/\/people.rennes.inria.fr\/Assia.Mahboubi\/assia_hdr_thesis.pdf\">Machine-checked computer-aided mathematics<\/a>. ~ Assia Mahboubi. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/martin.desharnais.me\/public\/documents\/cpp2021-Dyn-Inca-Ubx.pdf\">Towards efficient and verified virtual machines for dynamic languages<\/a>. ~ Martin Desharnais, Stefan Brunthaler. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/youtu.be\/wOQuW6QFdos\">From Aristotle to the iPhone<\/a>. ~ Moshe Y. Vardi. #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/vaibhavkarve.github.io\/leanteach_2020.html\">Axiomatic Geometry in Lean<\/a>. ~ Vaibhav Karve, Lawrence Zhao, Edward Kong, Alex Dolcos, Nicholas Phillips. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/K-kLck8BvDM\">Axiomatic Geometry in Lean [Video<\/a>]. ~ Vaibhav Karve. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/github.com\/vaibhavkarve\/leanteach2020\">Axiomatic Geometry in Lean [Code<\/a>]. ~ Vaibhav Karve, Lawrence Zhao, Edward Kong, Alex Dolcos, Nicholas Phillips. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2101.05678\">Lebesgue integration<\/a>. (Detailed proofs to be formalized in Coq). ~ Fran\u00e7ois Cl\u00e9ment, Vincent Martin. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/juliu.is\/permutate-parsers\/\">Permutate parsers, don&#8217;t validate<\/a>. ~ Ju Liu. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/9zuAsGk9xoM\">An introduction to ghc-debug: precise memory analysis for Haskell programs<\/a>. ~ Matthew Pickering. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/tek.brick.do\/a6d9388a-208e-4b18-a219-85457faf69aa\">Why exactly I want Boring Haskell to happen<\/a>. ~ Artyom Kazak. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/cantors-paradise\/beginners-guide-to-mathematical-constructivism-4015ca66825d\">Beginner\u2019s guide to mathematical constructivism<\/a>. ~ Jan Gronwald. #Math<\/li>\n<li><a href=\"https:\/\/interstices.info\/en-toute-logique-une-origine-de-lordinateur\/\">En toute logique: une origine de l\u2019ordinateur<\/a>. ~ Fr\u00e9d\u00e9ric Prost. #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/notxor.nueva-actitud.org\/2021\/01\/13\/publicar-html-con-org-mode.html\">Publicar HTML con Org-Mode<\/a>. #Emacs #OrgMode<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/software\/fortissimo\/cpp2021\/paper.pdf\">A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems<\/a>. ~ Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, Bertram Felgenhauer. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1911.00385\">A formal proof of PAC learnability for decision stumps<\/a>. ~ Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, Jean-Baptiste Tristan. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/1509c2950946374803b265830452880816e0f0c1\/archive\/100-theorems-list\/83_friendship_graphs.lean\">The friendship theorem in Lean<\/a>. ~ Aaron Anderson. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.11403\">CertRL: Formalizing convergence proofs for value and policy iteration in Coq<\/a>. ~ Koundinya Vajjha, Avraham Shinnar, Vasily Pestun, Barry Trager, Nathan Fulton. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/math-comp\/Abel\">Abel-Ruffini Theorem as a Mathematical Component<\/a>. ~ Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/cronokirby.com\/posts\/2021\/01\/making-an-io\/\">Making an IO<\/a>. ~ L\u00fac\u00e1s Meier. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.cs.au.dk\/~birke\/papers\/2021-ms-queue.pdf\">Contextual refinement of the Michael-Scott queue (Proof pearl)<\/a>. ~ Simon Friis Vindum, Lars Birkedal. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/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-verimag.imag.fr\/~monin\/Publis\/Docs\/datalog-cpp21.pdf\">Developing and certifying Datalog optimizations in Coq\/MathComp<\/a>. ~ Pierre-L\u00e9o B\u00e9gay, Pierre Cr\u00e9gut, Jean-Fran\u00e7ois Monin. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/isafor\/papers\/cpp2021.pdf\">An Isabelle\/HOL formalization of AProVE&#8217;s termination method for LLVM IR<\/a>. ~ Max W. Haslbeck, Ren\u00e9 Thiemann. #ITP #IsabelleHOL #Haskell<\/li>\n<li><a href=\"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09584-7\">Certified quantum computation in Isabelle\/HOL<\/a>. ~ Anthony Bordg, Hanna Lachnitt, Yijun He. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/alexjbest.github.io\/talks\/lean-generalisation\">Automatically generalising theorems using typeclasses in Lean [Slides<\/a>]. ~ Alex J. Best.\/#\/#ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/bostonu.zoom.us\/rec\/play\/yPZ5hwU7T5C2wwAUYMKEwed7Y83lsvPEci6CP-AiIel8A9u05OHbOLcAy-mi__tqgg3vBDvhXc4wVY_p.B9N6zDkf2SMpf2Nh?startTime=1609940780000\">Automatically generalising theorems using typeclasses in Lean [Video<\/a>]. ~ Alex J. Best. #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?LFMTP2020.4.pdf\">Implementation of two layers type theory in Dedukti and application to Cubical Type Theory<\/a>. ~ Bruno Barras, Valentin Maestracci. #ITP #Dedukti<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2021\/01\/12\/lean-together-2021\/\">Lean Together 2021<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.07059\">Formalizing category theory in Agda<\/a>. ~ Jason Z.S. Hu, Jacques Carette. #ITP #Agda #CategoryTheory #Math<\/li>\n<li><a href=\"https:\/\/shemesh.larc.nasa.gov\/people\/amd\/publications\/CPP2021-SAS_RA-draft.pdf\">Formal verification of semi-algebraic sets and real analytic functions<\/a>. ~ J. Tanner Slagel, Lauren White, Aaron Dutle. #ITP #PVS #Math<\/li>\n<li><a href=\"https:\/\/www.dropbox.com\/s\/q1whqz0v2c0falm\/CPP2021-Kolmogorov-complexity.pdf?dl=0\">On the formalisation of Kolmogorov complexity<\/a>. ~ Elliot Catt, Michael Norrish. #ITP #HOL4<\/li>\n<li><a href=\"https:\/\/melkornemesis.medium.com\/haskell-explained-3f91658a67d3\">Haskell: (.) . (.) explained (Let\u2019s get a grasp of composition equivalences in Haskell)<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/k-YncL7Cd4Q\">Formalizing the ring of Witt vectors<\/a>. ~ Robert Y. Lewis. #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?LFMTP2020.1.pdf\">Mechanisation of model-theoretic conservative extension for HOL with ad-hoc overloading<\/a>. ~ Arve Gengelbach, Johannes \u00c5man Pohjola, Tjark Weber. #ITP #HOL4<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?LFMTP2020.2.pdf\">Object-level reasoning with logics encoded in HOL Light<\/a>. ~ Petros Papapanagiotou, Jacques Fleuriot. #ITP #HOL_Light #Logic<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?LFMTP2020.3.pdf\">Deductive systems and coherence for skew prounital closed categories<\/a>. ~ Tarmo Uustalu, Niccol\u00f2 Veltri, Noam Zeilberger. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/www.foxhound.systems\/blog\/why-haskell-for-production\/\">Why Haskell is our first choice for building production software systems<\/a>. ~ Christian Charukiewicz. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/mhk119\/fibonacci_squares\">144 is the largest square in the Fibonacci Sequence (A formalisation of Cohn&#8217;s Proof)<\/a>. ~ Harun Khan #ITP #LeanProver #Math via @XenaProject<\/li>\n<li><a href=\"https:\/\/github.com\/Lix0120\/eudoxus\/\">The Eudoxus real numbers in Lean<\/a>. ~ Xiang Li. #ITP #LeanProver #Math via @XenaProject<\/li>\n<li><a href=\"http:\/\/wwwf.imperial.ac.uk\/~buzzard\/xena\/pdfs\/Set_theory_Type_Theory_and_the_future_of_Proof_verification_software.pdf\">Set theory, type theory and the future of proof verification software<\/a>. ~ James Palmer. #ITP #LeanProver #Math via @XenaProject<\/li>\n<li><a href=\"https:\/\/github.com\/mdickinson\/snippets\/blob\/master\/proofs\/isqrt\/src\/isqrt.lean\">A formal proof of correctness of a recursive integer square root algorithm<\/a>. ~ Mark Dickinson. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2101.02602\">Schemes in Lean<\/a>. ~ Kevin Buzzard, Chris Hughes, Kenny Lau, Amelia Livingston, Ramon Fern\u00e1ndez Mir, Scott Morrison. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/user.informatik.uni-bremen.de\/fritjof\/pdfs\/performance-aspects-of-correctness-oriented-synthesis-flows.pdf\">Performance aspects of correctness-oriented synthesis flows<\/a>. ~ F. Bornebusch, C. L\u00fcth, R. Wille, R. Drechsler. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-03096253\/document\">An anti-locally-nameless approach to formalizing quantifiers<\/a>. ~ Olivier Laurent. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.13761\">Formal verification of arithmetic RTL: Translating Verilog to C++ to ACL2<\/a>. ~ David M. Russinoff. #ITP #ACL2<\/li>\n<li><a href=\"http:\/\/www.cs.ru.nl\/~freek\/100\">Formalizing 100 theorems<\/a>. ~ Freek Wiedijk. #ITP #Math<\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/100.html\">Formalizing 100 theorems in Lean<\/a>. #ITP #Math #LeanProver<\/li>\n<li><a href=\"https:\/\/github.com\/effectfully\/sketches\/tree\/master\/trouble-in-paradise-fibonacci\">Trouble in paradise: Fibonacci<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/oleg.fi\/gists\/posts\/2021-01-08-indexed-optics-dilemma.html\">Indexed optics dilemma<\/a>. ~ Oleg Grenrus. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/jsannemo.se\/aps.pdf\">Algorithmic problem solving<\/a>. ~ Johan Sannemo. #eBook #Programming #Algorithms<\/li>\n<li><a href=\"https:\/\/www.gaussianos.com\/la-saga-del-infinito-de-mates-mike\/\">La saga del infinito, de Mates Mike<\/a>. ~ M.A. Morales. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/youtu.be\/eSXiClL4COw\">LeanStep: a dataset and environment for (interactive) neural theorem proving [Video<\/a>]. ~ Jason Rute. #ITP #Leanprover #MachineLearning<\/li>\n<li><a href=\"https:\/\/docs.google.com\/presentation\/d\/1poOu2gP9mSGAdAFvOupHvf4tpgD33jACQLJAVcphA1g\/edit?usp=sharing\">LeanStep: a dataset and environment for (interactive) neural theorem proving [Slides<\/a>]. ~ Jason Rute. #ITP #Leanprover #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2101.02690\">Theorem proving and algebra<\/a>. ~ Joseph A. Goguen. #eBook #ITP #Math<\/li>\n<li><a href=\"https:\/\/www.michaelpj.com\/blog\/2021\/01\/02\/elementary-programming.html\">Elementary programming<\/a>. ~ Michael Peyton Jones. #Haskell #Programming<\/li>\n<li><a href=\"https:\/\/well-typed.com\/blog\/2021\/01\/first-look-at-hi-profiling-mode\/\">A first look at info table profiling<\/a>. ~ Matthew Pickering, David Eichmann. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/oleg.fi\/gists\/posts\/2021-01-07-discrimination-benchmarks.html\">Benchmarks of discrimination package<\/a>. ~ Oleg Grenrus. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.metalevel.at\/prolog\/clpz\">CLP(FD) and CLP(\u2124): Prolog integer arithmetic<\/a>. ~ Markus Triska. #Prolog #LogicProgramming #CLP<\/li>\n<li><a href=\"https:\/\/eclipseclp.org\/doc\/tutorial.pdf\">ECLIPSE (A tutorial introduction)<\/a>. ~ Andrew M. Cheadle et als. #Prolog #LogicProgramming #CLP<\/li>\n<li><a href=\"https:\/\/www.cs.us.es\/~jalonso\/cursos\/d-pl-03\/temas\/tema-8.pdf\">Programaci\u00f3n l\u00f3gica con restricciones<\/a>. #Prolog #CLP<\/li>\n<li><a href=\"https:\/\/www.cs.us.es\/~jalonso\/apuntes\/Soluciones_logicas_de_problemas_logicos\/Tema_2.html\">Soluciones l\u00f3gicas de problemas l\u00f3gicos<\/a>. #Prolog #Programaci\u00f3nL\u00f3gica #CLP<\/li>\n<li><a href=\"https:\/\/www.cs.utexas.edu\/users\/moore\/publications\/acl2-induction-heuristics.pdf\">ACL2 induction heuristics<\/a>. ~ J Strother Moore. #ITP #ACL2<\/li>\n<li><a href=\"https:\/\/youtu.be\/cLuEaAsUvL4\">Word problem for one-relator groups<\/a>. ~ Chris Hughes. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/github.com\/gihanmarasingha\/mth1001_tutorial\">A Lean introduction to pure mathematics<\/a>. ~ Gihan Marasingha. #ITP #LeanProver #Logic #Math<\/li>\n<li><a href=\"https:\/\/github.com\/gihanmarasingha\/mth1001_sphinx\">MTH1001 (Mathematical structures) in Lean<\/a>. ~ Gihan Marasingha. #ITP #LeanProver #Logic #Math<\/li>\n<li><a href=\"https:\/\/github.com\/gihanmarasingha\/ems_reals\">EMS reals (A project for investigating the real number system via the interactive theorem prover Lean)<\/a>. ~ Gihan Marasingha. #ITP #LeanProver #Logic #Math<\/li>\n<li><a href=\"https:\/\/people.mpi-sws.org\/~eva\/papers\/cpp2021.pdf\">Lassie: HOL4 tactics by example<\/a>. ~ Heiko Becker et als.. #ITP #HOL4<\/li>\n<li><a href=\"https:\/\/gupea.ub.gu.se\/bitstream\/2077\/67193\/1\/gupea_2077_67193_1.pdf\">Formalizing domain models of the typed and the untyped lambda calculus in Agda<\/a>. ~ David Lidell. #MSc_Thesis #ITP #Agda<\/li>\n<li><a href=\"https:\/\/www.cs.rice.edu\/~vardi\/papers\/SATSolvers21.pdf\">On the unreasonable effectiveness of SAT Solvers<\/a>. ~ Vijay Ganesh, Moshe Y. Vardi. #Logic #ATP #SAT_Solvers<\/li>\n<li><a href=\"https:\/\/github.com\/bhgomes\/lean-riemann-hypothesis\">Riemann Hypothesis in Lean<\/a>. ~ Brandon H. Gomes, Alex Kontorovich. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/lt2021\/slides\/Macbeth-slides.pdf\">An example of a manifold [Slides<\/a>]. ~ Heather Macbeth. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/deppJ2q_5a0\">An example of a manifold [Video<\/a>]. ~ Heather Macbeth. #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/maude.cs.illinois.edu\/w\/images\/7\/70\/Maude-tapas.pdf\">Symbolic computation in Maude: Some tapas<\/a>. ~ Jos\u00e9 Meseguer. #ITP #Maude<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/compile-time-evaluation-haskell\">Compile-time evaluation in Haskell<\/a>. ~ Vladislav Zavialov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/rjlipton.wordpress.com\/2021\/01\/05\/predictions-for-2021\/\">Predictions for 2021<\/a>. | G\u00f6del\u2019s Lost Letter and P = NP. ~ R.J. Lipton &amp; K.W. Regan. #CompSci<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2101.00127\">Formalizing Hall&#8217;s Marriage Theorem in Lean<\/a>. ~ Alena Gusakov, Bhavik Mehta, Kyle A. Miller. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/pdfs\/masters-thesis.pdf\">Finiteness in cubical type theory<\/a>. ~ Donnacha Ois\u00edn Kidney. #MSc_Thesis #ITP #Agda #HoTT<\/li>\n<li><a href=\"https:\/\/youtu.be\/UeGvhfW1v9M\">An overview of Lean 4<\/a>. ~ Leonardo de Moura, Sebastian Ullrich. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/lt2021\/slides\/floris-measure.pdf\">Measure theory in Lean [slides<\/a>]. ~ Floris van Doorn. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/yH3-zE0bYCU\">Measure theory in Lean<\/a>\n<p><a href=\"https:\/\/youtu.be\/yH3-zE0bYCU\">. ~ Floris van Doorn. #ITP #LeanProver #Math<\/a><\/li>\n<li><a href=\"https:\/\/www.haskellforall.com\/2021\/01\/the-visitor-pattern-is-essentially-same.html\">The visitor pattern is essentially the same thing as Church encoding<\/a>. ~ Gabriel Gonzalez. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cs.nott.ac.uk\/~pszgmh\/123.pdf\">Functional Pearl: It\u2019s easy as 1,2,3<\/a>. ~ Graham Hutton. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/iokasimov.github.io\/posts\/2021\/01\/composable-monad-transformers\">Trying to compose non-composable: monads<\/a>. ~ Murat Kasimov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/l13D-CcwM5A\">Learning TypeFamilies together! ~ Flavio Corpa<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/ceur-ws.org\/Vol-2710\/paper21.pdf\">Tautology checkers in Isabelle and Haskell<\/a>. ~ J\u00f8rgen Villadsen. #Logic #ITP #IsabelleHOL #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/ceur-ws.org\/Vol-2710\/paper13.pdf\">Theorem proving for Lewis logics of counterfactual reasoning<\/a>. ~ Marianna Girlando, Bjoern Lellmann, Nicola Olivetti, Stefano Pesce, Gian Luca Pozzato. #ATP #Logic #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/384ba88bf56209e52a0bed1b7176805c09b05c9a\/src\/computability\/DFA.lean\">Deterministic Finite Automata (DFA) in Lean<\/a>. ~ Fox Thomson. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/384ba88bf56209e52a0bed1b7176805c09b05c9a\/src\/computability\/NFA.lean\">Nondeterministic Finite Automata (NFA) in Lean<\/a>. ~ Fox Thomson. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/blog.poisson.chat\/posts\/2021-01-03-iterative-categories.html\">Theory of iteration and recursion<\/a>. ~ Li-yao Xia. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/bindthegap.news\/issues\/02dec2020.html\">Bind the gap (Monthly digital functional programming magazine) [Issue 2, Dec 2020<\/a>]. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.parsonsmatt.org\/2020\/02\/04\/mirror_mirror.html%20https:\/\/www.parsonsmatt.org\/2020\/02\/04\/mirror_mirror.html\">Mirror mirror: Reflection and encoding via<\/a>. ~ Matt Parsons. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/wespiser.com\/posts\/2021-01-03-Lessons-Learned-From-A-Year-Of-Haskell.html\">Lessons learned from a year of writing Haskell<\/a>. ~ Adam Wespiser. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/oleg.fi\/gists\/posts\/2021-01-04-coindexed-optics.htm\">Coindexed optics<\/a>. ~ Oleg Grenrus.l#Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/04f8fd744a1d8e9f5aec9fd8d4809d4345365916\/src\/group_theory\/dihedral.lean\">Dihedral groups in Lean<\/a>. ~ Shing Tak Lam. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2012.14133v1\">Verifying C11-style weak memory libraries<\/a>. ~ Sadegh Dalvandi, Brijesh Dongol. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/leanprover.github.io\/lean4\/doc\/whatIsLean.html\">Lean 4 manual<\/a>. #Lean4 #FunctionalProgramming #ITP<\/li>\n<li><a href=\"https:\/\/www.mdpi.com\/2227-7390\/9\/1\/38\/pdf\">Formalization of the equivalence among completeness theorems of real number in Coq<\/a>. ~ Yaoshun Fu, Wensheng Yu. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.lri.fr\/~keller\/Documents-recherche\/Publications\/cpp21.pdf\">A Coq formalization of data provenance<\/a>. V\u00e9ronique Benzaken et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/~kirst\/downloads\/talk_TSEM_20.pdf\">Synthetic undecidability proofs in Coq<\/a>. ~ Dominik Kirst. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/schooloffp.co\/2020\/12\/27\/two-reasons-why-you-found-learning-haskell-hard.html\">Two reasons why you found learning haskell hard<\/a>. ~ School of FP. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/tek.brick.do\/64693fb8-39b4-40a5-8762-768009eeed91\">Learn just enough about linear types<\/a>. ~ Artyom Kazak. #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 enero 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\/7597"}],"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=7597"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7597\/revisions"}],"predecessor-version":[{"id":7598,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7597\/revisions\/7598"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7597"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7597"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7597"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}