{"id":7215,"date":"2020-08-01T18:28:48","date_gmt":"2020-08-01T16:28:48","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7215"},"modified":"2020-08-01T18:28:48","modified_gmt":"2020-08-01T16:28:48","slug":"resumen-de-lecturas-compartidas-durante-julio-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-julio-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas durante julio de 2020"},"content":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante julio 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:\/\/youtu.be\/OEZCp63GES8\">The complex number game, levels 1 to 3<\/a>. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/cs.uwaterloo.ca\/~plragde\/flaneries\/LACI\/\">Logic and computation intertwined<\/a>. ~ Prabhakar Ragde (@plragde). #eBook #Logic #ITP #Agda #Coq<\/li>\n<li><a href=\"https:\/\/cs.uwaterloo.ca\/~plragde\/flaneries\/TYR\/\">Teach yourself Racket<\/a>. ~ Prabhakar Ragde (@plragde). #eBook #Racket #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cs.uwaterloo.ca\/~plragde\/flaneries\/FDS\/\">Functional data structures<\/a>. ~ Prabhakar Ragde (@plragde). #eBook #OCaml #FunctionalProgramming #Algorithms<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/12326\/pdf\/LIPIcs-FSCD-2020-4.pdf\">Certifying the weighted path order<\/a>. ~ R. Thiemann, J. Sch\u00f6pf, C. Sternagel, A. Yamada. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/cs.uwaterloo.ca\/~plragde\/842\/handouts\/notes.html\">Notes on &#8220;Programming language foundations in Agda&#8221;<\/a>. ~ Prabhakar Ragde (@plragde). #eBook #ITP #Agda<\/li>\n<li><a href=\"https:\/\/cs.uwaterloo.ca\/~plragde\/842\/index.html\">Dependent types and software verification<\/a>. ~ Prabhakar Ragde (@plragde). #ITP #Agda<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1611.09473\">Proust: A nano proof assistant<\/a>. ~ Prabhakar Ragde (2016). #Logic #Racket #ITP #Proust<\/li>\n<li><a href=\"https:\/\/compostjs.github.io\/compost\/paper.pdf\">Functional Pearls: Composable data visualizations<\/a>. ~ T. Petricek. #FunctionalProgramming #Fsharp<\/li>\n<li><a href=\"http:\/\/www.jucs.org\/jucs_10_7\/total_functional_programming\/jucs_10_07_0751_0768_turner.pdf\">Total functional programming<\/a>. ~ D.A. Turner (2004). #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2007.01019.pdf\">Higher-order Logic as Lingua franca (Integrating argumentative discourse and deep logical analysis)<\/a>. ~ David Fuenmayor, Christoph Benzm\u00fcller. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2020\/07\/03\/equality-specifications-and-implementations\/\">Equality, specifications, and implementations<\/a>. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math #CompSci<\/li>\n<li><a href=\"http:\/\/www.poberezkin.com\/posts\/2020-06-29-modeling-state-machine-dependent-types-haskell-1.html\">Modeling state machines with dependent types in Haskell: Part 1<\/a>. ~ Evgeny Poberezkin (@epoberezkin). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/mavam\/abstract-algebra-cheatsheet\">Abstract algebra cheatsheet: a visual summary of key structures in abstract algebra<\/a>. ~ Matthias Vallentin. #Math<\/li>\n<li><a href=\"https:\/\/www.ncbi.nlm.nih.gov\/pmc\/articles\/PMC7324036\/pdf\/978-3-030-51054-1_Chapter_14.pdf\">Reasoning about algebraic structures with implicit carriers in Isabelle\/HOL<\/a>. ~ W. Guttmann. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2006.16711.pdf\">Binary intersection formalized<\/a>. ~ \u0160t\u011bp\u00e1n Holub, \u0160t\u011bp\u00e1n Starosta. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.labri.fr\/perso\/casteran\/hydras.pdf\">The hydra and the rooster<\/a>. ~ Pirre Cast\u00e9ran. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.ncbi.nlm.nih.gov\/pmc\/articles\/PMC7324010\/pdf\/978-3-030-51054-1_Chapter_9.pdf\">Teaching automated theorem proving by example: PyRes 1<\/a>.2: (System description). ~ S. Schulz, A. Pease. #ATP #Logic #Python<\/li>\n<li><a href=\"https:\/\/www.philipzucker.com\/unification-in-julia\/\">Unification in Julia<\/a>. ~ Philip Zucker (@SandMouth). #Logic #JuliaLang<\/li>\n<li><a href=\"https:\/\/gist.github.com\/serras\/caf3b7056f609c63a028f15c47a3ff4e\">Some thoughts on building software<\/a>. ~ Alejandro Serrano (@trupill). #FuncionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/rreusser.github.io\/explorations\/sphere-eversion\/\">Sphere eversion<\/a>. ~ Ricky Reusser. #Math<\/li>\n<li><a href=\"https:\/\/www.ncbi.nlm.nih.gov\/pmc\/articles\/PMC7324229\/pdf\/978-3-030-51074-9_Chapter_27.pdf\">Formalizing a Seligman-style tableau system for hybrid logic<\/a>. ~ Asta Halkj\u00e6r From, Patrick Blackburn, J\u00f8rgen Villadsen. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/www.ncbi.nlm.nih.gov\/pmc\/articles\/PMC7309514\/pdf\/978-3-030-51466-2_Chapter_12.pdf\">Prawf: An interactive proof system for program extraction<\/a>. ~ Ulrich Berger, Olga Petrovska, Hideki Tsuiki. #ITP #Haskell #FunctionalProgramming #Logic<\/li>\n<li><a href=\"https:\/\/www.ncbi.nlm.nih.gov\/pmc\/articles\/PMC7324146\/pdf\/978-3-030-51054-1_Chapter_11.pdf\">Formalizing the face lattice of polyhedra<\/a>. ~ Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.ams.org\/journals\/notices\/201806\/rnoti-p681.pdf\">The mechanization of Mathematics<\/a>. ~ Jeremy Avigad (2018). #ITP #Math<\/li>\n<li><a href=\"https:\/\/www.philipzucker.com\/category-theory-in-the-e-automated-theorem-prover\/\">Category theory in the E automated theorem prover<\/a>. ~ Philip Zucker (@SandMouth). #ATP #CategoryTheory<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2020\/07\/05\/division-by-zero-in-type-theory-a-faq\/\">Division by zero in type theory: a FAQ<\/a>. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/odr.chalmers.se\/bitstream\/20.500.12380\/301098\/1\/CSE%2020-12%20Tosun.pdf\">Formal topology in Univalent Foundations<\/a>. ~ Ayberk Tosun. #MsC_Thesis #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/projekter.aau.dk\/projekter\/files\/335444832\/pt101f20thesis.pdf\">Certifying time complexity of Agda programs using complexity signatures<\/a>. ~ Christian Bach M\u00f8llnitz, Johannes Elgaard, Simon Rannes. #Agda #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/codicalist.wordpress.com\/2020\/07\/06\/scientific-proof-oriented-programming-s-pop\/\">Scientific proof-oriented programming (S-pop)<\/a>. ~ Philip Thrift (@philipthrift). #CompSci<\/li>\n<li><a href=\"https:\/\/engineering.fb.com\/open-source\/retrie\/\">Retrie: Haskell refactoring made easy<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/lftcm2020\/\">Lean for the curious mathematician: A virtual workshop on computer-checked mathematics [13\u201317 July 2020<\/a>]. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/github.com\/jjaassoonn\/transcendental\">Theorems in transcendental number theory<\/a>. ~ Jujian Zhang. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/bit.ly\/38JvHGL\">La conjetura de Gilbreath<\/a>. ~ Juan Arias de Reyna. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/www.cs.bham.ac.uk\/~mhe\/HoTT-UF-in-Agda-Lecture-Notes\/index.html\">Introduction to Univalent Foundations of Mathematics with Agda<\/a>. ~ Mart\u00edn H\u00f6tzel Escard\u00f3. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1912.03028v1.pdf\">A survey on theorem provers in formal methods<\/a>. 4 M. Saqib Nawaz, Moin Malik, Yi Li, Meng Sun and M. Ikram Ullah Lali. #ITP #ATP #FormalMethods<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.12876\">A survey of languages for formalizing mathematics<\/a>. ~ Cezary Kaliszyk, Florian Rabe. #ITP #Math<\/li>\n<li><a href=\"http:\/\/paar2020.gforge.inria.fr\/papers\/PAAR_2020_paper_15.pdf\">A micro prover for teaching automated reasoning<\/a>. ~ J. Villadsen. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"http:\/\/ceur-ws.org\/Vol-2634\/FMM4.pdf\">Textbook mathematics in the Naproche-SAD system<\/a>. ~ P. Koepke. #ITP #Math<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/Saed_Abed\/project\/Formal-Analysis-of-Unmanned-Aerial-Vehicles-UAVs-using-Higher-order-Logic-Theorem-Proving\/attachment\/5efc4bd5d52c7c00018087a6\/AS:908408148471809%401593592788923\/download\/Technical%2BReport-uav.pdf\">Formal analysis of unmanned aerial vehicles using higher-order-logic theorem proving<\/a>. ~ Sa\u2019ed Abed, Adnan Rashid, Osman Hasan. #ITP #HOL_Light<\/li>\n<li><a href=\"http:\/\/paar2020.gforge.inria.fr\/papers\/PAAR_2020_paper_20.pdf\">Animated logic: Correct functional conversion to conjunctive normal form<\/a>. ~ Ant\u00f3nio Ravara, M\u00e1rio Pereira, Pedro Barroso. #Logic #Why3<\/li>\n<li><a href=\"http:\/\/ceur-ws.org\/Vol-2634\/FMM1.pdf\">Testing Mizar user interactivity in a University-level introductory course on foundations of Mathematics<\/a>. ~ Adam Naumowicz. #ITP #Mizar #Math<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-019-09516-0.pdf%20\">Strong extension-free proof systems<\/a>. ~ Marijn J H Heule, Benjamin Kiesl, Armin Biere. #SAT<\/li>\n<li><a href=\"https:\/\/freux.fr\/posts\/ogd.html\">Online convex optimization with Haskell<\/a>. ~ Valentin Reis. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2020\/07\/10\/competitive-programming-in-haskell-2d-cross-product-part-1\/\">Competitive programming in Haskell: 2D cross product, part 1<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/siek.blogspot.com\/2020\/07\/type-safety-in-two-easy-lemmas.html\">Type safety in two easy lemmas<\/a>. ~ Jeremy Siek (@jeremysiek). #ITP #Agda<\/li>\n<li><a href=\"https:\/\/alexey.kuleshevi.ch\/blog\/2020\/07\/10\/canny-benchmarks\/\">Performance of Haskell Array libraries through Canny edge detection<\/a>. ~ Alexey Kuleshevich. #Haskell #FuncionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.01917\">Learning selection strategies in Buchberger&#8217;s algorithm<\/a>. ~ Dylan Peifer, Michael Stillman, Daniel Halpern-Leistner. #MachineLearning #Math<\/li>\n<li><a href=\"https:\/\/www.xataka.com\/xataka\/que-matematicas-ha-pasado-ser-carrera-minoritaria-a-codiciadas-moda\">Por qu\u00e9 Matem\u00e1ticas ha pasado de ser una carrera minoritaria a una de las m\u00e1s codiciadas y de moda<\/a>. ~ Carlos Prego. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/williamyaoh.com\/posts\/2020-07-12-deriving-state-monad.html\">Deriving the State monad from first principles<\/a>. ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/2F3tQL-SmgI\">Adventures in verifying arithmetic<\/a>. ~ John Harrison. #ITP #HOL_Light #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/9V1Xo1n_3Qw\">The natural number game : an introduction to Lean tactics<\/a>. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/github.com\/kbuzzard\/xena\/blob\/master\/tactics.md\">The ten (or so) basic tactics<\/a>. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/youtu.be\/b59fpAJ8Mfs\">Infinitude of primes: a Lean theorem prover demo<\/a>. ~ Scott Morrison. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2007.04150\">Certifying emptiness of timed B\u00fcchi automata<\/a>. ~ Simon Wimmer, Fr\u00e9d\u00e9ric Herbreteau, Jaco van de Pol. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/repositorio.yachaytech.edu.ec\/bitstream\/123456789\/153\/1\/ECMC0024.pdf\">Development of a tropical algebraic geometry package in the Haskell programming language<\/a>. ~ Fernando Patricio Zhapa Camacho. #PhD_Thesis #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/repositorio.yachaytech.edu.ec\/bitstream\/123456789\/150\/1\/ECMC0021.pdf\">Optimization of Wu&#8217;s algorithm for the elimination of polynomial variables by High-Performance Computing (HPC)<\/a>. ~ Jos\u00e9 Luis Seraquive Cuenca. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"http:\/\/www.haskellforall.com\/2020\/07\/record-constructors.html\">Record constructors<\/a>. ~ G. Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/blog\/2020-07-13-qualified-do-announcement\/\">Qualified do: rebind your do-notation the right way<\/a>. ~ Matth\u00edas P\u00e1ll Gissurarson, Facundo Dom\u00ednguez, Arnaud Spiwack. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.youtube.com\/playlist?list=PLlF-CfQhukNnq2kDCw2P_vI5AfXN7egP2\">Metaprogramming in Lean<\/a>. ~ Robert Y. Lewis. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/gist.github.com\/jorendorff\/e50832fc9d58722015c7a488cd62c860\">A one-line proof of the infinitude of primes<\/a>. ~ Jason Orendorff. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/MsSlP_P2AkM\">A Lean tactic for normalising ring expressions with exponents<\/a>. ~ Anne Baanen. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/jhISAq4l8iI\">Formalization of forcing in Isabelle\/ZF<\/a>. ~ Pedro S\u00e1nchez Terraf. #ITP #Isabelle #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/A1oXyV27TUI\">The resolution of Keller&#8217;s conjecture<\/a>. ~ Marijn Heule. #ATP #SAT_Solver #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/lw8EfTmWzRU\">Mathematics in Lean introduction<\/a>. ~ Patrick Massot. #ITP #LeanProver #Math #LftCM2020<\/li>\n<li><a href=\"https:\/\/youtu.be\/WGwKefZ8KFo\">Logic in Lean<\/a>. ~ Jeremy Avigad. #ITP #LeanProver #Math #LftCM2020<\/li>\n<li><a href=\"https:\/\/youtu.be\/iEs2U_kzYy4\">Numbers in Lean<\/a>. ~ Rob Lewis. #ITP #LeanProver #Math #LftCM2020<\/li>\n<li><a href=\"https:\/\/youtu.be\/qlJrCtYiEkI\">Sets in Lean<\/a>. ~ Jeremy Avigad. #ITP #LeanProver #Math #LftCM2020<\/li>\n<li><a href=\"https:\/\/www.youtube.com\/playlist?list=PLlF-CfQhukNloaV_NiVvgJt-Pr6lQd56q\">Structures and classes in Lean<\/a>. ~ Floris van Doorn. #ITP #LeanProver #Math #LftCM2020<\/li>\n<li><a href=\"https:\/\/youtu.be\/ATlAQPAtiTY\">Building an algebraic hierarchy in Lean<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math #LftCM2020<\/li>\n<li><a href=\"https:\/\/apurvanakade.github.io\/courses\/lean_at_MC2020\/index.html\">Lean at Mathcamp 2020<\/a>. ~ Apurva Nakade, Jalex Stark. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/RTfjSlwbKjQ\">Building the topological hierarchy in Lean<\/a>. ~ Alex Best. #ITP #LeanProver #Math #LftCM2020<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.09452\">PubSub implementation in Haskell with formal verification in Coq<\/a>. ~ Boro Sitnikovski, Biljana Stojcevska, Lidija Goracinova-Ilieva, Irena Stojmenovska. #Haskell #FunctionalProgramming #ITP #Coq<\/li>\n<li><a href=\"https:\/\/kowainik.github.io\/posts\/2019-02-06-style-guide\">Haskell style guide<\/a>. ~ Kowainik. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/semantic.org\/post\/forbidden-haskell-types\/\">Forbidden Haskell types<\/a>. ~ Ashley Yakeley. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/erkin.party\/blog\/200715\/evolution\/\">The evolution of a Scheme programmer<\/a>. ~ Erkin Batu Altunba\u015f. #Programming #Scheme<\/li>\n<li><a href=\"https:\/\/neilmitchell.blogspot.com\/2020\/07\/managing-haskell-extensions.html\">Managing Haskell extensions<\/a>. ~ Neil Mitchell (@ndm_haskell). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/swlh\/optimizing-ray-tracing-in-haskell-3dc412fff20a\">Optimizing ray tracing in Haskell<\/a>. ~ Sarfaraz Nawaz. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/vsnB7W9nODI\">Order structures in Lean<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math #LftCM2020<\/li>\n<li><a href=\"https:\/\/youtu.be\/SdXvUU75cDA\">Groups, rings, and fields in Lean<\/a>. ~ Johan Commelin. #ITP #LeanProver #Math #LftCM2020<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2020\/07\/17\/lean-for-the-curious-mathematician-2020\/\">Lean for the Curious Mathematician 2020<\/a>. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math #LftCM2020<\/li>\n<li><a href=\"https:\/\/youtu.be\/EnZvGCU_jp\">Linear algebra in Lean<\/a>. ~ Anne Baanen.c#ITP #ITP #LeanProver #Math #LftCM2020<\/li>\n<li><a href=\"https:\/\/youtu.be\/1NUc-ZNC_2s\">Category theory in Lean<\/a>. ~ Scott Morrison. #ITP #LeanProver #Math #LftCM2020<\/li>\n<li><a href=\"https:\/\/youtu.be\/hhOPRaR3tx0\">Topology and filters in Lean<\/a>. ~ Patrick Massot. #ITP #LeanProver #Math #LftCM2020<\/li>\n<li><a href=\"https:\/\/youtu.be\/p8Etfv1_VqQ\">Calculus and integration in Lean<\/a>. ~ Yury Kudryashov. #ITP #LeanProver #Math #LftCM2020<\/li>\n<li><a href=\"https:\/\/lean-forward.github.io\/norm_cast\/norm_cast.pdf\">Simplifying casts and coercions<\/a>. ~ Robert Y. Lewis, Paul-Nicolas Madelaine. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2020\/07\/18\/competitive-programming-in-haskell-cycle-decomposition-with-mutable-arrays\/\">Competitive programming in Haskell: cycle decomposition with mutable arrays<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/1xXRQmhldFs\">Differential geometry in Lean<\/a>. ~ Sebastien Gou\u00ebzel. #ITP #LeanProver #Math #LftCM2020<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2007.06776\">Verification of ML systems via reparameterization<\/a>. ~ Jean-Baptiste Tristan et als. #ITP #LeanProver #MachineLearning<\/li>\n<li><a href=\"https:\/\/bahr.io\/pubs\/files\/bahr21popl2-paper.pdf\">Modal FRP For All (Functional reactive programming without space leaks in Haskell)<\/a>. ~ Patrick Bahr. #Haskell #FunctionalProgramming #ITP #Coq<\/li>\n<li><a href=\"https:\/\/intranet.math.vt.edu\/people\/fquinn\/history_nature\/nature0.pdf\">Contributions to a science of contemporary mathematics<\/a>. ~ Frank Quinn. #Math<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-53518-6_5\">Metamath Zero: Designing a theorem prover prover<\/a>. ~ Mario Carneiro. #ITP #MethamathZero0<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-53518-6_1\">A promising path towards autoformalization and general Artificial Intelligence<\/a>. ~ Christian Szegedy. #MKM #AI #ITP #MachineLearning0<\/li>\n<li><a href=\"https:\/\/das.li\/articles\/linear.html\">Graphics in Haskell: linear algebra<\/a>. ~ David Alexander Stuart. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/dev.to\/techway\/how-to-read-haskell-documentation-step-by-step-guide-12ic\">How to read Haskell Documentation<\/a>. Step by step guide. ~ Theofanis Despoudis. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-53518-6_12\">Formalizing graph trail properties in Isabelle\/HOL<\/a>. ~ Laura Kov\u00e1cs, Hanna Lachnitt, Stefan Szeider. #ITP #IsabelleHOL #Math0<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-53518-6_4\">Leveraging the information contained in theory presentations<\/a>. ~ Jacques Carette, William M. Farmer, Yasmine Sharoda. #ITP #Agda #IsabelleHOL #LeanProver<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-53518-6_7\">A framework for formal dynamic dependability analysis using HOL theorem proving<\/a>. ~ Yassmeen Elderhalli, Osman Hasan, Sofi\u00e8ne Tahar. #ITP #HOL4<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-53518-6_16\">Maintaining a library of formal mathematics<\/a>. ~ Floris van Doorn, Gabriel Ebner, Robert Y. Lewis. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/osf.io\/ag6e9\/download\">Formalizing Henkin-Style completeness of an axiomatic system for propositional logic<\/a>. ~ Asta Halkj\u00e6r From. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2020\/07\/23\/two-types-of-universe-for-two-types-of-mathematician\/\">Two types of universe for two types of mathematician<\/a>. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-53518-6_17\">The Tactician (A seamless, interactive tactic learner and prover for Coq)<\/a>. ~ Lasse Blaauwbroek, Josef Urban, Herman Geuvers. #ITP #Coq #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2007.07571\">Computational logic for biomedicine and neurosciences<\/a>. ~ A. Bahrami, E. de Maria, J. Despeyroux, A. Felty, P. Li\u00f3. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-53518-6_18\">Tree neural networks in HOL4<\/a>. ~ Thibault Gauthier. #ITP #HOL4 #NeuralNetwork<\/li>\n<li><a href=\"https:\/\/herebeseaswines.net\/essays\/2020-the-stillness-of-haskell-code\">The stillness of Haskell code<\/a>. ~ Claes-Magnus Berg. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/odr.chalmers.se\/bitstream\/20.500.12380\/301372\/1\/CSE%2020-44%20Andersson.pdf\">A formally verified compiler for programs that deal with cached address translation<\/a>. ~ J. Andersson. #MsC_Thesis #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/github.com\/gihanmarasingha\/miu_language\">An MIU decision procedure in Lean<\/a>. ~ Gihan Marasingha. #ITP #LeanProver<\/li>\n<li><a href=\"http:\/\/kodu.ut.ee\/%7Evarmo\/tday-andu\/chapman-slides.pdf\">A biased history of equality in type theory]. (Some equations are more equal than others)<\/a>. ~ James Chapman. #TypeTheory #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2007.10842\">Who verifies the verifiers? A computer-checked implementation of the DPLL algorithm in Dafny<\/a>. ~ Cezar-Constantin Andrici, \u015etefan Ciob\u00e2c\u0103. #Dafny #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1606.08514\">Towards verified Artificial Intelligence<\/a>. ~ Sanjit A. Seshia, Dorsa Sadigh, S. Shankar Sastry. #AI #FormalVerification<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-02903548\/document\">Playing with the tower of Hanoi formally<\/a>. ~ Laurent Th\u00e9ry. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/nachivpn.me\/haski.pdf\">Towards secure IoT programming in Haskell<\/a>. ~ N. Valliappan, R. Krook, A. Russo, K. Claessen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/schooloffp.co\/2020\/07\/25\/setting-up-haskell-development-environment-the-basics.html\">Setting up Haskell development environment: The basics<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/homepage.divms.uiowa.edu\/~astump\/papers\/stump-icfp20.pdf\">Strong functional pearl: Harper\u2019s regular-expression matcher in Cedille<\/a>. ~ Aaron Stump et als. #Haskell #Cedille #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2007.09737\">Approaches to the implementation of generalized complex numbers in the Julia language<\/a>. ~ M.N. Gevorkyan, A.V. Korolkova, D.S. Kulyabov. #JuliaLang #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2007.12105v1%20\">Formalizing Nakamoto-style proof of Stake<\/a>. ~ S\u00f8ren Eller Thomsen, Bas Spitters. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Relational_Paths.html\">Relational characterisations of paths<\/a>. ~ Walter Guttmann, Peter H\u00f6fner. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-53518-6_14\">Formally verifying proofs for algebraic identities of matrices<\/a>. ~ Leonard Schmitz, Viktor Levandovskyy. #ITP<\/li>\n<li><a href=\"http:\/\/materials.dagstuhl.de\/files\/15\/15381\/15381.CatherineDubois.Slides.pdf\">Formally verified constraint solvers<\/a>. ~ Catherine Dubois, Sourour Elloumi, Arnaud Gotlieb. #ITP #Coq #CSP<\/li>\n<li><a href=\"http:\/\/tonyday567.github.io\/posts\/learning\/\">Machine learning in Haskell<\/a>. ~ @tonyday567 #Haskell #FunctionalProgramming #MachineLearning<\/li>\n<li><a href=\"http:\/\/www.haskellforall.com\/2020\/07\/the-golden-rule-of-software-quality.html\">The golden rule of software quality<\/a>. ~ G. Gonzalez (@GabrielG439). #Programming #Haskell<\/li>\n<li><a href=\"https:\/\/spel.org.pe\/dia-logica-2021\/\">D\u00eda Mundial de la L\u00f3gica 2021<\/a>. #L\u00f3gica<\/li>\n<li><a href=\"https:\/\/repositorio.inesctec.pt\/bitstream\/123456789\/11436\/1\/P-00S-6ZF.pdf\">Expressing disambiguation filters as combinators<\/a>. ~ Jos\u00e9 Nuno Macedo, Jo\u00e3o Saraiva. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/oa.upm.es\/63139\/1\/TFG_DAVID_MUNUERA_MAZARRO.pdf\">An\u00e1lisis de coste en programas funcionales Usando CiaoPP<\/a>. ~ David Munuera Mazarro. #TFG #Haskell #Prolog #Algor\u00edtmica<\/li>\n<li><a href=\"https:\/\/dev.to\/tfausak\/golfing-language-extensions-2obl\">Golfing language extensions<\/a>. ~ Taylor Fausak (@taylorfausak). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/CxS0ONDfWJg\">Metamath Zero: Designing a theorem prover prover<\/a>. ~ #ITP<\/li>\n<li><a href=\"https:\/\/youtu.be\/5HDlgsjO8-w\">Maintaining a library of formal Mathematics<\/a>. ~ Gabriel Ebner. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2007.13529\">Automated verification of reactive and concurrent programs by calculation<\/a>. ~ Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock. #ITP #Isabelle<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-02907622\/document\">Certifying a rule-based model transformation engine for proof preservation<\/a>. ~ Z. Cheng, M. Tisi, J. Hotonnier. #ITP #Coq<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante julio 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\/7215"}],"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=7215"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7215\/revisions"}],"predecessor-version":[{"id":7216,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7215\/revisions\/7216"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7215"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7215"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7215"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}