{"id":7601,"date":"2021-04-01T19:26:05","date_gmt":"2021-04-01T17:26:05","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7601"},"modified":"2021-08-30T19:27:05","modified_gmt":"2021-08-30T17:27:05","slug":"resumen-de-lecturas-compartidas-durante-marzo-de-2021","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-marzo-de-2021\/","title":{"rendered":"Resumen de lecturas compartidas durante marzo de 2021"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante marzo 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=\"http:\/\/www.andreas-lochbihler.de\/pub\/basin2021.pdf\">Abstract modeling of systems communication in constructive cryptography using CryptHOL<\/a>. ~ D. Basin, A. Lochbihler, U. Maurer, S.R. Sefidgar. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.ncbi.nlm.nih.gov\/pmc\/articles\/PMC7984526\/pdf\/978-3-030-72019-3_Chapter_5.pdf\">Verified software units<\/a>. ~ Lennart Beringer. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/ekmett\/linear-logic\">linear-logic: a version of intuitionistic linear logic on top of linear Haskell<\/a>. ~ Edward Kmett. #Haskell #FunctionalProgramming #Logic<\/li>\n<li><a href=\"https:\/\/www.ncbi.nlm.nih.gov\/pmc\/articles\/PMC7984547\/pdf\/978-3-030-72019-3_Chapter_10.pdf\/?tool=EBI\">Do judge a test by its cover: Combining combinatorial and property-based testing<\/a>. ~ Harrison Goldstein, John Hughes, Leonidas Lampropoulos, Benjamin C. Pierce. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.ams.org\/\/journals\/bull\/0000-000-00\/S0273-0979-2021-01726-5\/S0273-0979-2021-01726-5.pdf\">Varieties of mathematical understanding<\/a>. ~ Jeremy Avigad. #ITP #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2103.13534v1\">A formal proof of the Lax equivalence theorem for finite difference schemes<\/a>. ~ Mohit Tekriwal, Karthik Duraisamy, Jean-Baptiste Jeannin. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-03176024\">Verifying min-plus Computations with Coq (extended version with appendix)<\/a>. ~ Lucien Rakotomalala, Pierre Roux, Marc Boyer. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.ncbi.nlm.nih.gov\/pmc\/articles\/PMC7984530\/\">For a few dollars more: Verified fine-grained algorithm analysis down to LLVM<\/a>. ~ Maximilian P.L. Haslbeck, Peter Lammich. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.ncbi.nlm.nih.gov\/pmc\/articles\/PMC7984549\/\">Certifying proofs in the first-order theory of rewriting<\/a>. ~ Fabian Mitterwallner, Alexander Lochmann, Aart Middeldorp, Bertram Felgenhauer. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2103.15702\">Limits of real numbers in the binary signed digit representation<\/a>. ~ Franziskus Wiesnet, Nils K\u00f6pp. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/www.microsiervos.com\/archivo\/matematicas\/analisis-complejo-mandelbrot-julia-codigo-abierto.html\">El An\u00e1lisis complejo y una exploraci\u00f3n de los conjuntos de Mandelbrot y Julia con c\u00f3digo abierto<\/a>. ~ @Alvy. #Matem\u00e1ticas #Programaci\u00f3n<\/li>\n<li><a href=\"https:\/\/complex-analysis.com\/es.html\">An\u00e1lisis complejo (Una introducci\u00f3n visual e interactiva)<\/a>. ~ Juan Carlos Ponce Campuzano. #eBook #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/novo.manzano.pro.br\/wp\/download\/logica-de-programacao-funcional-pense-em-hope\/\">L\u00f3gica de programa\u00e7\u00e3o funcional: Pense em Hope (Exerc\u00edcios de programa\u00e7\u00e3o funcional com Hope)<\/a>. ~ Jos\u00e9 Augusto N. G. Manzano, Jos\u00e9 A. Alonso Jim\u00e9nez, Mar\u00eda J. Hidalgo Doblado. #eBook #Hope #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/perl.plover.com\/yak\/typing\/notes.html\">Strong typing<\/a>. ~ M-J. Dominus (1999). #Programming<\/li>\n<li><a href=\"https:\/\/www.cse.chalmers.se\/~rjmh\/Papers\/whyfp.pdf\">Why functional programming matters<\/a>. ~ John Hughes. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.ams.org\/journals\/notices\/202104\/rnoti-p565.pdf\">The dawning of a new era in applied mathematics<\/a>. ~ Weinan E. #Math via @emulenews<\/li>\n<li><a href=\"https:\/\/www.lavanguardia.com\/ciencia\/20210329\/6607152\/inteligencia-artificial-nunca-sera-humana.html\">La inteligencia artificial nunca ser\u00e1 como la humana<\/a>. ~ Ram\u00f3n L\u00f3pez de M\u00e1ntaras. #IA<\/li>\n<li><a href=\"https:\/\/github.com\/AbstProcDo\/Master-Emacs-From-Scratch-with-Solid-Procedures\/blob\/master\/01.semantic-keybinding-en.org\">EmacsTutorial01: Semantic keybindings to memorize hundreds of keys instantly<\/a>. #Emacs<\/li>\n<li><a href=\"https:\/\/eprint.iacr.org\/2021\/397\">SSProve: A foundational framework for modular cryptographic proofs in Coq<\/a>. ~ C. Abate, P.G. Haselwarter, E. Rivas, A. Van Muylder, T. Winterhalter, C. Hritcu, K. Maillard, B. Spitters. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/webspace.science.uu.nl\/~swier004\/publications\/2021-jfp-submission.pdf\">A well-known representation of monoids and its application to the function &#8220;vector reverse&#8221;<\/a>. ~ Wouter Swierstra. #Agda #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2103.11751v1\">Functional Pearl: Witness me &#8211; Constructive arguments must be guided with concrete witness<\/a>. ~ Hiromi Ishii. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/luctielen.com\/posts\/combining_folds_using_semigroups\/\">Combining folds using semigroups<\/a>. ~ Luc Tielen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/kowainik.github.io\/posts\/internal-functions\">Many faces of internal functions<\/a>. ~ Veronika Romashkina. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/plv.csail.mit.edu\/blog\/alectryon.html\">Alectryon: a collection of tools for writing technical documents that mix Coq code and prose<\/a>. ~ Cl\u00e9ment Pit-Claudel. #ITP #Coq via @jjcarett2<\/li>\n<li><a href=\"https:\/\/www.ereslibre.es\/blog\/2019\/09\/building-a-personal-website-with-org-mode.html\">Building a personal website with org-mode<\/a>. ~ Rafael Fern\u00e1ndez. #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/emacs.love\/weblorg\/\">Weblorg: A static HTML generator for Emacs and Org-Mode<\/a>. #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/lexi-lambda.github.io\/blog\/2021\/03\/25\/an-introduction-to-typeclass-metaprogramming\/\">An introduction to typeclass metaprogramming<\/a>. ~ Alexis King. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/blog\/2021-03-25-haskell-java\/\">How to build hybrid Haskell and Java programs<\/a>. ~ Facundo Dom\u00ednguez, Andreas Hermann. #Haskell #Java<\/li>\n<li><a href=\"https:\/\/courses.cs.washington.edu\/courses\/cse505\/17au\/\">Course: Programming languages<\/a>. ~ Zach Tatlock, Leonardo De Moura. #CompSci #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/docs.google.com\/document\/d\/1V22TC-vf6b7ciBquR5-IK3wJ1WCPhrBLWIP1Tf18z0Y\/edit#\">Coq fundamentals<\/a>. ~ Zach Tatlock. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.tomhoule.com\/leaning-into-calculus-chapter-1\/\">Leaning into Spivak&#8217;s calculus<\/a>. ~ Tom Houle. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/openreview.net\/pdf\/c9fb7dd359102a00d8676684bd704c54961a5285.pdf\">IsarStep: A benchmark for high-level mathematical reasoning<\/a>. ~ W. Li, L. Yu, Y. Wu, L.C. Paulson. #ITP #IsabelleHOL #Math #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2103.11389\">Formal verification of Zagier&#8217;s one-sentence proof<\/a>. ~ Guillaume Dubach, Fabian Muehlboeck. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.snoyman.com\/blog\/2021\/03\/programmer-learning-list\/\">Programmer learning list<\/a>. ~ Michael Snoyman. #Programming<\/li>\n<li><a href=\"https:\/\/github.com\/tomjaguarpaw\/tilapia\/blob\/master\/Windows10.md\">Install GHC, Cabal and Haskell Language Server IDE on Windows 10<\/a>. ~ Will Gould. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/readerunner.wordpress.com\/2021\/03\/20\/diagrams-for-penrose-tiles\/\">Diagrams for Penrose tiles<\/a>. ~ Chris Reade. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2103.08535v1\">Quantum projective measurements and the CHSH inequality in Isabelle\/HOL<\/a>. ~ Mnacho Echenim, Mehdi Mhalla. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2103.07543v1\">Reasoning about the garden of forking paths<\/a>. ~ Yao Li, Li-yao Xia, Stephanie Weirich. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-03168208\/document\">Plotting in a formally verified way<\/a>. ~ Guillaume Melquiond. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2103.06913v1\">Classical (co)recursion: Programming<\/a>. ~ Paul Downen, Zena M. Ariola. #Agda #Scheme #Python #Java<\/li>\n<li><a href=\"http:\/\/web.wakayama-u.ac.jp\/~sakama\/slide\/aspocp2018-slide.pdf\">Partial evaluation of logic programs in vector spaces<\/a>. ~ Chiaki Sakama, Hien D. Nguyen, Taisuke Sato, Katsumi Inoue. #LogicProgramming #Math<\/li>\n<li><a href=\"https:\/\/www21.in.tum.de\/~haslbema\/documents\/haslbeck2021thesis.pdf\">Verified quantitative analysis of imperative algorithms<\/a>. ~ Maximilian P.L. Haslbeck. #PhDThesis #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Constructive_Cryptography_CM.html\">Constructive cryptography in HOL: the communication modeling aspect<\/a>. ~ Andreas Lochbihler, S. Reza Sefidgar. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.cs.helsinki.fi\/u\/jllang\/Introduction_to_Lambda_Calculus.pdf\">Introduction to lambda calculus<\/a>. ~ John L\u00e5ng. #LambdaCalculus #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/avi-wigderson-and-laszlo-lovasz-win-abel-prize-20210317\/\">Pioneers linking Math and Computer Science win the Abel Prize<\/a>. ~ Kevin Hartnett. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/plus.maths.org\/content\/laszlo-lovasz-working-mathematical-miracles\">L\u00e1szl\u00f3 Lov\u00e1sz: Working mathematical miracles<\/a>. ~ Marianne Freiberger. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/plus.maths.org\/content\/its-good-have-hard-problems\">Avi Wigderson: &#8220;It&#8217;s good to have hard problems&#8221;<\/a>. ~ Rachel Thomas. #Math #CompSci<\/li>\n<li><a href=\"http:\/\/www.cs.toronto.edu\/~ledt\/papers\/Avi\/L2.pdf\">Cryptography and pseudorandomness<\/a>. ~ Avi Wigderson. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/www.math.ias.edu\/avi\/book\">Mathematics and computation (A theory revolutionizing technology and science)<\/a>. ~ Avi Wigderson. #eBook #Math #CompSci via @mbelcrypt_vasco<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2103.09092\">The Agda universal algebra library, Part 2: Structure<\/a>. ~ William DeMeo. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/5e7UdWzITyQ\">Formal methods for the informal engineer (Tutorial 2: The Coq theorem prover)<\/a>. ~ Cody Roux. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/gilmi.me\/blog\/post\/2021\/03\/16\/bottom-haskell-pyramid\">The bottom of the Haskell Pyramid<\/a>. ~ Gil Mizrahi. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.math.wustl.edu\/~sk\/eolss.pdf\">The history and concept of mathematical proof<\/a>. ~ Steven G. Krantz. #Logic #Math via @mathematicsprof<\/li>\n<li><a href=\"https:\/\/ingenieriadesoftware.es\/historia-visual-lenguajes-programacion\/\">Historia visual de los lenguajes de programaci\u00f3n<\/a>. ~ Jordi Cabot. #Programaci\u00f3n v\u00eda @fernand0<\/li>\n<li><a href=\"https:\/\/ps.uni-saarland.de\/Publications\/documents\/KirstHermes_2021_Synthetic.pdf\">Synthetic undecidability and incompleteness of first-order axiom systems in Coq<\/a>. ~ Dominik Kirst, Marc Hermes. #ITP #Coq #Logic #Math<\/li>\n<li><a href=\"https:\/\/webspace.science.uu.nl\/~swier004\/publications\/2020-jfp.pdf\">Functional Pearls: Heterogeneous binary random-access lists<\/a>. ~ Wouter Swierstra. #Agda #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/kowainik.github.io\/images\/Haskell_Knowledge_Map.png\">Haskell knowledge map<\/a>. ~ Veronika Romashkina, Dmitrii Kovanikov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.ch3m4.org\/2021\/03\/07\/evaluacion-perezosa-en-python-parte-5\/\">Evaluaci\u00f3n perezosa en Python. Parte 5: Formalizaci\u00f3n de la secuencia perezosa<\/a>. ~ Chema Cort\u00e9s. #Python #Programaci\u00f3n<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2021\/03\/15\/formalising-mathematics-workshop-8-group-cohomology\/\">Formalising mathematics: workshop 8 (group cohomology)<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Modular_arithmetic_LLL_and_HNF_algorithms.html\">Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation (in Isabelle\/HOL)<\/a>. ~ Ralph Bottesch, Jose Divason, Rene Thiemann. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2021-03-14-hyperfunctions.html\">Hyperfunctions<\/a>. ~ Donnacha Ois\u00edn Kidney. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.wikiwand.com\/en\/List_of_formulae_involving_%CF%80\">List of formulae involving \u03c0<\/a>. #Math via @mathematicsprof<\/li>\n<li><a href=\"https:\/\/ubikium.gitlab.io\/portfolio\/2021-03-13-wait-a-moment.html\">(((Wait a moment .) .) .) &#8211; Composing functions with multiple arguments<\/a>. ~ Philip K. Dick. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/magnus.therning.org\/posts\/2021-03-05-000-flycheck-and-hls.html\">Flycheck and HLS<\/a>. ~ Magnus Therning. #Emacs #LSPmode #Haskell #HLS via @jneira<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Hermite_Lindemann.html\">The Hermite\u2013Lindemann\u2013Weierstra\u00df transcendence theorem (in Isabelle\/HOL)<\/a>. ~ Manuel Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/matt.might.net\/articles\/partial-orders\/\">Order theory for computer scientists<\/a>. ~ Matt Might. #Math #CompSci #Haskell #FunctionalProgramming via @CompSciFact<\/li>\n<li><a href=\"https:\/\/www.newyorker.com\/culture\/culture-desk\/what-is-mathematics\">What is mathematics?<\/a> ~ Alec Wilkinson. #Math<\/li>\n<li><a href=\"https:\/\/infinitedescent.xyz\/\">An infinite descent into pure mathematics<\/a>. ~ Clive Newstead. #eBook #Math<\/li>\n<li><a href=\"http:\/\/eugeniacheng.com\/wp-content\/uploads\/2017\/02\/cheng-proofguide.pdf\">How to write proofs: a quick guide<\/a>. ~ Eugenia Cheng. #Logic #Math<\/li>\n<li><a href=\"https:\/\/notxor.nueva-actitud.org\/2021\/03\/11\/emacs-y-lsp-mode.html\">Emacs y lsp-mode<\/a>. #Emacs #LSPmode<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2103.05581\">The Agda universal algebra library &#8211; Part 1: Foundation (Equality, extensionality, truncation, and dependent types for relations and algebras)<\/a>. ~ William DeMeo. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/link.springer.com\/article\/10.1007\/s00283-020-10037-7\">A replication crisis in mathematics?<\/a> ~ Anthony Bordg. #Math #ITP<\/li>\n<li><a href=\"http:\/\/www.divulgamat.net\/index.php?option=com_content&amp;view=article&amp;id=18\">Contrastando dos c\u00f3dices matem\u00e1ticos iluminados<\/a>. ~ \u00c1ngel Requena Fraile. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/github.com\/jespercockx\/agda-lecture-notes\/blob\/master\/agda.pdf\">Programming and proving in Agda<\/a>. ~ Jesper Cockx. #ITP #Agda #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2103.04519\">Formal verification of authenticated, append-only skip lists in Agda: Extended version<\/a>. ~ Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, Guy L. Steele Jr. #ITP #Agda<\/li>\n<li><a href=\"http:\/\/conal.net\/papers\/language-derivatives\/paper.pdf\">Symbolic and automatic differentiation of languages<\/a>. ~ Conal Elliott. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Projective_Measurements.html\">Quantum projective measurements and the CHSH inequality (in Isabelle\/HOL)<\/a>. ~ Mnacho Echenim. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/b25994d522d1368e19a6e568aa7e642d72a95294\/src\/number_theory\/bernoulli_polynomials.lean\">Bernoulli polynomials (in Lean prover)<\/a>. ~ Ashvni Narayanan. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/dfithian.github.io\/2021\/03\/08\/pruning-unused-haskell-dependencies.html\">Pruning unused Haskell dependencies<\/a>. ~ Dan Fithian. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2103.03930\">Logical foundations: Personal perspective<\/a>. ~ Yuri Gurevich. #Logic #Math #CompSci<\/li>\n<li><a href=\"http:\/\/math.fau.edu\/yiu\/RecreationalMathematics2003.pdf\">Recreational Mathematics<\/a>. ~ Paul Yiu. #eBook #Math<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/blogs\/blog-cacm\/203554-five-principles-for-programming-languages-for-learners\">Five principles for programming languages for learners<\/a>. ~ Mark Guzdial. #CompSci #Teaching #Programming<\/li>\n<li><a href=\"https:\/\/blog.jpolak.org\/?p=2358\">Fifteen awesome cross-platform math apps<\/a>. ~ Jason Polak. #Math #CompSci #Programming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2103.03607\">Formalizing graph trail properties in Isabelle\/HOL<\/a>. ~ Laura Kovacs, Hanna Lachnitt, Stefan Szeider. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2103.03798\">Training a first-order theorem prover from synthetic data<\/a>. ~ Vlad Firoiu, Eser Aygun, Ankit Anand, Zafarali Ahmed, Xavier Glorot, Laurent Orseau, Lei Zhang, Doina Precup, Shibl Mourad. #ATP #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2103.03874\">Measuring mathematical problem solving with the MATH dataset<\/a>. ~ Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, Jacob Steinhardt. #MachineLearning #ITP #Math<\/li>\n<li><a href=\"https:\/\/users-cs.au.dk\/birke\/papers\/free-theorems-sep-logic.pdf%20\">Theorems for free from separation logic specifications<\/a>. ~ Lars Birkedal et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Mereology.html\">Mereology (in Isabelle\/HOL)<\/a>. ~ Ben Blumson. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/wiki.tfpie.science.ru.nl\/images\/a\/a6\/TFPIE_AHF_JV.pdf\">Teaching automated reasoning and formally verified functional programming in Agda and Isabelle\/HOL<\/a>. ~ Asta Halkj\u00e6r From, J\u00f8rgen Villadsen. #Logic #FunctionalProgramming #ITP #Agda #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.scitepress.org\/Papers\/2020\/98936\/98936.pdf\">Formalization and verification of reconfigurable discrete-event system using model driven engineering and Isabelle\/HOL<\/a>. ~ S. Soualah, Y. Hafidi, M. Khalgui, A. Chaoui, L. Kahloul. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2103.00223\">Generalized universe hierarchies and first-class universe levels<\/a>. ~ Andr\u00e1s Kov\u00e1cs. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2103.01346\">Roosterize: Suggesting lemma names for Coq verification projects using deep learning<\/a>. ~ Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric. #ITP #Coq #DeepLearning<\/li>\n<li><a href=\"https:\/\/youtu.be\/EXpmbAfBNnw\">Neural theorem proving in Lean using Proof Artifact Co-training and language models<\/a>. ~ Jason Rute. #ITP #LeanProver #MachineLearning<\/li>\n<li><a href=\"https:\/\/cmsa.fas.harvard.edu\/wp-content\/uploads\/2021\/03\/LeanStep-Talk-New-Technology-in-Mathematics-Seminar.pdf\">Neural theorem proving in Lean using Proof Artifact Co-training and language models<\/a>. [Slides] ~ Jason Rute. #ITP #LeanProver #MachineLearning<\/li>\n<li><a href=\"https:\/\/github.com\/atarnoam\/lean-automata\">Proving theorems about regular languages and DFAs in Lean<\/a>. ~ Noam Atar. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/5962c76fb636d17a041726adcc11299c8a23e2b6\/src\/algebra\/ring\/boolean_ring.lean\">Boolean rings (in Lean prover)<\/a>. ~ Bryan Gin-ge Chen. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/hgeometry.org\/\">HGeometry: Computational Geometry in Haskell<\/a>. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2021\/03\/04\/formalising-mathematics-workshop-7-quotients\/\">Formalising mathematics: workshop 7 (quotients)<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/functional.works-hub.com\/learn\/tutorial-cellular-automata-and-comonads-fc3a6\">Tutorial: Cellular automata and comonads<\/a>. ~ Siddharth Bhat. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.popularmechanics.com\/science\/math\/g29008356\/hard-math-problems\/\">These are the 10 toughest math problems ever solved<\/a>. ~ Dave Linkletter. #Math<\/li>\n<li><a href=\"https:\/\/www.lemonde.fr\/blog\/binaire\/2021\/03\/05\/linformatique-quelques-questions-pour-se-facher-entre-amis\/\">L\u2019informatique, quelques questions pour se f\u00e2cher entre amis<\/a>. ~ Serge Abiteboul, Inria Paris, Gilles Dowek. #CompSci<\/li>\n<li><a href=\"https:\/\/www.cs.rice.edu\/~vardi\/comp409\/history.pdf\">A brief history of Logic<\/a>. ~ Moshe Y. Vardi (2003). #Logic #Math #CompSci via @prathyvsh<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2103.02102\">Experimental mathematics approach to Gauss diagrams realizability<\/a>. ~ A. Khan, A. Lisitsa, A. Vernitski. #Prolog #LogicProgramming #Math<\/li>\n<li><a href=\"https:\/\/blog.plover.com\/math\/topology-doc.html\">Short introduction to Topology (for Computer Science grad students)<\/a>. ~ Mark Jason Dominus (2010). #Math via @CompSciFact<\/li>\n<li><a href=\"https:\/\/jcodev.eu\/posts\/using-nix-for-haskell-development-in-emacs-with-lsp\/\">Using Nix for Haskell development in Emacs with LSP<\/a>. ~ Jonas Collberg. #Haskell #Emacs<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/348829872_Towards_a_Notion_of_Basis_for_Knowledge-Based_Systems_-_Applications\">Towards a notion of basis for knowledge-based systems &#8211; Applications<\/a>. ~ Gonzalo A. Aranda, Joaqu\u00edn Borrego, Juan Gal\u00e1n, Daniel Rodr\u00edguez. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/youtu.be\/UnYrWuOzOlc\">AI and Theorem Proving [Video<\/a>]. ~ Josef Urban. #ATP #ITP #MachineLearning #AI<\/li>\n<li><a href=\"https:\/\/cmsa.fas.harvard.edu\/wp-content\/uploads\/2021\/01\/Urbanslides.pdf\">AI and Theorem Proving [Slides<\/a>]. ~ Josef Urban. #ATP #ITP #MachineLearning #AI<\/li>\n<li><a href=\"https:\/\/youtu.be\/Y0hpHm74FYs\">Language modeling for mathematical reasoning [Video<\/a>]. ~ Christian Szegedy. #Logic #Math #AI<\/li>\n<li><a href=\"https:\/\/cmsa.fas.harvard.edu\/wp-content\/uploads\/2021\/01\/Language-modeling-for-Mathematical-Reasoning-.pdf%20\">Language modeling for mathematical reasoning [Slides<\/a>]. ~ Christian Szegedy. #Logic #Math #AI<\/li>\n<li><a href=\"https:\/\/kowainik.github.io\/posts\/arrows-zoo\">Arrows Zoo<\/a>. ~ Veronika Romashkina, Dmitrii Kovanikov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.cs.utexas.edu\/users\/EWD\/transcriptions\/EWD10xx\/EWD1011.html\">Introducing my fall 1987 course on Mathematical Methodology<\/a>. ~ Edsger W.Dijkstra. #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Sunflowers.html\">The sunflower lemma of Erd\u0151s and Rado (in Isabelle\/HOL)<\/a>. ~ Ren\u00e9 Thiemann. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.303.8201&amp;rep=rep1&amp;type=pdf\">12\u00b2 beautiful mathematical theorems with short proofs<\/a>. ~ Jo\u0308rg Neunha\u0308userer. #Math via @@lizardbill<\/li>\n<li><a href=\"http:\/\/www.cut-the-knot.org\/proofs\/index.shtml\">Proofs in Mathematics<\/a>. ~ Alexander Bogomolny. #Math<\/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 marzo 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\/7601"}],"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=7601"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7601\/revisions"}],"predecessor-version":[{"id":7602,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7601\/revisions\/7602"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7601"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7601"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7601"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}