{"id":7217,"date":"2020-02-01T18:33:58","date_gmt":"2020-02-01T17:33:58","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7217"},"modified":"2020-08-01T18:35:23","modified_gmt":"2020-08-01T16:35:23","slug":"resumen-de-lecturas-compartidas-durante-enero-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-enero-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas durante enero de 2020"},"content":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante enero 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=\"http:\/\/www.eds.yildiz.edu.tr\/AjaxTool\/GetArticleByPublishedArticleId?PublishedArticleId=3936\">Introduction to HOL4 theorem prover<\/a>. ~ K. Aksoy, S. Tahar, Y. Zeren. #ITP #HOL4<\/li>\n<li><a href=\"https:\/\/t.co\/8IZttMkU33\">Design and verification of parity checking circuit using HOL4 theorem proving<\/a>. ~ E. Deni\u0307z, K. Aksoy, S. Tahar, Y. Zeren. #ITP #HOL4<\/li>\n<li><a href=\"http:\/\/save.seecs.nust.edu.pk\/pubs\/2020\/SAC_2020_1.pdf\">Proof searching in HOL4 with genetic algorithm<\/a>. ~ M.Z. Nawaz et als #ITP #HOL4<\/li>\n<li><a href=\"https:\/\/blog.sigplan.org\/2019\/12\/30\/defunctionalization-everybody-does-it-nobody-talks-about-it\/\">Defunctionalization: Everybody does it, nobody talks about it<\/a>. ~ James Koppel. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1804.05495\">Constructive reverse mathematics<\/a>. ~ Hannes Diener. #Logic #Math<\/li>\n<li><a href=\"https:\/\/tqft.net\/web\/research\/students\/YimingXu\/thesis.pdf\">Formalizing modal logic in HOL<\/a>. ~ Yiming Xu. #PhD_Thesis #ITP #HOL #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1909.07479\">On correctness of an n queens program<\/a>. ~ W\u0142odzimierz Drabent. #LogicProgramming #Prolog #Verification<\/li>\n<li><a href=\"https:\/\/www.simplehaskell.org\/\">The simple Haskell initiative<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/news\/241912-a-computer-made-from-dna-can-compute-the-square-root-of-900\/fulltext\">A computer made from DNA can compute the square root of 900<\/a>. #CompSci<\/li>\n<li><a href=\"https:\/\/her.esy.fun\/posts\/0010-Haskell-Now\/index.html\">Learn Haskell now!<\/a> ~ Yann Esposito (@yogsototh). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/artagnon.com\/articles\/leancoq#main\">Lean versus Coq: The cultural chasm<\/a>. ~ Ramkumar Ramachandra. #ITP #LeanProver #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/gelisam\/typelevel-rewrite-rules\">Type-level rewrite rules<\/a>. ~ Samuel G\u00e9lineau. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/jaspervdj.be\/posts\/2020-01-04-mandelbrot-lovejoy-rain.html\">Mandelbrot &amp; Lovejoy&#8217;s rain fractals<\/a>. ~ Jasper Van der Jeugt (@jaspervdj). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371121?download=true\">Kind inference for datatypes<\/a>. ~ N. Xie, R.A. Eisenberg, B.C.d.S. Oliveira. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2020\/1\/6\/organizing-our-package\">Organizing our package!<\/a> ~ James Bowen (@james_OWA). #Haskell #Cabal #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-septiembre-de-2019\/\">Resumen de lecturas compartidas durante septiembre de 2019<\/a>. #FunctionalProgramming #Haskell #ITP #IsabelleHOL #Coq #Agda<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-octubre-de-2019\/\">Resumen de lecturas compartidas durante octubre de 2019<\/a>. #FunctionalProgramming #Haskell #ITP #IsabelleHOL #Coq #Agda<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-noviembre-de-2019\/\">Resumen de lecturas compartidas durante noviembre de 2019<\/a>. #FunctionalProgramming #Haskell #ITP #IsabelleHOL #Coq #Agda<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-diciembre-de-2019\/\">Resumen de lecturas compartidas durante diciembre de 2019<\/a>. #FunctionalProgramming #Haskell #ITP #IsabelleHOL #Coq #Agda<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Hybrid_Logic.html\">Formalizing a Seligman-style tableau system for hybrid logic in Isabelle\/HOL<\/a>. ~ Asta Halkj\u00e6r. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"http:\/\/www.ams.org\/journals\/notices\/202001\/rnoti-p77.pdf\">Different problems, common threads: Computing the difficulty of mathematical problems<\/a>. ~ Karen Lange. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/www.johndcook.com\/blog\/2020\/01\/06\/smooth-numbers\/\">Estimating the proportion of smooth numbers<\/a>. ~ John D. Cook (@JohnDCook). #Math #Programming #Python<\/li>\n<li><a href=\"https:\/\/agentultra.github.io\/lean-for-hackers\/\">Lean 3 for hackers<\/a>. ~ J Kenneth King. #LeanProver #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/gist.github.com\/mightybyte\/6c469c125eb50e0c2ebf4ae26b5adfff\">Haskell language extension taxonomy<\/a>. ~ Doug Beardsley. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1912.06611\">A formal proof of the irrationality of \u03b6(3)<\/a>. ~ Assia Mahboubi, Thomas Sibut-Pinote. #ITP #Coq #Math<\/li>\n<li><a href=\"http:\/\/www21.in.tum.de\/~nipkow\/pubs\/cpp20.pdf\">Proof pearl: Braun trees<\/a>. ~ T. Nipkow, T. Sewell. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Gauss_Sums.html\">Gauss sums and the P\u00f3lya\u2013Vinogradov inequality<\/a>. ~ R. Raya, M. Eberl. #ITP #IsabellleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Bicategory.html\">Bicategories in Isabelle\/HO: ~ Eugene W<\/a>. Stark. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Zeta_3_Irrational.html\">The irrationality of \u03b6(3) in Isabelle\/HOL<\/a>. ~ Manuel Eberl. #ITP #IsabellleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Skip_Lists.html\">Skip lists in Isabelle\/HOL<\/a>. ~ M.W. Haslbeck, M. Eberl. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.02657\">Motivated proofs: what they are, why they matter and how to write them<\/a>. ~ Rebecca Lea Morris. #Math<\/li>\n<li><a href=\"https:\/\/www.logicmatters.net\/2020\/01\/09\/programming-with-categories\/\">Programming with categories<\/a>. ~ Peter Smith. #Programming #CategoryTheory<\/li>\n<li><a href=\"https:\/\/dixonary.co.uk\/blog\/haskell\/small\">Generating small binaries in Haskell<\/a>. ~ Alex Dixon (@dixonary_). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/saurabhkukade\/Haskell_Study\">Collections of papers and books about Haskell, type theory and category theory<\/a>. ~ Saurabh Kukade. #Haskell #TypeTheory #CategoryTheory<\/li>\n<li><a href=\"https:\/\/jfr.unibo.it\/article\/view\/9757\">LF+ in Coq for &#8220;fast and loose&#8221; reasoning<\/a>. ~ F. Alessi. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/bolt12\/master-thesis\">Selective applicative functors &amp; probabilities<\/a>. ~ Armando Santos (@_bolt12). #MSc_Thesis #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/github.com\/bolt12\/laop\">Linear algebra of programming &#8211; Algebraic matrices in Haskell<\/a>. ~ Armando Santos (@_bolt12). #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/cswithbaddrawings.wordpress.com\/2020\/01\/10\/gain-confidence-with-haskell\/\">Gain confidence with Haskell!<\/a> ~ Brandon Chinn. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/lisp-univ-etc.blogspot.com\/2020\/01\/programming-algorithms-approximation.html\">Programming algorithms: approximation<\/a>. ~ Vsevolod Dyomkin. #CommonLisp #Algorithms<\/li>\n<li><a href=\"https:\/\/williamyaoh.com\/posts\/2020-01-11-road-to-proficient.html\">The road to proficient Haskell<\/a>. ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.logicmatters.net\/wp-content\/uploads\/2019\/12\/TeachYourselfLogic2020.pdf\">Teach yourself Logic 2020: A study guide<\/a>. ~ Peter Smith. #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/salmans\/rusty-razor\">Rusty Razor is a tool for constructing finite models for first-order theories<\/a>. ~ Salman Saghafi. #Logic<\/li>\n<li><a href=\"https:\/\/digitalcommons.wpi.edu\/cgi\/viewcontent.cgi?article=1457&amp;context=etd-dissertations\">A framework for exploring finite models<\/a>. ~ Salman Saghafi. #PhD_Thesis #Logic #Haskell<\/li>\n<li><a href=\"http:\/\/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 #WorldLogicDay<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1802.03292\">Mathematical Logic in Computer Science<\/a>. ~ Assaf Kfoury. #Logic #CompSci #WorldLogicDay<\/li>\n<li><a href=\"https:\/\/www.cs.upc.edu\/~roberto\/EffectivenessOfLogic.pdf\">On the unusual effectiveness of Logic in Computer Science<\/a>. ~ J.Y. Halpern et als. #Logic #CompSci #WorldLogicDay<\/li>\n<li><a href=\"http:\/\/www.ru.is\/faculty\/luca\/SLIDES\/logic-and-cs.pdf\">Computer Science and Logic (a match made in heaven)<\/a>. ~ Luca Aceto. #Logic #CompSci #WorldLogicDay<\/li>\n<li><a href=\"http:\/\/www.cs.cornell.edu\/courses\/cs4860\/2019fa\/lectures\/L2-A-Story-of-Logic.pdf\">The story of Logic<\/a>. ~ Robert L. Constable. #Logic #CompSci #WorldLogicDay<\/li>\n<li><a href=\"http:\/\/www.cl.cam.ac.uk\/~jrh13\/papers\/joerg.pdf\">History of interactive theorem <\/a>.proving. ~ J. Harrison, J. Urban, F. Wiedijk. #ITP #Logic #CompSci #WorldLogicDay<\/li>\n<li><a href=\"https:\/\/www.cadeinc.org\/Data\/HerbrandAwardSlidesConstable.pdf\">Automated reasoning: From bold dreams to Computer Science methodology<\/a>. ~ Robert L. Constable. #ATP #CompSci #WorldLogicDay<\/li>\n<li><a href=\"https:\/\/www.cs.ru.nl\/~herman\/ictopen.pdf\">Can the computer really help us to prove theorems? ~ Herman Geuvers<\/a>. #ITP #Logic #CompSci #WorldLogicDay<\/li>\n<li><a href=\"https:\/\/www.taut-logic.com\/index.html\">TAUT: A website that contains randomly-generated, self-correcting logic excercises<\/a>. ~ Ariel Roff\u00e9. #Logic<\/li>\n<li><a href=\"https:\/\/www.conicet.gov.ar\/taut-el-software-desarrollado-por-un-filosofo-del-conicet-para-ensenar-logica\/\">TAUT: el software desarrollado por un fil\u00f3sofo del CONICET para ense\u00f1ar L\u00f3gica<\/a>. #L\u00f3gica #WorldLogicDay<\/li>\n<li><a href=\"http:\/\/dailynous.com\/2018\/11\/20\/randomly-generated-self-correcting-logic-exercises-site\/\">Randomly generated and self-correcting logic exercises site<\/a>. ~ Justin Weinberg. #Logic #WorldLogicDay<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/foldl-adjunction.html\">Adjunctions in the wild: foldl<\/a>. ~ Justin Le (@mstk). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1910.12863\">Computer-supported exploration of a categorical axiomatization of modeloids<\/a>. ~ L. Tiemens, D.S. Scott, C. Benzm\u00fcller, M. Benda. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1910.08955\">Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of G\u00f6del&#8217;s ontological argument<\/a>. ~ C. Benzm\u00fcller, D. Fuenmayor. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.04457\">A verified packrat parser interpreter for parsing expression grammars<\/a>. ~ C. Blaudeau, N. Shankar. #ITP #PVS<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2020\/1\/13\/using-cabal-on-its-own\">Using Cabal on its own<\/a>. ~ James Bowen (@james_OWA). #Haskell #Cabal<\/li>\n<li><a href=\"https:\/\/vrom911.github.io\/blog\/common-stanzas\">Common stanzas<\/a>. ~ Veronika Romashkina (@vronnie911). #Haskell #Cabal<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Closest_Pair_Points.html\">Closest pair of points algorithms<\/a>. ~ M. Rau, T. Nipkow. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.02981\">Automatic generation and verification of test-stable floating-point code<\/a>. ~ L. Titolo, M. Moscato, C.A. Mu\u00f1oz. #ITP #PVS<\/li>\n<li><a href=\"https:\/\/kwarc.info\/people\/mkohlhase\/submit\/tetrapod-survey.pdf\">The space of mathematical software systems<\/a>. ~ J. Carette, W.M. Farmer, Y. Sharoda. #ATP #ITP #Math #CompSci<\/li>\n<li><a href=\"https:\/\/www.cs.rit.edu\/~mtf\/student-resources\/20191_huang_mscourse.pdf\">A mechanized formalization of the WebAssembly specification in Coq<\/a>. ~ X. Huang. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/brendanfong.com\/programmingcats_files\/C4P-chapter1.pdf\">Is Haskell a category?<\/a> ~ B. Fong, B. Milewski, D. Spivak. #Haskell #FunctionalProgramming #CategoryTheory<\/li>\n<li><a href=\"https:\/\/medium.com\/@cdsmithus\/your-students-could-have-invented-the-pythagorean-theorem-438db433aec5\">Your students could have invented \u2026 the Pythagorean theorem<\/a>. ~ Chris Smith (@cdsmithus). #Math #Teaching<\/li>\n<li><a href=\"http:\/\/brendanfong.com\/programmingcats_files\/cats4progs-DRAFT.pdf\">Programming with categories (Draft)<\/a>. ~ B. Fong, B. Milewski, D.I. Spivak. #FunctionalProgramming #Haskell #CategoryTheory<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Approximation_Algorithms.html\">Verified approximation algorithms in Isabelle\/HOL<\/a>. ~ R. E\u00dfmann, T. Nipkow, S. Robillard. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.bbvaopenmind.com\/tecnologia\/innovacion\/la-magia-del-orden-de-los-datos\">La magia del orden (de los datos)<\/a>. ~ Alejandro Serrano (@trupill). #Algoritmos<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2020-01-16-data-vs-control.html\">A tale of two functors (or: how I learned to stop worrying and love Data and Control)<\/a>. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.youtube.com\/playlist?list=PLlF-CfQhukNkWwZt45vkNfWfuO-tBBqPN\">Talks from the formal methods in Mathematics \/ Lean together 2020 workshop<\/a>. #ITP #LeanProver #IsabelleHOL #Coq<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_cohen.pdf\">Generating mathematical structure hierarchies using Coq-ELPI<\/a>. ~ C. Cohen, K. Sakaguchi, E. Tassi. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/github.com\/math-comp\/hierarchy-builder\">High level commands to declare a hierarchy based on packed classes<\/a>. ~ C. Cohen, K. Sakaguchi, E. Tassi. #ITP #Coq #Math<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_gouezel.pdf\">On a mathematician&#8217;s attempts to formalize his own research in proof assistants<\/a>. ~ S\u00e9bastien Gou\u00ebzel. #ITP #IsabelleHOL #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_eberl.pdf\">Automating asymptotics in a theorem prover<\/a>. ~ Manuel Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_strickland.pdf\">Using Lean for new research<\/a>. ~ Neil Strickland. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.07801\">Iterated chromatic localisation<\/a>. ~ Neil Strickland, Nicola Bellumat. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/github.com\/NeilStrickland\/itloc\">Lean code formalising many of the proofs from the paper &#8220;Iterated chromatic localisation&#8221;<\/a>. ~ Neil Strickland, Nicola Bellumat. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/github.com\/NeilStrickland\/lean_primes\">Proof in Lean that there are infinitely many primes<\/a>. ~ Neil Strickland. #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_li.pdf\">Reasoning with non-linear formulas in Isabelle\/HOL<\/a>. ~ Wenda Li. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_immler.pdf\">ODEs and the Poincar\u00e9-Bendixson theorem in Isabelle\/HOL<\/a>. ~ Fabian Immler, Yong Kiam Tan. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.hpcwire.com\/2020\/01\/14\/julia-programmings-dramatic-rise-in-hpc-and-elsewhere\/\">Julia programming\u2019s dramatic rise in HPC and elsewhere<\/a>. ~ John Russell. #JuliaLang<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Complex_Geometry.html\">Complex geometry in Isabelle\/HOL<\/a>. ~ F. Mari\u0107, D. Simi\u0107. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Poincare_Disc.html\">Poincar\u00e9 disc model in Isabelle\/HOL<\/a>. ~ D. Simi\u0107, F. Mari\u0107, P. Boutry. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/alexnixon.github.io\/2020\/01\/14\/static-types-are-dangerous.html\">Static types are dangerously interesting<\/a>. ~ Alex Nixon (@alexnixon_uk). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/deontologician.com\/wiki\/lenses\/\">Digging into Lenses<\/a>. ~ Josh Kuhn (@deontologician). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_massot.pdf\">Formalizing a sophisticated definition<\/a>. ~ Patrick Massot, Kevin Buzzard, Johan Commelin. #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_boldo.pdf\">A Coq formalization of Lebesgue integration of nonnegative functions<\/a>. ~ Sylvie Boldo et als. #ITP #Coq #Math<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_lisitsa.pdf\">First-order theorem (dis)proving for reachability problems in verification and experimental mathematics<\/a>. ~ Alexei Lisitsa. #ATP #Prover9 #Mace4 #Math<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_keller.pdf\">SMTCoq: Coq automation and its application to formal mathematics<\/a>. ~ Chantal Keller. #ITP #Coq #SMT #Math<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_carneiro.pdf\">Metamath Zero (or: how to verify a verifier)<\/a>. ~ Mario Carneiro. #ITP #MetamathZero<\/li>\n<li><a href=\"http:\/\/flownet.com\/gat\/jpl-lisp.html\">Lisping at JPL<\/a>. ~ Ron Garret. #Programming #CommonLisp<\/li>\n<li><a href=\"https:\/\/www.microsiervos.com\/archivo\/matematicas\/numeros-primos-que-son-imagenes.html\">N\u00fameros primos que son im\u00e1genes<\/a>. ~ @Alvy #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/swmath.org\">swMATH: an information service for mathematical software<\/a>. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/www.encyclopediaofmath.org\">The Encyclopedia of Mathematics wiki is an open access resource designed specifically for the mathematics community<\/a>. #Math<\/li>\n<li><a href=\"http:\/\/www.encyclopediaofmath.org\/index.php?title=Theorem_prover&amp;oldid=31805\">Theorem prover<\/a>. ~ Encyclopedia of Mathematics. #ATP #ITP #Math<\/li>\n<li><a href=\"https:\/\/dlmf.nist.gov\/\">NIST digital library of mathematical functions<\/a>. #Math<\/li>\n<li><a href=\"https:\/\/oeis.org\">The On-Line Encyclopedia of Integer Sequences (OEIS)<\/a>. #Math<\/li>\n<li><a href=\"https:\/\/books.google.es\/books?id=0el8pO27BPoC&amp;lpg=PP1\">A modern perspective on type theory: From its origins until today<\/a>. ~ Fairouz Kamareddine, Twan Laan, and Rob Nederpelt. #eBook #TypeTheory<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/meetings\/fomm2020\/slides\/fomm_buzzard.pdf\">The future of Mathematics?<\/a> ~ Kevin Buzzard. #Math #ITP<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.04314\">Formal specification of a security framework for smart contracts<\/a>. ~ M. Mandrykin et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.04301\">Tabled typeclass resolution<\/a>. ~ D. Selsam, S. Ullrich, L. de Moura. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Mersenne_Primes.html\">Mersenne primes and the Lucas\u2013Lehmer test in Isabelle\/HOL<\/a>. ~ Manuel Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2020\/1\/20\/nicer-package-organization-with-stack\">Nicer package organization with Stack!<\/a> ~ James Bowen (@james_OWA). #Haskell #Stack<\/li>\n<li><a href=\"https:\/\/blog.sigplan.org\/2020\/01\/20\/a-small-matter-of-programming\/\">A small matter of programming<\/a>. ~ Jeremy Gibbons. #AI #Programming<\/li>\n<li><a href=\"https:\/\/richardzach.org\/2020\/01\/19\/adding-online-exercises-with-automated-grading-to-any-logic-course-with-carnap\/\">Adding online exercises with automated grading to any logic course with Carnap<\/a>. ~ Richard Zach (@RrrichardZach). #Logic #Teaching<\/li>\n<li><a href=\"https:\/\/youtu.be\/Rt2OrG3IHkU\">Three equivalent ordinal notation systems in cubical Agda<\/a>. ~ Fredrick Nordvall Forsberg. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/8542Cw7DdYY\">Undecidability of higher-order unification formalised in Coq<\/a>. ~ Simon Spies. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/youtu.be\/F35yA6EHrAo\">A functional proof pearl: Inverting the Ackermann heirarchy<\/a>. ~ Linh Tran. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1202.3670\">Euclid&#8217;s theorem on the infinitude of primes: a historical survey of its proofs (300 B<\/a>.C.\u20132017) and another new proof. ~ Romeo Me\u0161trovi\u0107. #Math #History<\/li>\n<li><a href=\"http:\/\/tedsider.org\/teaching\/higher_order_20\/higher_order_crash_course.pdf\">Crash course on higher-order logic, type theory, etc<\/a>. ~ Theodore Sider. #Logic via @RrrichardZach<\/li>\n<li><a href=\"https:\/\/youtu.be\/HKrIMvC4xTA\">Verified programming of Turing machines in Coq<\/a>. ~ Fabian Kunze. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/youtu.be\/EipOEWKlSBQ\">Proof pearl: Braun trees<\/a>. ~ Tobias Nipkow. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/blog.ploeh.dk\/2020\/01\/20\/algebraic-data-types-arent-numbers-on-steroids\/\">Algebraic data types aren&#8217;t numbers on steroids<\/a>. Mark Seemann (@ploeh). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/eprints.whiterose.ac.uk\/155734\/1\/hybrid_kat.pdf\">Differential Hoare logics and refinement calculi for hybrid systems with Isabelle\/HOL<\/a>. ~ Simon Foster, Jonathan Juli\u00e1n Huerta y Munive, and Georg Struth. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/niccoloveltri.github.io\/cpp20.pdf\">Formalizing \u03c0-calculus in Guarded Cubical Agda<\/a>. ~ Niccol\u00f2 Veltri, Andrea Vezzosi. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/argumatronic.com\/posts\/1970-01-01-beginners.html\">For beginners<\/a>. ~ Julie Moronuki (@argumatronic). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.08133\">Drawing Prolog search trees: A manual for teachers and students of logic programming<\/a>. ~ Johan Bos. #Prolog #LogicProgramming<\/li>\n<li><a href=\"ftp:\/\/ceur-ws.org\/pub\/publications\/rwth\/informatik\/2020\/2020-02.pdf\">Towards an Isabelle Theory for distributed, interactive systems-the untimed case<\/a>. ~ Jens Christoph B\u00fcrger et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/is.muni.cz\/th\/vhz48\/thesis.pdf\">Coinductive formalization of SECD machine in Agda<\/a>. ~ Adam Krupi\u010dka. #MsC_Thesis #ITP #Agda<\/li>\n<li><a href=\"https:\/\/typeclasses.com\/phrasebook\/folding-lists\">Folding lists<\/a>. ~ Chris Martin (@chris__martin), Julie Moronuki (@argumatronic). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mutable.jle.im\/\">Beautiful mutable values<\/a>. ~ Justin Le (@mstk). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.stephendiehl.com\/posts\/decade.html\">Haskell problems for a new decade<\/a>. ~ Stephen Diehl (@smdiehl). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cvlad.info\/profunctor\/\">The Functor family: Profunctor<\/a>. ~ Vladimir Ciobanu. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/ruor.uottawa.ca\/bitstream\/10393\/39994\/1\/Lu_Weiyun_2019_thesis.pdf\">Formally verified code obfuscation in the Coq Proof Assistant<\/a>. ~ Weiyun Lu. #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/~gaeher\/files\/3SATClique.pdf\">A formalised polynomial-time reduction from 3SAT to Clique<\/a>. ~ Lennard G\u00e4her. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/haskell-in-production-centralapp\">Haskell in production: CentralApp<\/a>. ~ Ashesh Ambasta (@AsheshAmbasta), Gints Dreimanis. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.microsiervos.com\/archivo\/matematicas\/conjetura-merterns-relacion-numero-colosalmente-grande.html\">La conjetura de Merterns y su relaci\u00f3n con un n\u00famero tan raro como extremada y colosalmente grande<\/a>. ~ @Alvy. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/www.irif.fr\/~emiquey\/content\/lmw19.pdf\">The benefits of sequent calculus<\/a>. ~ \u00c9tienne Miquey. #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/www.irif.fr\/~emiquey\/content\/imerl18.pdf\">Curry-Howard: unveiling the computational content of proofs<\/a>. ~ \u00c9tienne Miquey. #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/www.irif.fr\/~emiquey\/content\/banner.pdf\">Realizabilidad cl\u00e1sica y efectos colaterales: Extendiendo la correspondencia de Curry-Howard<\/a>. ~ \u00c9tienne Miquey. #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/github.com\/Coq-Andes-Summer-School\/CASS2020\/raw\/master\/assia-intro\/slides.pdf\">Introduction to Coq<\/a>. ~ Assia Mahboubi. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/cass.pleiad.cl\/jscoq\/examples\/funext\/lecture1.html\">First steps with Coq<\/a>. ~ Assia Mahboubi. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/Coq-Andes-Summer-School\/CASS2020\/raw\/master\/matthieu\/depelim.pdf\">Programming with dependent types in Coq: inductive families and dependent patter-matching<\/a>. ~ Matthieu Sozeau. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/Coq-Andes-Summer-School\/CASS2020\/raw\/master\/slides_tabareau.pdf\">Homotopy Type Theory<\/a>. ~ Nicolas Tabareau. #ITP #Coq #HoTT<\/li>\n<li><a href=\"https:\/\/github.com\/Coq-Andes-Summer-School\/CASS2020\/raw\/master\/typesets.pdf\">Set Theory vs. Type Theory<\/a>. Alexandre Miquel. #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.07488\">Profunctor optics, a categorical update<\/a>. ~ Bryce Clarke et als. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.research-collection.ethz.ch\/bitstream\/handle\/20.500.11850\/392353\/1\/Hossle_Nora.pdf\">Multiple address spaces in a distributed capability system<\/a>. ~ Nora Hossle. #MsC_Thesis #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.07655\">Coherence via wellfoundedness<\/a>. ~ Nicolai Kraus, Jakob von Raumer. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1912.10961\">Formalizing the Curry-Howard correspondence<\/a>. ~ Juan Ferrer Meleiro, Hugo Luiz Mariano. #ITP #Idris #Logic<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/a-sketch-of-categorical-relation-algebra-combinators-in-z3py\/\">A sketch of categorical relation algebra combinators in Z3Py<\/a>. ~ Philip Zucker (@SandMouth). #Z3 #SMT<\/li>\n<li><a href=\"https:\/\/blog.adrianistan.eu\/primeros-pasos-nix-linux-funcional\">Primeros pasos con Nix: un Linux m\u00e1s funcional<\/a>. ~ Adri\u00e1n Arroyo Calle. #Nix #Linux #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/oleg.fi\/gists\/posts\/2020-01-25-case-study-migration-from-lens-to-optics.html\">Case study: migrating from lens to optics<\/a>. ~ Oleg Grenrus (@phadej). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/ruor.uottawa.ca\/bitstream\/10393\/39876\/1\/Eaman_Amir_2019_thesis.pdf\">TEpla: A certified type enforcement access-control policy language<\/a>. ~ Amir Eaman. #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.cambridge.org\/core\/journals\/journal-of-functional-programming\/article\/elaborating-dependent-copattern-matching-no-pattern-left-behind\/F13CECDAB2B6200135D45452CA44A8B3\">Elaborating dependent (co)pattern matching: No pattern left behind<\/a>. ~ Jesper Cockx, Andreas Abel. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/homotopytypetheory.org\/2020\/01\/26\/the-cantor-schroder-bernstein-theorem-for-%e2%88%9e-groupoids\/\">The Cantor-Schr\u00f6der-Bernstein theorem for \u221e-groupoids<\/a>. ~ Martin Escardo. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.06702\">FASiM: A framework for automatic formal analysis of simulink models of linear analog circuits<\/a>. ~ Adnan Rashid, Ayesha Gauhar and Osman Hasan. #ITP #HOL_Light<\/li>\n<li><a href=\"https:\/\/tech.fpcomplete.com\/blog\/transformations-on-applicative-concurrent-computations\">Transformations on applicative concurrent computations<\/a>. ~ Rom\u00e1n Gonz\u00e1lez. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/gup.ub.gu.se\/file\/208036\">The beauty of abstraction in mathematics<\/a>. ~ Thomas Lingefj\u00e4rd, Russell Hatami. #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.09715\">Formalization of forcing in Isabelle\/ZF<\/a>. ~ Emmanuel Gunther, Miguel Pagano, Pedro S\u00e1nchez Terraf. #ITP #IsabelleZF #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.05970\">HolPy: Interactive theorem proving in Python<\/a>. ~ Bohua Zhan. #ITP #HolPy #Logic #Python<\/li>\n<li><a href=\"https:\/\/bzg.fr\/en\/some-emacs-org-mode-features-you-may-not-know.html\/\">Org-mode features you may not know<\/a>. ~ Bastien Guerry (@bzg2). #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.10834\">Smart induction for Isabelle\/HOL (System description)<\/a>. ~ Yutaka Nagashima. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/stackoverflow.com\/a\/59719944\/5157338\">Show that a monic (injective) and epic (surjective) function has an inverse in Coq<\/a>. ~ Arthur Azevedo De Amorim. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/blog.sigplan.org\/2020\/01\/29\/mechanized-proofs-for-pl-past-present-and-future\/\">Mechanized proofs for PL: Past, present, and future<\/a>. ~ Talia Ringer. #ITP<\/li>\n<li><a href=\"https:\/\/golem.ph.utexas.edu\/category\/2020\/01\/profunctor_optics_the_categori.html\">Profunctor optics: The categorical view<\/a>. ~ Emily Pillmore and Mario Rom\u00e1n. #Haskell #FunctionalProgramming #CategoryTheory<\/li>\n<li><a href=\"http:\/\/blog.ezyang.com\/2020\/01\/vmap-in-haskell\">vmap in Haskell<\/a>. ~ Edward Z. Yang (@ezyang). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/developing-ghc-for-a-living\">Developing GHC for a Living: Interview with Vladislav Zavialov<\/a>. ~ Denis Oleynikov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2020-01-29-terminating-tricky-traversals.html\">Terminating tricky traversals<\/a>. ~ Donnacha Ois\u00edn Kidney (@oisdk). #Haskell #Agda #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2020-01-30-haskell-profiling.html\">Locating performance bottlenecks in large Haskell codebases<\/a>. ~ Juan Raphael Diaz Sim\u00f5es. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/hal.laas.fr\/hal-02088529v2\/document\">A certificate-based approach to formally verified approximations<\/a>. ~ Florent Br\u00e9hard, Assia Mahboubi, Damien Pous. #ITP #Coq #Math<\/li>\n<li><a href=\"http:\/\/www.staff.science.uu.nl\/~swier004\/publications\/2020-msfp-submission.pdf\">Combining predicate transformer semantics for effects: a case study in parsing regular languages<\/a>. ~ Tim Baanen, Wouter Swierstra. #Agda #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/era.ed.ac.uk\/bitstream\/handle\/1842\/22936\/Raggi2016.pdf\">Searching the space of representations: reasoning through transformations for mathematical problem solving<\/a>. ~ Daniel Raggi. #PhD_Thesis #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/bor0.wordpress.com\/2020\/01\/31\/introduction-and-formalization-of-boolean-algebra\/\">Introduction and formalization of Boolean algebra<\/a>. ~ Boro Sitnikovski (@BSitnikovski). #ITP #Metamath #Math<\/li>\n<li><a href=\"https:\/\/cs-syd.eu\/posts\/2020-01-28-property-testing-size\">Property testing in depth: The size parameter<\/a>. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/bytes.yingw787.com\/posts\/2020\/01\/30\/a_review_of_haskell\/\">A Pythonista&#8217;s Review of Haskell<\/a>. ~ Ying Wang. #Haskell #Python<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante enero 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\/7217"}],"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=7217"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7217\/revisions"}],"predecessor-version":[{"id":7218,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7217\/revisions\/7218"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7217"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7217"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7217"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}