{"id":7599,"date":"2021-03-01T19:21:40","date_gmt":"2021-03-01T18:21:40","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7599"},"modified":"2021-08-30T19:22:47","modified_gmt":"2021-08-30T17:22:47","slug":"resumen-de-lecturas-compartidas-durante-febrero-de-2021","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-febrero-de-2021\/","title":{"rendered":"Resumen de lecturas compartidas durante febrero de 2021"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante febrero de 2021, en <a href=\"https:\/\/twitter.com\/Jose_A_Alonso\">Twitter<\/a> fundamentalmente sobre programaci\u00f3n funcional y demostraci\u00f3n asistida por ordenador.<\/p>\n<p>Las lecturas est\u00e1n ordenadas seg\u00fan su fecha de publicaci\u00f3n en <a href=\"https:\/\/twitter.com\/Jose_A_Alonso\">Twitter<\/a>.<\/p>\n<p>Al final de cada art\u00edculo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.<\/p>\n<p>Una recopilaci\u00f3n de todas las lecturas compartidas se encuentra en <a href=\"https:\/\/github.com\/jaalonso\/Lecturas_GLC\">GitHub<\/a>.<br \/>\n<!--more--><\/p>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/cs.nyu.edu\/faculty\/davise\/papers\/proof.pdf\">Proof verification technology and elementary physics<\/a>. ~ Ernest Davis. #FormalVerification #Physics<\/li>\n<li><a href=\"http:\/\/h2.jaguarpaw.co.uk\/posts\/how-i-use-dante\/\">How I use Dante<\/a>. #Haskell #FunctionalProgramming #Emacs<\/li>\n<li><a href=\"https:\/\/www.scitepress.org\/Papers\/2020\/94644\/94644.pdf\">Computational logic in the first semester of computer science: An experience report<\/a>. ~ David M. Cerna et als. #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.10698v1\">Certifying choreography compilation<\/a>. ~ Lu\u00eds Cruz-Filipe, Fabrizio Montesi, Marco Peressotti. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2021\/02\/25\/formalising-mathematics-workshop-6-limits\/\">Formalising mathematics: workshop 6 (limits)<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/mediatum.ub.tum.de\/doc\/1596550\/1596550.pdf\">A verified imperative implementation of B-trees (in Isabelle\/HOL)<\/a>. ~ Niels M\u00fcndle. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/kowainik.github.io\/posts\/totality\">Totality<\/a>. ~ Veronika Romashkina, Dmitrii Kovanikov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.ch3m4.org\/2021\/02\/15\/evaluacion-perezosa-en-python-parte-4\/\">Evaluaci\u00f3n perezosa en Python. Parte 4: Evaluaci\u00f3n perezosa avanzada<\/a>. ~ Chema Cort\u00e9s. #Python #Programaci\u00f3n<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Formal_Puiseux_Series.html\">Formal Puiseux series (in Isabelle\/HOL)<\/a>. ~ Manuel Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/blog.drewolson.org\/purescript-and-haskell\">PureScript and Haskell<\/a>. ~ Drew Olson. #Haskell #PureScript #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/math.andrej.com\/2021\/02\/22\/burali-forti-in-hott-uf\/\">The Burali-Forti argument in HoTT\/UF<\/a>. ~ Martin Escardo. #Logic #Math #HoTT<\/li>\n<li><a href=\"https:\/\/youtu.be\/YqAu1hdd4Z4\">Rerecorded introduction to the Algebra of Programming research group<\/a>. ~ Jeremy Gibbons. #CompSci #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/student.cs.uwaterloo.ca\/~cs442\/W21\/notes\/\">Course: Principles of Programming Languages<\/a>. ~ Gregor Richards. #Programming #Haskell #Prolog #Pascal #Smalltalk #Erlang #C<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/magazines\/2021\/3\/250711-knowledge-graphs\/fulltext\">Knowledge graphs<\/a>. ~ Claudio Gutierrez, Juan F. Sequeda. #AI #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/magazines\/2021\/3\/250710-the-decline-of-computers-as-a-general-purpose-technology\/fulltext\">The decline of computers as a general purpose technology<\/a>. ~ Neil C. Thompson, Svenja Spanuth. #CompSci<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/magazines\/2021\/3\/250705-50-years-of-pascal\/fulltext\">50 years of Pascal<\/a>. ~ Niklaus Wirth. #Pascal #Programming #CompSci<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.10556v1\">Inductive logic programming at 30<\/a>. ~ Andrew Cropper, Sebastijan Duman\u010di\u0107, Richard Evans, Stephen H. Muggleton. #ILP #LogicProgramming #MachineLearning<\/li>\n<li><a href=\"https:\/\/link.medium.com\/LjTU9hQL3db\">A formal proof of safegcd bounds<\/a>. ~ Russell O\u2019Connor, Andrew Poelstra. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.07636\">Formalized Haar measure<\/a>. ~ Floris van Doorn. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-03142192\/document\">A variant of Wagner\u2019s theorem based on combinatorial hypermaps<\/a>. ~ Christian Doczkal. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/eprint.iacr.org\/2021\/147.pdf\">IPDL: A simple framework for formally verifying distributed cryptographic protocols<\/a>. ~ Greg Morrisett, Elaine Shi, Kristina Sojakova, Xiong Fan, Joshua Gancher. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/angg.twu.net\/LATEX\/2021excuse.pdf\">Category theory as an excuse to learn type theory<\/a>. ~ Eduardo Ochs, Selana Ochs. #CategoryTheory #TypeTheory<\/li>\n<li><a href=\"https:\/\/youtu.be\/ipIY7MWhk8s\">Introducci\u00f3n al sistema de tipos en Haskell<\/a>. ~ Manuel Soto. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/ipIY7MWhk8s\">Type classes: de aprendiz a maestro<\/a>. ~ Alejandro Serrano. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.09125v1\">Formalizing groups in type theory<\/a>. ~ Farida Kachapova. #Logic #Math #ITP<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2021\/02\/18\/formalising-mathematics-workshop-5-filters\">Formalising mathematics: workshop 5 (filters)<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/en.wikipedia.org\/wiki\/Filter_(mathematics)\">Filter (mathematics)<\/a>. ~ Wikipedia. #Math<\/li>\n<li><a href=\"https:\/\/en.wikipedia.org\/wiki\/Filters_in_topology\">Filters in topology<\/a>. ~ Wikipedia. #Math<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/set-theory\/\">Set theory (in &#8220;The Stanford Encyclopedia of Philosophy&#8221;)<\/a>. ~ Joan Bagaria. #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.icrea.cat\/security\/files\/researchers\/researcher-sections\/pcm_set_theory_long_revised.pdf\">Set theory<\/a>. ~ Joan Bagaria. #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.icrea.cat\/security\/files\/researchers\/researcher-sections\/mst2019-20.pdf\">Models of set theory<\/a>. ~ Joan Bagaria. #Logic #Math #Set_theory<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/boolalg-math\/\">The mathematics of boolean algebra (in &#8220;The Stanford Encyclopedia of Philosophy&#8221;)<\/a>. ~ J. Donald Monk. #Logic #Math<\/li>\n<li><a href=\"https:\/\/alistairb.dev\/reflections-on-haskell-for-startup\/\">Reflections on using Haskell for my startup<\/a>. ~ Alistair Burrowes. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.08595v1\">Formalizing relations in type theory<\/a>. ~ Farida Kachapova. #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.lri.fr\/~wolff\/teach-material\/2020-2021\/M2-CSMR\/index.html\">Course: Interactive theorem proving and applications<\/a>. ~ Burkhart Wolff. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/algebra\/\">#SEP: Algebra (in &#8220;The Stanford Encyclopedia of Philosophy&#8221;)<\/a>. ~ Vaughan Pratt. #Math<\/li>\n<li><a href=\"https:\/\/blog.ch3m4.org\/2021\/02\/14\/evaluacion-perezosa-en-python-parte-3\/\">Evaluaci\u00f3n perezosa en Python<\/a>. Parte 3: Cach\u00e9s y memoizaci\u00f3n. ~ Chema Cort\u00e9s. #Python #Programaci\u00f3n<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.05242\">Patterns, predictions, and actions: A story about machine learning<\/a>. ~ Moritz Hardt, Benjamin Recht. #eBook #MachineLearning<\/li>\n<li><a href=\"http:\/\/mathcentral.uregina.ca\/RR\/database\/RR.09.95\/grzesina1.html\">A geometric view of the square root algorithm<\/a>. ~ A. Grzesina. #Math #Algorithms<\/li>\n<li><a href=\"https:\/\/ieeexplore.ieee.org\/stamp\/stamp.jsp?arnumber=9348915\">Study of Isabelle\/HOL on formal algorithm analysis and code generation<\/a>. ~ Haitao Wang, Lihua Song. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/Christoph-Benzmueller\/publication\/349061647_Cantor's_Theorem_without_Reductio_Ad_Absurdum\/links\/601e41a592851c4ed54fa746\/Cantors-Theorem-without-Reductio-Ad-Absurdum.pdf\">Cantor\u2019s theorem without reductio ad absurdum<\/a>. ~ Christoph Benzm\u00fcller, David Fuenmayor. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/fallacies\/\">#SEP: Fallacies<\/a>. ~ Hans Hansen. #Logic<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/algebra-logic-tradition\/\">#SEP: The algebra of logic tradition<\/a>. ~ Stanley Burris, Javier Legris. #Logic<\/li>\n<li><a href=\"https:\/\/kaygun.tumblr.com\/post\/643010859143151616\/kruskals-algorithm-implemented-in-clojure\">Kruskal\u2019s algorithm implemented in Clojure<\/a>. ~ Atabey Kaygun. #Clojure #Algorithms<\/li>\n<li><a href=\"https:\/\/kaygun.tumblr.com\/post\/643088741013012480\/kruskals-algorithm-in-common-lisp\">Kruskal\u2019s algorithm in Common Lisp<\/a>. ~ Atabey Kaygun. #CommonLisp #Algorithms<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/Christoph-Benzmueller\/publication\/349027173_Value-oriented_Legal_Argumentation_in_IsabelleHOL\/links\/601b90b5299bf1cc26a00e9a\/Value-oriented-Legal-Argumentation-in-Isabelle-HOL.pdf\">Value-oriented legal argumentation in Isabelle\/HOL<\/a>. ~ Christoph Benzm\u00fcller, David Fuenmayor. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-03136002\/document\">Unsolvability of the quintic formalized in dependent type theory<\/a>. ~ Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/tel.archives-ouvertes.fr\/tel-03107626\/document\/\">Machine-checked computer-aided mathematics<\/a>. ~ Assia Mahboubi. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/academic.oup.com\/logcom\/advance-article\/doi\/10.1093\/logcom\/exab006\/6129486\">A study of continuous vector representations for theorem proving<\/a>. ~ Stanis\u0141aw Purga\u0141, Julian Parsert, Cezary Kaliszyk. #ATP #MachineLearning<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/mathematician-solves-computer-science-conjecture-in-two-pages-20190725\/\">Decades-old computer science conjecture solved in two pages<\/a>. ~ Erica Klarreich. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/72141fdc94feec6f394b95c9310687f517bb4d02\/src\/combinatorics\/hall.lean\">Hall&#8217;s Marriage Theorem in Lean<\/a>. ~ Alena Gusakov, Bhavik Mehta, Kyle Miller. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/2f566202f1bbefee115b5b45b48a7127133309c7\/src\/data\/real\/liouville.lean\">Liouville&#8217;s theorem in Lean<\/a>. ~ Jujian Zhang. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/983cb905e2468a820d833263bd537686b549267a\/archive\/imo\/imo1987_q1.lean\">Formalization in Lean of IMO (International Mathematical Olympiads) 1987, Q1<\/a>. ~ Yury Kudryashov. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.05945\">A formal proof of modal completeness for provability logic<\/a>. ~ Marco Maggesi, Cosimo Perini Brogi. #ITP #HOL_Light #Logic<\/li>\n<li><a href=\"https:\/\/youtube.com\/playlist?list=PLguYJK7ydFE4aS8fq4D6DqjF6qsysxTnx\">HaskellRank: HackerRank in Haskell<\/a>. ~ @tsoding. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.ch3m4.org\/2021\/02\/09\/evaluacion-perezosa-en-python-parte-2\/\">Evaluaci\u00f3n perezosa en Python &#8211; Parte 2: Secuencias infinitas<\/a>. ~ Chema Cort\u00e9s. #Python #Programming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Laws_of_Large_Numbers.html\">The laws of large numbers (in Isabelle\/HOL)<\/a>. ~ Manuel Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2021\/02\/10\/formalising-mathematics-workshop-4\/\">Formalising mathematics: workshop 4 (topology)<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.05547\">Learning equational theorem proving<\/a>. ~ Jelle Piepenbrock, Tom Heskes, Mikol\u00e1\u0161 Janota, Josef Urban. #ATP #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.05616\">An algebra of properties of binary relations<\/a>. ~ Jochen Burghardt. #Logic #Math #ATP #Eprover<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/fdbd4bffdc00b53b0b337ff308378a448b069f7e\/archive\/imo\/imo2013_q1.lean\">IMO 2013 Q1 in Lean<\/a>. ~ David Renshaw. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.02679\">Certifying differential equation solutions from computer algebra systems in Isabelle\/HOL<\/a>. ~ Thomas Hickman, Christian Pardillo Laursen, Simon Foster. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.03529\">Vampire with a brain is a good ITP hammer<\/a>. ~ Martin Suda. #Vampire #ATP #ITP #MachineLearning<\/li>\n<li><a href=\"https:\/\/users.utcluj.ro\/~agroza\/puzzles\/maloga\/preface.html\">Modelling puzzles in First Order Logic<\/a>. ~ Adrian Groza. #Logic #ATP #Prover9<\/li>\n<li><a href=\"https:\/\/blog.ch3m4.org\/2021\/02\/08\/evaluacion-perezosa-en-python-parte-1\/\">Evaluaci\u00f3n perezosa en Python<\/a>. Parte 1: Introducci\u00f3n a la evaluaci\u00f3n perezosa. ~ Chema Cort\u00e9s. #Python #Programming<\/li>\n<li><a href=\"https:\/\/www.galoisrepresentations.com\/2019\/07\/17\/the-ramanujan-machine-is-an-intellectual-fraud\/\">The Ramanujan Machine is an intellectual fraud<\/a>. #AI #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.03003\">A verified decision procedure for univariate real arithmetic with the BKR algorithm<\/a>. ~ Katherine Cordwell, Yong Kiam Tan, Andr\u00e9 Platzer. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.02901\">A formal proof of the independence of the continuum hypothesis<\/a>. ~ Jesse Michael Han, Floris van Doorn. #ITP #LeanProver #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.philipzucker.com\/javascript-automated-proving\/\">Automated propositional sequent proofs in your browser with Tau Prolog<\/a>. Philip Zucker. #ATP #Logic #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/fosdem.org\/2021\/schedule\/event\/open_research_emacs_orgmode\/\">Emacs and org-mode for reproducible research<\/a>. (Organize your research in plain text!). ~ Thibault Lestang. #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/www.hhyu.org\/posts\/literate_config\/\">Writing the Emacs configuration script in org-mode: a simple example of literate programming<\/a>. ~ Hsin-Hao Yu. #Emacs<\/li>\n<li><a href=\"https:\/\/www.haskellforall.com\/2021\/02\/folds-are-constructor-substitution.html\">Folds are constructor substitution<\/a>. ~ Gabriel Gonzalez. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.00378\">Model-based testing of networked applications<\/a>. ~ Yishuai Li, Benjamin C. Pierce, Steve Zdancewic. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.01167\">Verifying the Hashgraph consensus algorithm<\/a>. ~ Karl Crary. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.nature.com\/articles\/d41586-021-00304-8\">AI maths whiz creates tough new problems for humans to solve<\/a>. ~ Davide Castelvecchi. #AI #Math #ITP<\/li>\n<li><a href=\"https:\/\/www.ramanujanmachine.com\/\">The Ramanujan Machine (an algorithmic approach to discover new mathematical conjectures)<\/a>. #AI #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.00205\">The Ramanujan Machine: automatically generated conjectures on fundamental constants<\/a>. ~ Gal Raayoni, Shahar Gottlieb, George Pisha, Yoav Harris, Yahel Manor, Uri Mendlovic, Doron Haviv, Yaron Hadad, Ido Kaminer. #AI #Math<\/li>\n<li><a href=\"https:\/\/takenobu-hs.github.io\/downloads\/haskell_ghc_reading_guide.pdf\">GHC reading guide (Exploring entrances and mental models to the source code)<\/a>. ~ Takenobu Tani. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cscx.org\/\">Computer Science by Example<\/a>. #CompSci #Programming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.02627\">Formalising a Turing-complete choreographic language in Coq<\/a>. ~ Lu\u00eds Cruz-Filipe, Fabrizio Montesi, Marco Peressotti. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.02600\">A formalization of Dedekind domains and class groups of global fields<\/a>. ~ Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, Filippo A. E. Nuccio Mortarino Majno di Capriglio. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/alexey.kuleshevi.ch\/blog\/2021\/01\/29\/random-interface\/\">New random interface<\/a>. ~ Alexey Kuleshevich. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2021\/02\/04\/formalising-mathematics-workshop-3\/\">Formalising mathematics: Workshop 3 (Limits of sequences)<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2018\/08\/04\/what-is-a-filter-how-some-computer-scientists-think-about-limits\/\">What is a filter? How some computer scientists think about limits<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2018\/08\/05\/what-is-a-uniform-space-how-some-computer-scientists-think-about-completions\/\">What is a uniform space? How some computer scientists think about completions<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/Marco_Bonatto\/publication\/348662657_Superconnected_left_quasigroups_and_involutory_quandles\/links\/6009d8bea6fdccdcb86fc158\/Superconnected-left-quasigroups-and-involutory-quandles.pdf\">Superconnected left quasigroups and involutory quandles<\/a>. ~ Marco Bonatto. #ATP #Prover9 #Math<\/li>\n<li><a href=\"https:\/\/zacwood.me\/posts\/haskell-type-application\/\">Haskell&#8217;s @ symbol &#8211; Type application<\/a>. ~ Zac Wood. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/jonascarpay.com\/posts\/2021-01-28-haskell-project-template.html\">The working programmer\u2019s guide to setting up Haskell projects<\/a>. ~ Jonas Carpay. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.microsiervos.com\/archivo\/seguridad\/cifrado-monjes-cistercienses.html\">El cifrado de los monjes cistercienses: de 0000 a 9999 con \u00abs\u00edmbolos raros\u00bb<\/a>. ~ @Alvy. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/browser_info\/current\/AFP\/IsaGeoCoq\/document.pdf\">Tarski&#8217;s parallel postulate implies the 5th postulate of Euclid, the postulate of Playfair and the original parallel postulate of Euclid<\/a>. ~ Roland Coghetto. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Blue_Eyes.html\">Solution to the xkcd Blue Eyes puzzle (in Isabelle\/HOL)<\/a>. ~ Jakub K\u0105dzio\u0142ka. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/thma.github.io\/posts\/2021-01-30-How-QuickCheck-destroyed-my-favourite-theory.html\">Proving me wrong (How QuickCheck destroyed my favourite theory)<\/a>. ~ Thomas Mahler. #Haskell #FunctionalProgramming #QuickCheck<\/li>\n<li><a href=\"https:\/\/people.mpi-sws.org\/~beta\/papers\/jlamp20.pdf\">Verification of dynamic bisimulation theorems in Coq<\/a>. ~ R Fervari, F Trucco, B Ziliani. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2101.11320v1\">Tutorial on implementing Hoare logic for imperative programs in Haskell<\/a>. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2101.11421v1\">Deriving monadic quicksort (Declarative Pearl)<\/a>. ~ Shin-Cheng Mu, Tsung-Ju Chiang. #Haskell #FunctionalProgramming<\/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 febrero de 2021, en Twitter fundamentalmente sobre programaci\u00f3n funcional y demostraci\u00f3n asistida por ordenador. Las lecturas est\u00e1n ordenadas seg\u00fan su fecha de publicaci\u00f3n en Twitter. Al final de cada art\u00edculo se encuentran etiquetas relativas a los sistemas que usa o a su contenido. Una recopilaci\u00f3n de&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[6],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7599"}],"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=7599"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7599\/revisions"}],"predecessor-version":[{"id":7600,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7599\/revisions\/7600"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7599"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7599"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7599"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}