{"id":7210,"date":"2020-06-01T18:19:15","date_gmt":"2020-06-01T16:19:15","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7210"},"modified":"2020-08-01T18:22:06","modified_gmt":"2020-08-01T16:22:06","slug":"resumen-de-lecturas-compartidas-durante-mayo-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-mayo-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas durante mayo de 2020"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante mayo 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:\/\/www.isa-afp.org\/entries\/Gaussian_Integers.html\">Gaussian integers in Isabelle\/HOL<\/a>. ~ Manuel Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Power_Sum_Polynomials.html\">Power sum polynomials and the Girard\u2013Newton theorem in Isabelle\/HOL<\/a>. ~ Manuel Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.00205\">The Ramanujan Machine: Automatically generated conjectures on fundamental constants<\/a>. ~ Gal Raayoni et als. #MachineLearning #Math<\/li>\n<li><a href=\"https:\/\/pages.cs.wisc.edu\/~justhsu\/teaching\/current\/cs538\/calendar\/\">UWisconsin course on Haskell and Rust<\/a>. #Haskell #Rust<\/li>\n<li><a href=\"https:\/\/iokasimov.github.io\/posts\/2020\/04\/waterflow\">Learn to moonwalk with waterflow problem<\/a>. ~ Murat Kasimov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cs-syd.eu\/posts\/2020-04-28-genvalidity-improvements\">Property testing in depth: genvalidity&#8217;s fixed-size type generators<\/a>. ~ Tom Sydney Kerckhove. #Haskell #QuickCheck<\/li>\n<li><a href=\"https:\/\/www.hcii.cmu.edu\/news\/2020\/new-ai-enables-teachers-rapidly-develop-intelligent-tutoring-systems\">New AI enables teachers to rapidly develop intelligent tutoring systems<\/a>. #AI #Teaching<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007%2F978-3-030-45190-5_24.pdf\">Verified certification of reachability checking for timed automata<\/a>. ~ Simon Wimmer, Joshua von Mutius. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007%2F978-3-030-45237-7_11.pdf\">Formalized proofs of the infinity and normal form predicates in the first-order theory of rewriting<\/a>. ~ Alexander Lochmann, Aart Middeldorp. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2004.12030\">Formal proof of the group law for Edwards elliptic curves<\/a>. ~ Thomas Hales, Rodrigo Raya. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2004.12713%20\">Formal adventures in convex and conical spaces<\/a>. ~ Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2020-05-02-more-random-access-lists.html\">More random access lists<\/a>. ~ Donnacha Ois\u00edn Kidney (@oisdk). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/escholarship.org\/content\/qt1623m1p3\/qt1623m1p3.pdf\">History of Logo<\/a>. ~ C. Solomon et als. #Logo #Programming<\/li>\n<li><a href=\"http:\/\/ojs.elte.hu\/cejntrep\/article\/view\/470\/381\">Interactive teaching of programming language theory with a proof assistant<\/a>. ~ Horp\u00e1csi D\u00e1niel et als. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/ojs.elte.hu\/cejntrep\/article\/view\/399\/386\">A problem-based curriculum for algorithmic programming<\/a>. ~ Nikh\u00e1zy L\u00e1szl\u00f3. #Programming<\/li>\n<li><a href=\"https:\/\/towardsdatascience.com\/bye-bye-python-hello-julia-9230bff0df62\">Bye-bye Python. Hello Julia!<\/a> ~ Rhea Moutafis (@RheaMoutafis). #Python #JuliaLang #Programming<\/li>\n<li><a href=\"https:\/\/techualization.blogspot.com\/2020\/05\/design-by-contract-with-lean-theorem.html?m=0\">Design by Contract with Lean theorem prover<\/a>. ~ Nam Nguyen. #ITP #LeanProver #Programming<\/li>\n<li><a href=\"https:\/\/www.mikulskibartosz.name\/functional-programming-principles-vs-data-streaming\/\">Data flow &#8211; what functional programming and Unix philosophy can teach us about data streaming<\/a>. ~ Bartosz Mikulski (@mikulskibartosz). #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/marcosh.github.io\/post\/2020\/05\/04\/intervals-and-their-relations.html\">Intervals and their relations<\/a>. ~ Marco Perone (@marcoshuttle). #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2020\/4\/20\/frozen-lake-in-haskell\">Frozen lake in Haskell<\/a>. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming #AI<\/li>\n<li><a href=\"http:\/\/matt.might.net\/articles\/best-programming-languages\/\">Advanced programming languages<\/a>. ~ Matt Might (@mattmight). #Haskell #Scala #SML #OCaml #Scheme #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/books.google.es\/books?id=0dLQDwAAQBAJ&amp;lpg=PP1&amp;hl=es&amp;pg=PP1#v=onepage&amp;q&amp;f=false\">The age of algorithms<\/a>. ~ Serge Abiteboul, Gilles Dowek. #eBook #Algorithms<\/li>\n<li><a href=\"http:\/\/wwwf.imperial.ac.uk\/~buzzard\/xena\/computers2.pdf\">Proving theorems with computers<\/a>. ~ Kevin Buzzard. #ITP #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Forcing.html\">Formalization of forcing in Isabelle\/ZF<\/a>. ~ Emmanuel Gunther, Miguel Pagano, Pedro S\u00e1nchez Terraf. #ITP #IsabelleZF #Logic<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Banach_Steinhaus.html\">Banach-Steinhaus theorem in Isabelle\/HOL<\/a>. ~ Dominique Unruh, Jose Manuel Rodriguez Caballero. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/free.cofree.io\/2020\/05\/06\/string-types\/\">Eat Haskell string types for breakfast<\/a>. ~ Ziyang Liu. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/tech.fretlink.com\/environment-variables-parsing-for-free-applicatives\/\">Environment variables parsing for free (applicatives)<\/a>. ~ Cl\u00e9ment Delafargue. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/iceland_jack.brick.do\/8c0bc94e-ed41-4db5-8de8-422fc800a061\">Monoids as one-object categories, or not?<\/a> ~ @Iceland_jack #Haskell #FunctionalProgramming #CategoryTheory<\/li>\n<li><a href=\"https:\/\/umazalakain.info\/static\/typing-linear-pi.pdf\">\u03c0 with leftovers: a mechanisation in Agda<\/a>. ~ Uma Zalakain, Ornela Dardha. #ITP #Agda<\/li>\n<li><a href=\"http:\/\/chalmersfp.org\/\">The Chalmers online functional programming seminar series<\/a>. #FunctionalProgramming<\/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<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Matrices_for_ODEs.html\">Matrices for ODEs in Isabelle\/HOL<\/a>. ~ Jonathan Julian Huerta y Munive. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.02247\">A linear algebra approach to linear metatheory<\/a>. ~ James Wood, Robert Atkey. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.01018\">Certified semantics for relational programming<\/a>. ~ Dmitry Rozplokhas, Andrey Vyatkin, Dmitry Boulytchev. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.quora.com\/Why-is-Lisp-not-as-popular-as-Python\/answer\/Jan-Meww\">Why is Lisp not as popular as Python?<\/a> ~ Jan Meww (@JanMeww). #Python #CommonLisp #Scheme #Clojure<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.02259\">Learning programs by learning from failures<\/a>. ~ Andrew Cropper, Rolf Morel. #ILP #MachineLearning #LogicProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/KJ8uZiWpomg\">Clean vs. defaulty representations in Prolog<\/a>. ~ Markus Triska (@MarkusTriska). #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/pp.ipd.kit.edu\/uploads\/publikationen\/himmel20bachelorarbeit.pdf\">Diagram chasing in interactive theorem proving<\/a>. ~ Markus Himmel. #BsC_Thesis #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.01917\">Learning selection strategies in Buchberger&#8217;s algorithm<\/a>. ~ Dylan Peifer, Michael Stillman, Daniel Halpern-Leistner. #MachineLearning #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.04022\">On the effect of learned clauses on stochastic local search<\/a>. ~ Jan-Hendrik Lorenz, Florian W\u00f6rz. #ATP #SAT_solvers<\/li>\n<li><a href=\"https:\/\/lasciencepourtous.cafe-sciences.org\/articles\/lintelligence-artificielle-et-lapprentissage-profond\/\">L\u2019intelligence artificielle et l\u2019apprentissage profond<\/a>. ~ Benjamin Bradu. #AI #DeepLearning<\/li>\n<li><a href=\"https:\/\/kowainik.github.io\/posts\/extensions\">Extensions<\/a>. ~ Veronika Romashkina (@vrom911). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/wespiser.com\/posts\/2020-05-06-IxMonad.html\">Indexed monads: examples and discussion<\/a>. ~ Adam Wespiser (@wespiser). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.ias.edu\/ideas\/2014\/voevodsky-origins\">The origins and motivations of univalent foundations (A personal mission to develop computer proof verification to avoid mathematical mistakes)<\/a>. ~ Vladimir Voevodsky (2014). #Logic #Math #ITP via @AngelikiKoutso1<\/li>\n<li><a href=\"https:\/\/www.iro.umontreal.ca\/~monnier\/hopl-4-emacs-lisp.pdf\">Evolution of Emacs Lisp<\/a>. ~ Stefan Monnier et als. #Emacs #Lisp<\/li>\n<li><a href=\"https:\/\/medium.com\/better-programming\/15-reasons-why-i-use-emacs-with-gifs-5b03c6608b61\">15 reasons why I use Emacs, with GIFs<\/a>. ~ Dominik Tarnowski. #Emacs<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2020\/4\/27\/blackjack-following-the-patterns\">Blackjack: Following the patterns<\/a>. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming #AI<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Recursion-Addition.html\">Recursion theorem in ZF<\/a>. ~ Georgy Dunaev. #ITP #IsabelleZF #Logic #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/YS7DWacP55U\">Haskell: Function application vs fmap vs sequential application vs bind<\/a>. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.47deg.com\/blog\/science-behind-functional-programming\/\">The science behind functional programming<\/a>. ~ Rafa Paradela. #CategoryTheory #FuncionalProgramming #Kotlin<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Irrational_Series_Erdos_Straus.html\">Irrationality criteria for series by Erd\u0151s and Straus in Isabelle\/HOL<\/a>. ~ Angeliki Koutsoukou-Argyraki, Wenda Li. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/ZuNMo136QqI\">A quick look at impredicativity<\/a>. ~ Simon Peyton Jones. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.07059\">Proof-relevant category theory in Agda<\/a>. ~ Jason Z.S. Hu, Jacques Carette. #ITP #Agda #CategoryTheory<\/li>\n<li><a href=\"https:\/\/janet-lang.org\">Janet: a functional and imperative programming language<\/a>. #FunctionalProgramming #JanetLang<\/li>\n<li><a href=\"https:\/\/youtu.be\/B5RRq1BJHEE\">MathZero, the classification problem, and set-theoretic type theory<\/a>. ~ David McAllester. #MachineLearning #TypeTheory<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Knuth_Bendix_Order.htmla\">A formalization of Knuth\u2013Bendix orders in Isabelle\/HOL<\/a>. ~ Christian Sternagel, Ren\u00e9 Thiemann. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/wwwf.imperial.ac.uk\/~buzzard\/xena\/pdfs\/formalise_UG_maths.pdf\">Formalising Mathematics in a theorem prover<\/a>. ~ K. Buzzard. #ITP #Math<\/li>\n<li><a href=\"https:\/\/jesseevers.com\/haskell-types\/\">Types vs. datatypes vs. typeclasses in Haskell<\/a>. ~ Jesse Evers (@_jlevers). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.vstill.eu\/publications\/2020\/hsExprTest.pdf\">Automatic test generationfor Haskell programming assignments<\/a>. ~ Vladim\u00edr \u0160till. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/videos-de-las-clases-de-algoritmica-con-haskell\/\">V\u00eddeos de las clases de algor\u00edtmica con Haskell<\/a>. #Haskell #Programaci\u00f3nFuncional #Algor\u00edtmica #I1M2019<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/videos-de-las-clases-de-razonamiento-automatico-con-isabelle-hol\/%20\">V\u00eddeos de las clases de razonamiento autom\u00e1tico con Isabelle\/HOL<\/a>. #L\u00f3gica #DAO #IsabelleHOL #LMF2019<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/2005.04722.pdf\">Dynamic IFC theorems for free!<\/a> ~ Maximilian Algehed, Jean-Philippe Bernardy, C\u0103t\u0103lin Hrit. #ITP #Agda #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/iris-project.org\/pdfs\/2020-actris2-submission.pdf\">Machine-checked semantic session typing<\/a>. ~ Jonas Kastberg Hinrichsen et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.05512\">MathZero, the classification problem, and set-theoretic type theory<\/a>. ~ David McAllester. #MachineLearning #TypeTheory<\/li>\n<li><a href=\"https:\/\/github.com\/avesus\/ATP_Proofs\">Interesting ATP proofs<\/a>. #ATP #Logic #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/ya5SAmx-7QI\">Automating Mathematics? ~ Siddhartha Gadgil<\/a>. #ITP #Math<\/li>\n<li><a href=\"http:\/\/siddhartha-gadgil.github.io\/ProvingGround\/index.html\">ProvingGround: Automated Theorem proving by learning<\/a>. ~ Siddhartha Gadgil. #ATP #Math #HoTT<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/pdfs\/purely-functional-data-structures-slides.pdf\">Purely functional data structures and monoids<\/a>. ~ Donnacha Ois\u00edn Kidney (@oisdk). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2020\/5\/4\/frozen-lake-with-q-learning\">Frozen lake with Q-learning!<\/a> ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming #MachineLearning<\/li>\n<li><a href=\"https:\/\/sites.google.com\/view\/berkeleyleanseminar\/home\">2020 Berkeley Lean Seminar<\/a>. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/youtu.be\/dfZ94N0hS4I\">Backtracking generators for random testing<\/a>. ~ Benjamin Pierce. #ITP #Coq #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/adam.chlipala.net\/papers\/KoikaPLDI20\/KoikaPLDI20.pdf\">The essence of Bluespec (A core language for rule-based hardware design)<\/a>. Thomas Bourgeat et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.09452\">PubSub implementation in Haskell with formal verification in Coq<\/a>. ~ Boro Sitnikovski, Biljana Stojcevska, Lidija Goracinova-Ilieva, Irena Stojmenovska. #Haskell #FuncionalProgramming #ITP #Coq<\/li>\n<li><a href=\"https:\/\/youtu.be\/eZ9FpG8May8\">Why functors and applicatives compose but monads don&#8217;t<\/a>. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.dropbox.com\/s\/1j828vngpm0yhja\/fp-berlin-2020.pdf?dl=0\">Why functors and applicatives compose but monads don&#8217;t<\/a>. [Slides]. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2020\/05\/19\/competitive-programming-in-haskell-sorting-tree-shapes\/\">Competitive programming in Haskell: sorting tree shapes<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/towardsdatascience.com\/galois-theory-for-non-mathematicians-3bc08cd40c4a\">Galois theory for non-mathematicians<\/a>. ~ Mikael Davidsson. #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Stateful_Protocol_Composition_and_Typing.html\">Stateful protocol composition and typing in Isabelle\/HOL<\/a>. ~ Andreas V. Hess, Sebastian M\u00f6dersheim, Achim D. Brucker. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/emarzion.github.io\/Cantor-Thm\/\">Visualizing Cantor&#8217;s theorem on dense linear orders using Coq<\/a>. ~ Evan Marzion. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.twitch.tv\/videos\/627659597\">The complex numbers are a ring<\/a>. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/fpcomplete.com\/how-to-build-with-stack\/\">How to build with Stack<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fpcomplete.com\/how-to-script-with-stack\/\">How to script with Stack<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fpcomplete.com\/how-to-play-with-stack\/\">How to play with Stack<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fpcomplete.com\/profiling-and-performance\/\">Profiling and performance<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fpcomplete.com\/monad-transformers\/\">Monad transformers<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fpcomplete.com\/recommended-haskell-libraries\/\">Recommended Haskell libraries<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fpcomplete.com\/string-types\/\">String types<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fpcomplete.com\/synonyms-in-base\/\">Synonyms in base<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fpcomplete.com\/lenses\/\">Lenses<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fpcomplete.com\/safe-exception-handling\/\">Safe exception handling<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fpcomplete.com\/data-types\/\">Data types<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fpcomplete.com\/data-structures\/\">Data structures<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fpcomplete.com\/common-typeclasses\/\">Common typeclasses<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fpcomplete.com\/applied-haskell-101\/\">Applied Haskell 101 course<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fpcomplete.com\/crash-course-to-applicative-syntax\/\">Crash course to applicative syntax<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fpcomplete.com\/all-about-strictness\/\">All about strictness<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.youtube.com\/playlist?list=PLA66mD-6yK8yjlJCI0Ay2f2IvvmB9Ktga\">European Lisp Symposium 2020 videos<\/a>. #Lisp #Programming<\/li>\n<li><a href=\"https:\/\/github.com\/junjihashimoto\/sixel\">SIXEL Library for Haskell: displaying images on ghci<\/a>. ~ Junji Hashimoto. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/anthony.noided.media\/blog\/haskell\/programming\/2020\/05\/14\/haskell-errors.html\">Error messages in Haskell, and how to improve them<\/a>. ~ Anthony Super. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/@fommil\/simple-haskell-is-best-haskell-6a1ea59c73b\">Simple Haskell is best Haskell<\/a>. ~ Sam Halliday. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2020\/05\/22\/competitive-programming-in-haskell-building-unordered-trees\/\">Competitive programming in Haskell: building unordered trees<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/books.google.es\/books?id=zz9wDBjsqlAC&amp;lpg=PP1&amp;hl=es&amp;pg=PP\">Sets, logic and maths for computing<\/a>. ~ David Makinson.1#v=onepage&amp;q&amp;f=false #eBook #Logic #Math #CompSci<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.08396\">A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper<\/a>. ~ Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger. #FuncionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/mathematics_in_lean\/\">Mathematics in Lean<\/a>. ~ Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, Patrick Massot. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/maxfieldchen.com\/posts\/2020-05-23-Dynamically-Flunking-Code-Interview-Haskell.html\">Dynamically flunking the coding interview (A gentle introduction to functional dynamic programming)<\/a>. ~ Maxfield Chen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2020\/05\/23\/the-complex-number-game\/\">The complex number game<\/a>. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/teh.id.au\/posts\/2017\/03\/13\/accumulating-errors\/\">Accumulating independent errors<\/a>. ~ Tim Humphries (@thumphriees). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/handwiki.org\/wiki\/Start\">HandWiki: Online Encyclopedia of Science and Computing<\/a>.<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.08856\">How to generate random lambda terms?<\/a> ~ Maciej Bendkowski. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/kwarc.info\/people\/mkohlhase\/papers\/icms20-glf-jupyter.pdf\">Prototyping controlled mathematical languages in Jupyter notebooks<\/a>. ~ Jan Frederik Schaefer, Kai Amann, Michael Kohlhase. #MKM<\/li>\n<li><a href=\"https:\/\/hal-lirmm.ccsd.cnrs.fr\/lirmm-02611153\/document\">Toward the formal verification of HILECOP: Formalization and implementation of synchronously executed Petri nets<\/a>. ~ Vincent Iampietro, David Andreu, David Delahaye. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.diva-portal.org\/smash\/get\/diva2:1431287\/FULLTEXT01.pdf\">A proof and formalization of the initiality conjecture of dependent type theory<\/a>. ~ Menno de Boer. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.11023\">Symbolic reasoning about quantum circuits in Coq<\/a>. ~ Wenjun Shi, Qinxiang Cao, Yuxin Deng, Hanru Jiang, Yuan Feng. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/splintah.gitlab.io\/posts\/2020-05-24-Simply-typed-lambda.html\">Simply typed lambda calculus<\/a>. ~ Splinter Suidman. #Haskell #FuncionalProgramming #LambdaCalculus<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Smith_Normal_Form.html\">A verified algorithm for computing the Smith normal form of a matrix<\/a>. ~ Jose Divas\u00f3n. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.12876\">A survey of languages for formalizing mathematics<\/a>. ~ Cezary Kaliszyk, Florian Rabe. #Logic #Math #ITP #MKM<\/li>\n<li><a href=\"https:\/\/jonascarpay.com\/posts\/2020-05-26-solver.html\">Monoidal puzzle solving<\/a>. ~ Jonas Carpay (@jonascarpay) #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/_3cYAsJClEg\">Cap\u00edtulo 1 de &#8220;Paradojas del nihilismo: La Academia&#8221;: Desilusi\u00f3n<\/a>. #Universidad<\/li>\n<li><a href=\"https:\/\/medium.com\/syncedreview\/new-latex-css-library-enables-websites-to-look-like-latex-docs-690a36e30f4b\">New LaTeX.css library enables websites to look like LaTeX docs<\/a>. #LaTeX #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1910.12320\">Formalising perfectoid spaces<\/a>. ~ Kevin Buzzard, Johan Commelin, Patrick Massot. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/theorylunch.wordpress.com\/2013\/12\/03\/natural-numbers-with-addition-form-a-monoid\/\">Natural numbers with addition form a monoid<\/a>. ~ James Chapman. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/assets.amazon.science\/d0\/de\/cbec0b4547e3ae7ff077f8aa978f\/code-level-model-checking-in-thesoftware-development-workflow.pdf\">Code-level model checking in the software development workflow<\/a>. ~ Nathan Chong et als. #FormalVerification #ModelChecking<\/li>\n<li><a href=\"https:\/\/www.amazon.science\/blog\/how-to-integrate-formal-proofs-into-software-development\">How to integrate formal proofs into software development<\/a>. ~ Daniel Schwartz-Narbonne. #FormalVerification<\/li>\n<li><a href=\"https:\/\/gist.github.com\/Kazark\/06acabbd25817ac9efc7fbe0493f23ff\">Curry-Howard tutorial in literate Haskell<\/a>. ~ Keith Pinson. #Haskell #FunctionalProgramming #Logic<\/li>\n<li><a href=\"https:\/\/www.stephendiehl.com\/posts\/marketing.html\">On marketing Haskell<\/a>. ~ Stephen Diehl (@smdiehl) #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/@cdsmithus\/a-calculator-with-reflex-and-codeworld-8f154b776f02\">A calculator with Reflex and CodeWorld<\/a>. ~ Chris Smith (@cdsmithus). #Haskell #CodeWorld<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2020\/05\/30\/competitive-programming-in-haskell-permutations\/\">Competitive programming in Haskell: permutations<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/n7QETok5hYI\">Economic argument for functional programming<\/a>. ~ Michael Snoyman (@snoyberg). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.snoyman.com\/reveal\/economic-argument-functional-programming\">Economic argument for functional programming [Slides<\/a>]. ~ Michael Snoyman (@snoyberg). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.11821\">A proof assistant based formalisation of core Erlang<\/a>. ~ P\u00e9ter Bereczky, D\u00e1niel Horp\u00e1csi, Simon Thompson. #ITP #Coq #Erlang<\/li>\n<li><a href=\"https:\/\/www21.in.tum.de\/~nipkow\/pubs\/ijcar20-closest.pdf\">Verification of closest pair of points algorithms<\/a>. ~ Martin Rau, Tobias Nipkow. #ITP #IsabelleHOL #Algorithms<\/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 mayo 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\/7210"}],"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=7210"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7210\/revisions"}],"predecessor-version":[{"id":7211,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7210\/revisions\/7211"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7210"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7210"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7210"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}