{"id":7213,"date":"2020-07-01T18:22:28","date_gmt":"2020-07-01T16:22:28","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7213"},"modified":"2020-08-01T18:25:12","modified_gmt":"2020-08-01T16:25:12","slug":"resumen-de-lecturas-compartidas-durante-junio-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-junio-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas durante junio de 2020"},"content":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante junio 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:\/\/emanuelpeg.blogspot.com\/2020\/05\/breve-historia-de-haskell.html\">Breve historia de Haskell<\/a>. ~ Emanuel Goette (@emanuelpeg). #Haskell #Programaci\u00f3nFuncional<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Nash_Williams.html\">The Nash-Williams partition theorem in Isabelle\/HOL<\/a>. ~ Lawrence C. Paulson. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/romainviallard.dev\/en\/blog\/setting-up-a-haskell-development-environment-with-nix\/\">Setting up a Haskell development environment with Nix<\/a>. ~ Romain Viallard. #Haskell #Nix<\/li>\n<li><a href=\"https:\/\/nottingham-repository.worktribe.com\/preview\/4475690\/big_step_normalisation.pdf\">Big step normalisation for type theory<\/a>. ~ Thorsten Altenkirch, Colin Geniet. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/techxplore.com\/news\/2020-06-carnegie-mellon-tool-automatically-math.html\">Carnegie Mellon tool automatically turns math into pictures<\/a>. #Math<\/li>\n<li><a href=\"http:\/\/penrose.ink\/siggraph20.html\">Penrose: from mathematical notation to beautiful diagrams<\/a>. ~ Katherine Ye el als. #Math<\/li>\n<li><a href=\"http:\/\/prooftheory.blog\/2020\/05\/01\/hello-world\/\">Welcome to The Proof Theory Blog! ~ Anupam Das<\/a>. #Logic #Math<\/li>\n<li><a href=\"https:\/\/github.com\/penrose\/penrose\">Penrose: Create beautiful diagrams just by typing mathematical notation in plain text<\/a>. #Haskell #DSL #Math #Visualization<\/li>\n<li><a href=\"https:\/\/wiki.alcidesfonseca.com\/blog\/lean-tutorial-mere-mortals\/\">Lean tutorial for mere mortals<\/a>. ~ Alcides Fonseca. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Safe_Distance.html\">A formally verified checker of the safe distance traffic rules for autonomous vehicles<\/a>. ~ Albert Rizaldi, Fabian Immler. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.kestrel.edu\/home\/people\/coglio\/acl220i.pdf\">Isomorphic data type transformations<\/a>. ~ Alessandro Coglio, Stephen Westfold. #ITP #ACL2<\/li>\n<li><a href=\"https:\/\/lmcs.episciences.org\/6518\/pdf\">Cellular cohomology in homotopy type theory<\/a>. ~ Ulrik Buchholtz, Kuen-Bang Hou. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/download.clojure.org\/papers\/clojure-hopl-iv-final.pdf\">A history of Clojure<\/a>. ~ Rich Hickey. #Clojure #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/samtay.github.io\/posts\/refactoring-adventures\">Adventures in refactoring<\/a>. ~ Sam Tay. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/williamyaoh.com\/posts\/2020-05-31-reanimate-nqueens-tutorial.html\">Reanimate: a tutorial on making programmatic animations<\/a>. ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/jmtd.net\/log\/template_haskell\/boilerplate\/\">Using Template Haskell to generate boilerplate<\/a>. ~ Jonathan Dowland. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/oleg.fi\/gists\/posts\/2020-06-02-simulated-annealing.html\">Simulated annealing<\/a>. ~ Oleg Grenrus (@phadej). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.fosskers.ca\/en\/blog\/tolist\">Trusting toList<\/a>. ~ Colin Woodbury (@fosskers). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/formal-verification-history\">Formal verification: History and methods<\/a>. ~ Danya Rogozin. #FormalVerification<\/li>\n<li><a href=\"https:\/\/www.redblobgames.com\/\">Red Blob Games: interactive visual explanations of math and algorithms, using motivating examples from computer games<\/a>. ~ Amit Patel. #Algorithms<\/li>\n<li><a href=\"https:\/\/medium.com\/@cdsmithus\/toy-machine-learning-with-haskell-b18cd04fb9e1\">Toy machine learning with Haskell<\/a>. ~ Chris Smith (@cdsmithus). #Haskell #FunctionalProgramming #MachineLearning<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2020\/06\/05\/the-sphere-eversion-project\/\">The sphere eversion project<\/a>. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/books.google.es\/books?id=toLoDwAAQBAJ&amp;lpg=PR13&amp;ots=OnJD33xm6P&amp;pg=PP\">Algorithm design with Haskell<\/a>. ~ Richard Bird, Jeremy Gibbons.1#v=onepage&amp;q&amp;f=false #eBook #Haskell #FunctionalProgramming #Algorithms<\/li>\n<li><a href=\"http:\/\/ayala.mat.unb.br\/mf_PVS0.pdf\">Formalization of the computational theory of a Turing complete functional language model<\/a>. ~ TMF Ramos, AA Almeida, M Ayala-Rinc\u00f3n. #ITP #PVS<\/li>\n<li><a href=\"http:\/\/www.lix.polytechnique.fr\/Labo\/Dale.Miller\/papers\/tease-lp-2020.pdf\">The proof-theoretic foundations of logic programming<\/a>. ~ Dale Miller. #LogicProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/@getsmarter\/what-is-mathematics-5f39b41a4db1\">What is Mathematics?<\/a> ~ Get Smarter. #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2006.03525\">Formalizing text editors in Coq<\/a>. ~ Boro Sitnikovski. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/lukelau.me\/haskell\/posts\/making-the-most-of-cabal\/\">Making the most of Cabal<\/a>. ~ Luke Lau. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dixonary.co.uk\/blog\/haskell\/pain\">The pain points of Haskell: A practical summary<\/a>. ~ Alex Dixon (@dixonary_). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/towardsdatascience.com\/functional-programing-in-data-science-projects-c909c11138bb\">Functional programming in data science projects<\/a>. ~ Nathanael Weill. #FuncionalProgramming #DataScience<\/li>\n<li><a href=\"https:\/\/medium.com\/@cdsmithus\/using-client-side-haskell-web-frameworks-in-codeworld-7d8661647191\">Using client-side Haskell web frameworks in CodeWorld<\/a>. ~ Chris Smith (@cdsmithus). #Haskell #CodeWorld<\/li>\n<li><a href=\"https:\/\/www.linuxlinks.com\/excellent-free-books-learn-agda-type-theory\/\">4 excellent free books to learn Agda and type theory<\/a>. ~ Erik Karlsson. #ITP #Agda #FunctionalProgramming #TypeTheory<\/li>\n<li><a href=\"https:\/\/github.com\/disco-lang\/disco\/\">Disco: Functional teaching language for use in a discrete mathematics course<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming #DSL #Math<\/li>\n<li><a href=\"http:\/\/neilmitchell.blogspot.com\/2020\/06\/hoogle-searching-overview.html\">Hoogle searching overview<\/a>. ~ Neil Mitchell (@ndm_haskell). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/the-useless-perspective-that-transformed-mathematics-20200609\/\">The \u2018useless\u2019 perspective that transformed mathematics<\/a>. ~ Kevin Hartnett (@KSHartnett). #Math<\/li>\n<li><a href=\"https:\/\/rjlipton.wordpress.com\/2020\/06\/04\/the-truth\/\">&#8220;The truth: What is the truth?&#8221;, at G\u00f6del&#8217;s Lost Letter and P=NP<\/a>. ~ R.J. Lipton. #Logic #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/PU9Gs-XRYEQ\">Scripting in Haskell: Parsing command line arguments<\/a>. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/jmtd.net\/log\/template_haskell\/streamgraph\/\">Template Haskell and stream-processing programs<\/a>. ~ Jonathan Dowland (@jmtd). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/patternsinfp.wordpress.com\/2018\/11\/21\/how-to-design-co-programs\/\">How to design co-programs<\/a>. ~ Jeremy Gibbons. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/aperiodical.com\/2020\/06\/conways-circle-theorem-a-proof-this-time-with-words\/\">Conway\u2019s circle theorem: a proof, this time with words<\/a>. ~ Colin Beveridge, Elizabeth A. Williams. #Math<\/li>\n<li><a href=\"https:\/\/github.com\/affeldt-aist\/monae\">Monadic equational reasoning in Coq<\/a>. ~ Reynald Affeldt. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/www.math.mcgill.ca\/triples\/Barr-Wells-ctcs.pdf\">Category theory for computing science<\/a>. ~ Michael Barr, Charles Wells (1998). #eBook #CategoryTheory #Math #CompSci<\/li>\n<li><a href=\"https:\/\/math.mit.edu\/~dspivak\/teaching\/sp18\/7Sketches.pdf\">Seven sketches in compositionality: An invitation to applied category theory<\/a>. ~ Brendan Fong, David I. Spivak (2018). #eBook #CategoryTheory #Math #CompSci<\/li>\n<li><a href=\"https:\/\/www.inner-product.com\/posts\/fp-what-and-why\/\">What functional programming is, what it isn&#8217;t, and why it matters<\/a>. ~ Noel Welsh. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/zfoh\/haskell-simple-install\">Simple Haskell install instructions &#8211; ZuriHac 2020<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.lemonde.fr\/blog\/binaire\/2020\/06\/12\/la-logique-un-instrument-theorique-pour-des-problemes-pratiques\/\">La logique: un instrument th\u00e9orique pour des probl\u00e8mes pratiques<\/a>. ~ Franco Raimondi. #Logic #Math #CompSci<\/li>\n<li><a href=\"https:\/\/romainviallard.dev\/en\/blog\/deploying-your-app-with-nixos\/\">Deploying your application with NixOS<\/a>. ~ Romain Viallard. #Nix #Haskell<\/li>\n<li><a href=\"https:\/\/citeseerx.ist.psu.edu\/viewdoc\/download;jsessionid=B2E32B9A9303A9017662D564EB848FFE?doi=10.1.1.110.122&amp;rep=rep1&amp;type=pdf\">An extended comparative study of language support for generic programming<\/a>. ~ Ronald Garcia, Jaakko J \u00c4rvi, Andrew Lumsdaine, Jeremy Siek, Jeremiah Willcock. #Cpp #SML #OCaml #Haskell #Eiffel #Java #Csharp #Cecil.<\/li>\n<li><a href=\"http:\/\/adam.chlipala.net\/theses\/zygi.pdf\">Towards a verified first-stage bootloader in Coq<\/a>. ~ Zygimantas Straznickas. #MsC_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/2006.04399.pdf\">Completeness theorems for first-order logic analysed in constructive type theory<\/a>. ~ Yannick Forster, Dominik Kirst, Dominik Weh. #ITP #Coq #Logic<\/li>\n<li><a href=\"http:\/\/www21.in.tum.de\/~lammich\/isabelle_llvm\/paper_IJCAR2020.pdf\">Efficient verified implementation of introsort and pdqsort<\/a>. ~ Peter Lammich. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/youtu.be\/x0R5h190Yts\">(Programming Languages) in Agda = Programming (Languages in Agda)<\/a>. ~ Philip Wadler. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/ttaylorr.com\/publications\/uw-thesis.pdf\">Verifying strong eventual consistency in \u03b4-CRDTs<\/a>. Taylor Blau. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3386336\">The history of Standard ML<\/a>. ~ David MacQueen, Robert Harper, John Reppy. #SML #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/y0GwxCDTJvA\">Programaci\u00f3n funcional: Pr\u00f3ximamente en un lenguaje de programaci\u00f3n cerca de usted<\/a>. ~ Andr\u00e9s Marzal. #Programaci\u00f3nFuncional<\/li>\n<li><a href=\"https:\/\/andys8.github.io\/awesome-haskell-videos\/\">Awesome Haskell videos (A collection of awesome Haskell videos)<\/a>. ~ @_andys8 #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/splintah.gitlab.io\/posts\/2020-06-14-Type-inference.html\">Type inference<\/a>. ~ Splinter Suidman. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.mimuw.edu.pl\/~lukaszcz\/sauto.pdf\">Practical proof search for Coq by type inhabitation<\/a>. ~ Lukasz Czajka. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2002.00620\">Validating mathematical structures<\/a>. ~ Kazuhiko Sakaguchi. #ITP #Coq #math<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-02463336v2\/document\">Competing inheritance paths in dependent type theory: a case study in functional analysis<\/a>. ~ Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling and Kazuhiko Sakaguchi. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www21.in.tum.de\/~traytel\/papers\/ijcar20-qbnf\/qbnf.pdf\">Quotients of bounded natural functors<\/a>. ~ Basil F\u00fcrer, Andreas Lochbihler, Joshua Schneider and Dmitriy Traytel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/github.com\/prathyvsh\/formal-systems-in-biology\">Application of formal systems to model biological systems<\/a>. ~ @prathyvsh #Math #Biology<\/li>\n<li><a href=\"http:\/\/pit-claudel.fr\/clement\/papers\/fiat-to-facade.pdf\">Extensible extraction of efficient imperative programs with foreign functions, manually managed memory, and proofs<\/a>. ~ Cl\u00e9ment Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross and Adam Chlipala. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/acl2-2020.info\/slides\/adventures-verifying-arithmetic.pdf\">Adventures in verifying arithmetic<\/a>. ~ John Harrison. #ITP #HOL_Light #Math<\/li>\n<li><a href=\"https:\/\/www21.in.tum.de\/~traytel\/papers\/ijcar20-verimonplus\/verimonplus.pdf\">A formally verified, optimized monitor for metric first-order dynamic logic<\/a>. ~ David Basin, Thibault Dardinier, Lukas Heimes, Sr\u0111an Krsti\u0107, Martin Raszyk, Joshua Schneider, Dmitriy Traytel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1910.03740.pdf\">The resolution of Keller&#8217;s conjecture<\/a>. ~ Joshua Brakensiek, Marijn Heule, John Mackey, David Narvaez. ~ #ATP #SAT_Solver #Math<\/li>\n<li><a href=\"https:\/\/bartoszmilewski.com\/2020\/06\/15\/monoidal-catamorphisms\/\">Monoidal catamorphisms<\/a>. ~ Bartosz Milewski (@BartoszMilewski). #Haskell #CategoryTheory<\/li>\n<li><a href=\"http:\/\/www.openculture.com\/free-math-textbooks\">Free Math Textbooks<\/a>. #Math<\/li>\n<li><a href=\"https:\/\/www.47deg.com\/blog\/io-haskell\/\">The power of IO in Haskell<\/a>. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2020\/6\/15\/training-our-agent-with-haskell\">Training our agent with Haskell!<\/a> ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.cs.vu.nl\/~tbn305\/publicaties\/2020-ring_exp.pdf\">A Lean tactic for normalising ring expressions with exponents<\/a>. ~ Anne Baanen. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/simon-robillard.net\/content\/essmann2020approximation.pdf\">Verified approximation algorithms<\/a>. ~ Robin E\u00dfmann, Tobias Nipkow, Simon Robillard. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/emanuelpeg.blogspot.com\/2020\/06\/analisis-de-texto-usando-funciones-de.html\">An\u00e1lisis de texto usando funciones de orden superior<\/a>. ~ Emanuel Goette (@emanuelpeg). #Haskell #Programaci\u00f3nFuncional<\/li>\n<li><a href=\"https:\/\/well-typed.com\/blog\/2020\/06\/th-for-static-data\/\">Using Template Haskell to generate static data<\/a>. ~ Andreas Klebinger. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2006.09884\">Computer-assisted proofs for Lyapunov stability via Sums of Squares certificates and Constructive Analysis<\/a>. ~ Grigory Devadze, Victor Magron, Stefan Streif. #ITP #MinLog #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/geV8F59q48E\">Basic optics: lenses, prisms, and traversals in Haskell<\/a>. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.danielbrice.net\/blog\/simple-linear-regression-in-one-pass\/\">Simple linear regression in one pass<\/a>. ~ Daniel Brice (@fried_brice). #Haskell #FuncionalProgramming<\/li>\n<li><a href=\"https:\/\/dev.to\/theodesp\/solving-algorithm-challenges-in-haskell-anagrams-15jd\">Solving algorithm challenges in Haskell: Anagrams<\/a>. ~ Theofanis Despoudis (@nerdokto). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/leanprover.github.io\/talks\/LeanPLDI.pdf\">Lean 4<\/a>. ~ Leonardo de Moura, Sebastian Ullrich. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/www.connectedpapers.com\/\">Connected Papers: A visual tool to help researchers and practitioners find and explore academic papers<\/a>. ~ @ConnectedPapers<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/blog\/2020-06-19-linear-types-merged\/\">Linear types are merged in GHC<\/a>. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/bor0.wordpress.com\/2020\/06\/20\/proofs-and-computation-with-trees\/\">Proofs and computation with trees<\/a>. ~ Boro Sitnikovski (@BSitnikovski). #Math #CompSci<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2020\/06\/20\/mathematics-in-type-theory\/\">Mathematics in type theory<\/a>. ~ Kevin Buzzard (@XenaProject). #Logic #Math #ITP #LeanProver<\/li>\n<li><a href=\"http:\/\/syrcose.ispras.ru\/2020\/presentations\/SYRCoSE_2020_slides_05_99.pdf\">Verified Isabelle\/HOL tactic for the theory of bounded linear integer arithmeticl based on quantifier instantiation and SMT<\/a>. ~ Rafael Sadykov , Mikhail Mandrykin. #ITP #IsabelleHOL #SMT<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/LTL_Normal_Form.html\">An efficient normalisation procedure for linear temporal logic: Isabelle\/HOL formalisation<\/a>. ~ Salomon Sickert. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"http:\/\/acl2-2020.info\/papers\/formal-verification-of-arithmetic-rtl.pdf\">Formal verification of arithmetic RTL: Translating Verilog to C++ to ACL2<\/a>. ~ David M. Russinoff. #ITP #ACL2<\/li>\n<li><a href=\"http:\/\/acl2-2020.info\/papers\/cauchy-schwarz.pdf\">Cauchy-Schwarz in ACL2(r) abstract vector spaces<\/a>. ~ Carl Kwan, Yan Peng, Mark R. Greenstreet. #ITP #ACL2 #Math<\/li>\n<li><a href=\"http:\/\/acl2-2020.info\/papers\/quadratic-extensions.pdf\">Quadratic extensions in ACL2<\/a>. ~ Ruben Gamboa, John Cowles, Woodrow Gamboa. #ITP #ACL2 #Math<\/li>\n<li><a href=\"http:\/\/syrcose.ispras.ru\/2020\/submissions\/SYRCoSE_2020_paper_09_81.pdf\">Techniques for implementation of symbolically interpretable Haskell EDSLs<\/a>. ~ Grigoriy Volkov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/jesper.sikanda.be\/files\/leibniz-equality.pdf\">Leibniz equality is isomorphic to Martin-L\u00f6f identity, parametrically<\/a>. ~ Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany. #ITP #Agda #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/j2xYSxMkXeQ\">Strongly typed system F in GHC<\/a>. ~ Stephanie Weirich. #Haskell #FunctionalProgramming #Logic<\/li>\n<li><a href=\"https:\/\/www.cnblogs.com\/ncore\/p\/6892500.html\">An introduction to parsing text in Haskell with Parsec<\/a>. ~ Nick Chung. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/neilmitchell.blogspot.com\/2020\/06\/the-hlint-match-engine.html\">The HLint match engine<\/a>. ~ Neil Mitchell (@ndm_haskell). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2020\/6\/22\/rendering-frozen-lake-with-gloss\">Rendering frozen lake with Gloss!<\/a> ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/dev.stephendiehl.com\/new_decade.pdf\">Haskell for a new decade<\/a>. ~ Stephen Diehl (@smdiehl). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cs.nott.ac.uk\/~pszgmh\/ccc2.pdf\">Calculating correct compilers II (Return of the register machines)<\/a>. ~ Patrick Bahr, Graham Hutton. #Haskell #FuncionalProgramming<\/li>\n<li><a href=\"https:\/\/files.sketis.net\/Isabelle_Workshop_2020\/Isabelle_2020_paper_10.pdf\">Lucas\u2019s theorem: Formalising generating function proofs<\/a>. ~ Chelsea Edmonds. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/files.sketis.net\/Isabelle_Workshop_2020\/Isabelle_2020_paper_1.pdf\">Ackermann\u2019s function in iterative form: A subtle termination proof with Isabelle\/HOL<\/a>. ~ Lawrence Paulson. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/philomatica.org\/wp-content\/uploads\/2020\/06\/bde.pdf\">Axiomatic architecture of scientific theories<\/a>. ~ Andrei V. Rodin. #PhD_Thesis #Logic #Math<\/li>\n<li><a href=\"https:\/\/files.sketis.net\/Isabelle_Workshop_2020\/Isabelle_2020_paper_6.pdf\">A concise sequent calculus for teaching first-order logic<\/a>. ~ Asta Halkj\u00e6r From, J\u00f8rgen Villadsen. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/files.sketis.net\/Isabelle_Workshop_2020\/Isabelle_2020_paper_4.pdf\">SErAPIS : A concept-oriented search engine for the Isabelle libraries based on natural language<\/a>. ~ Yiannos Stathopoulos, Angeliki Koutsoukou-Argyraki, Lawrence Paulson. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/files.sketis.net\/Isabelle_Workshop_2020\/Isabelle_2020_paper_5.pdf\">Authenticated data structures as functors in Isabelle\/HOL<\/a>. ~ Andreas Lochbihler, Ognjen Mari\u0107. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/files.sketis.net\/Isabelle_Workshop_2020\/Isabelle_2020_paper_11.pdf\">A generic framework for verified compilers using Isabelle\/HOL\u2019s locales<\/a>. ~ Martin Desharnais, Stefan Brunthaler. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2020\/06\/24\/competitive-programming-in-haskell-vectors-and-2d-geometry\/\">Competitive programming in Haskell: vectors and 2D geometry<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.seer.ufrgs.br\/rita\/article\/download\/Vol27_nr3_13\/pdf_1\">A mechanized proof of a textbook type unification algorithm<\/a>. ~ Maycon Amaro, Rodrigo Ribeiro, Andr\u00e9 Rauber Du Bois. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.seer.ufrgs.br\/rita\/article\/download\/Vol27_nr3_84\/pdf_1\">Reasoning about partial correctness assertions in Isabelle\/HOL<\/a>. ~ A.R. Martini. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02874762\/document\">Extensive infinite games and escalation, an exercice in Agda<\/a>. ~ Pierre Lescanne. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2003.05081\">Animated logic: Correct functional conversion to conjunctive normal form<\/a>. ~ Pedro Barroso, M\u00e1rio Pereira, Ant\u00f3nio Ravara. #Why3 #Logic<\/li>\n<li><a href=\"https:\/\/www.mat.unb.br\/~ayala\/TeachingIP2Mathematicians.pdf\">Teaching interactive proofs to mathematicians<\/a>. ~ M. Ayala-Rinc\u00f3n, T.A. de Lima. #ITP #PVS #Math<\/li>\n<li><a href=\"http:\/\/ayala.mat.unb.br\/Summer_UnB_2020\/program.html\">Interactively proving mathematical theorems<\/a>. ~ M. Ayala-Rinc\u00f3n et als. #Logic #Math #ITP #PVS<\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/undergrad.html\">Undergraduate mathematics in mathlib<\/a>. #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/ayala.mat.unb.br\/Formalization_of_Ring_Theory.pdf\">Formalization of ring theory in PVS (Isomorphism theorems, principal, prime and maximal ideals ,chinese remainder theorem)<\/a>. ~ T.A. de Lima, A L. Galdino, A. Borges Avelar, M. Ayala-Rinc\u00f3n. #ITP #PVS #Math<\/li>\n<li><a href=\"http:\/\/ayala.mat.unb.br\/CICM_NFM.pdf\">Why we need structured proofs in mathematics<\/a>. ~ M. Ayala-Rinc\u00f3n, G.F. Silva. #Logic #Math #ITP #PVS<\/li>\n<li><a href=\"https:\/\/hbr.github.io\/Lambda-Calculus\/untyped_lambda.pdf\">Lambda Calculus &#8211; step by step<\/a>. ~ Helmut Brandl. #Logic #Math #CompSci #LambdaCalculus<\/li>\n<li><a href=\"https:\/\/hbr.github.io\/Lambda-Calculus\/lambda.pdf\">Programming with Lambda Calculus<\/a>. ~ Helmut Brandl. #Logic #Math #CompSci #LambdaCalculus<\/li>\n<li><a href=\"https:\/\/ai.stanford.edu\/~nilsson\/QAI\/qai.pdf\">The quest for Artificial Intelligence (A history of ideas and achievements)<\/a>. ~ Nils J. Nilsson. #eBook #AI<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2020\/06\/27\/teaching-dependent-type-theory-to-4-year-olds-via-mathematics\/\">Teaching dependent type theory to 4 year olds via mathematics<\/a>. ~ Kevin Buzzard (@XenaProject). #Math #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2004.07761\">Deep generation of Coq lemma names using elaborated terms<\/a>. ~ Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.investigacionyciencia.es\/revistas\/investigacion-y-ciencia\/una-nueva-era-para-el-alzhimer-803\/el-traje-nuevo-de-la-inteligencia-artificial-18746\">El traje nuevo de la inteligencia artificial<\/a>. ~ Ramon L\u00f3pez de M\u00e1ntaras. #IA<\/li>\n<li><a href=\"https:\/\/dev.to\/itsjzt\/try-these-4-languages-from-4-corners-of-programming-epm%20\">Try these 4 languages from 4 corners of programming<\/a>. ~ Saurabh Sharma (@itsjzt). #C #Smalltak #Clojure #Haskell<\/li>\n<li><a href=\"https:\/\/youtu.be\/26ViUXHtah0\">Using Haskell in the Mission Control Domain<\/a>. ~ Michael Oswald (@OswaldChocolate). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/blog\/2020-06-29-prng-test\/\">Splittable pseudo-random number generators in Haskell: random v1<\/a>.1 and v1.2. ~ Leonhard Markert. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2006.13613.pdf\">Formalizing the soundness of the encoding methods of SAT-based model checking<\/a>. ~ Daisuke Ishii, Saito Fujii. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.twitch.tv\/videos\/661148267\">Teaching Lean what a group is (ignoring the fact that it actually already knows)<\/a>. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2020\/06\/29\/competitive-programming-in-haskell-data-representation-and-optimization-with-cake\/\">Competitive programming in Haskell: data representation and optimization, with cake<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/JJv74IJUp4E\">Algorithm design with Haskell<\/a>. ~ Jeremy Gibbons (@jer_gib). #Haskell #FunctionalProgramming<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante junio 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\/7213"}],"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=7213"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7213\/revisions"}],"predecessor-version":[{"id":7214,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7213\/revisions\/7214"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7213"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7213"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7213"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}