{"id":7595,"date":"2021-01-01T19:11:50","date_gmt":"2021-01-01T18:11:50","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7595"},"modified":"2021-08-30T19:13:00","modified_gmt":"2021-08-30T17:13:00","slug":"resumen-de-lecturas-compartidas-durante-diciembre-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-diciembre-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas durante diciembre de 2020"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante diciembre 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=\"https:\/\/www.seas.upenn.edu\/~lucsil\/papers\/dmf.pdf\">Dijkstra monads forever: termination-sensitive specifications for interaction trees<\/a>. ~ Lucas Silver, Steve Zdancewic. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~myreen\/cpp2021-bootstrap-myreen.pdf\">A minimalistic verified bootstrapped compiler (Proof Pearl)<\/a>. ~ Magnus O. Myreen. #ITP #HOL4<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/advent-of-code-2020.html\">Advent of Code 2020: Haskell solution reflections for all 25 days<\/a>. ~ Justin Le. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/leanpub.com\/haskell-cookbook\/read\">Haskell tutorial and cookbook, Second edition<\/a>. ~ Mark Watson. #eBook #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/mark-watson\/haskell_tutorial_cookbook_examples\">Examples for &#8220;Haskell tutorial and cookbook, Second edition&#8221;<\/a>. ~ Mark Watson. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/onurgumus.github.io\/2022\/12\/26\/Functional-Programming.html\">Functional programming: Enemy of the state<\/a>. ~ Onur G\u00fcm\u00fc\u015f. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dev.to\/kakkun61\/the-simplest-monadfail-instance-2i4e\">The simplest MonadFail instance<\/a>. ~ Kazuki Okamoto. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/ro-che.info\/articles\/2020-12-29-statet-vs-ioref\">StateT vs IORef: a benchmark<\/a>. ~ Roman Cheplyaka. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/347964119_Irrationality_and_Transcendence_Criteria_for_Infinite_Series_in_IsabelleHOL\">Irrationality and transcendence criteria for infinite series in Isabelle\/HOL<\/a>. ~ Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence Paulson. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/notes.abhinavsarkar.net\/2020\/aoc-learnings\">Learnings from solving Advent of Code 2020 in Haskell<\/a>. ~ Abhinav Sarkar. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/nauths.fr\/en\/2020\/12\/27\/haskell-type-level-shenanigans.html\">Haskell type-level functions shenanigans (An introduction to some useful language extensions)<\/a>. ~ Antoine Leblanc. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dev.to\/kakkun61\/ephemeral-purely-functional-data-structure-and-linear-type-489j\">Ephemeral purely functional data structure and linear type<\/a>. ~ Kazuki Okamoto. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/kremer.cpsc.ucalgary.ca\/courses\/seng403\/W2013\/papers\/11ProgrammingLanguages.pdf\">Programming language families (Procedural, object oriented, logic, and functional languages)<\/a>. ~ Jobelle Firme, Nicolas Valera, Yunus Canemre, Stephen Burchill, Beenish Khurshid. #Programming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/browser_info\/current\/AFP\/Delta_System_Lemma\/document.pdf\">Cofinality and the delta system lemma (in Isabelle)<\/a>. ~ Pedro S\u00e1nchez Terraf. #ITP #IsabelleZF #Logic #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/drYFAEzKJOE\">Counting bits with Haskell (The bad and the good way)<\/a>. ~ Flavio Corpa. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cronokirby.com\/posts\/2020\/12\/haskell-in-haskell-3\/\">(Haskell in Haskell) 3: Parsing<\/a>. ~ L\u00fac\u00e1s Meier. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/BQNOjum8YlU\">My first type theory<\/a>. ~ Arved Friedemann. #TypeTheory<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2020-12-27-cayley-trees.html\">Trees indexed by a Cayley Monoid<\/a>. ~ Donnacha Ois\u00edn Kidney. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/lean\/blob\/master\/doc\/faq.md\">Lean prover: Frequently Asked Questions<\/a>. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/blog.ocharles.org.uk\/posts\/2020-12-23-monad-transformers-and-effects-with-backpack.html\">Monad transformers and effects with Backpack<\/a>. ~ Ollie Charles. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/frasertweedale.github.io\/blog-fp\/posts\/2020-12-21-refactoring-type-classes-optics.html\">Refactoring using type classes and optics<\/a>. ~ Fraser Tweedale. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/lucasdicioccio\/santa-wrap\">Santa Wrap<\/a>. ~ Lucas Di Cioccio. #Haskell #FunctionalProgramming #MiniZinc<\/li>\n<li><a href=\"https:\/\/ai.ia.agh.edu.pl\/_media\/pl:dydaktyka:est:essential_thinking_2020-59.pdf\">Essential thinking<\/a>. The art of creative thinking for problem solving. ~ Antoni Ligeza. #ProblemSolving #Prolog #CLP #AI<\/li>\n<li><a href=\"https:\/\/leanpub.com\/hy-lisp-python\/read\">A Lisp programmer living in Python-land: The Hy programming language<\/a>. ~ Mark Watson. #eBook #Lisp #Python #Programmig<\/li>\n<li><a href=\"http:\/\/www.math.ac.vn\/training\/images\/TTDaotao\/VinIF\/Laptrinh_TNTrung.pdf\">Python programming and scientific computation<\/a>. ~ Tran Nam Trung. #eBook #Python #Programming<\/li>\n<li><a href=\"https:\/\/republicaweb.es\/podcast\/descubriendo-la-programacion-funcional-elixir-con-erick-navarro\/\">Descubriendo la programaci\u00f3n funcional: Elixir con Erick Navarro<\/a>. #Elixir #Programaci\u00f3nFuncional v\u00eda @republicawebes<\/li>\n<li><a href=\"https:\/\/github.com\/mmasdeu\/euler\">Formalization of Euler summation formula (in Lean)<\/a>. ~ Marc Masdeu. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www21.in.tum.de\/~haslbema\/documents\/Haslbeck_Lammich_LLVM_with_Time.pdf\">For a few dollars more (Verified fine-grained algorithm analysis down to LLVM)<\/a>. ~ Maximilian P. L. Haslbeck, Peter Lammich. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2012.10313\">Towards formally verified compilation of tag-based policy enforcement<\/a>. ~ CHR Chhak, Andrew Tolmach, Sean Anderson. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2007.08017\">\u03bbS: Computable semantics for differentiable programming with higher-order functions and datatypes<\/a>. ~ Benjamin Sherman, Jesse Michel, Michael Carbin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/quantas-year-in-math-and-computer-science-2020-20201223\/\">The year in Math and Computer Science<\/a>. ~ Bill Andrews. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/notxor.nueva-actitud.org\/2020\/12\/23\/slime-lisp-y-emacs.html\">Lisp, Slime y Emacs<\/a>. #Lisp #Emacs<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Topological_Semantics.html\">Topological semantics for paraconsistent and paracomplete logics<\/a>. ~ David Fuenmayor. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.joachim-breitner.de\/blog\/778-Don%E2%80%99t_think%2C_just_defunctionalize\">Don\u2019t think, just defunctionalize<\/a>. ~ Joachim Breitner. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=245\">Sistemas deductivos proposicionales<\/a>. ~ Fernando Sancho. #L\u00f3gica<\/li>\n<li><a href=\"https:\/\/orbit.dtu.dk\/files\/236443090\/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:\/\/www.ps.uni-saarland.de\/Publications\/documents\/KirstRech_2021_The-Generalised.pdf\">The generalised continuum hypothesis implies the axiom of choice in Coq<\/a>. ~ Dominik Kirst, Felix Rech. #ITP #Coq #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/347256855_GeoGebra_Reasoning_Tools_for_Humans_and_for_Automatons\">GeoGebra reasoning tools for humans and for automatons<\/a>. ~ Zolt\u00e1n Kov\u00e1cs, Tom\u00e1s Recio. #ATP #GeoGebra #Math<\/li>\n<li><a href=\"https:\/\/tonyday567.github.io\/posts\/lowercase\/\">Lower case Haskell<\/a>. ~ @tonyday567. #Haskell #FunctionalProgramming #AdventOfHaskell<\/li>\n<li><a href=\"https:\/\/gist.github.com\/ChrisPenner\/1f7b6923448b3396a45d04a2b6b9d066\">Optics by example cheat sheets<\/a>. ~ Chris Penner. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/thma.github.io\/posts\/2020-12-20-reconciling-fp-and-oop-concepts.html\">Reconciling concepts from FP and OOP<\/a>. ~ Thomas Mahler. #Haskell #FunctionalProgramming #AdventOfHaskell<\/li>\n<li><a href=\"https:\/\/www.fpcomplete.com\/haskell\/library\/vector\/\">vector: Efficient packed-memory data representations<\/a>. ~ @FPComplete. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/odone.io\/posts\/2020-12-21-scripting-the-hell-out-of-trello-in-haskell.html\">Scripting the Hell out of Trello with Haskell<\/a>. ~ Riccardo Odone. #Haskell #FunctionalProgramming #AdventOfHaskell<\/li>\n<li><a href=\"https:\/\/benoit.viguier.nl\/files\/tweetverif.pdf\">A Coq proof of the correctness of X25519 in TweetNaCl<\/a>. ~ P. Schwabe, B. Viguier, T. Weerwag, F. Wiedijk. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/ryan.orendorff.io\/posts\/2020-12-19-dependent-fold\/\">Dependently typed folds (folds that change type at each step!)<\/a>. ~ Ryan Orendorff. #Haskell #FunctionalProgramming #AdventOfHaskell<\/li>\n<li><a href=\"https:\/\/encodepanda.com\/posts\/2020-12-15-getting-acquainted-with-lens.html\">Getting acquainted with Lens (part 1)<\/a>. ~ Pawel Szulc. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/kowainik.github.io\/posts\/naming-conventions\">Foo to bar: Naming conventions in Haskell<\/a>. ~ Veronika Romashkina, Dmitrii Kovanikov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/republicaweb.es\/podcast\/descubriendo-la-programacion-funcional-haskell-con-hector-navarro\/\">Descubriendo la programaci\u00f3n funcional: Haskell con H\u00e9ctor Navarro<\/a>. #Haskell #Programaci\u00f3nFuncional<\/li>\n<li><a href=\"https:\/\/pit-claudel.fr\/clement\/papers\/koika-dsls-CoqPL21.pdf\">An experience report on writing usable DSLs in Coq<\/a>. ~ Cl\u00e9ment Pit-Claudel, Thomas Bourgeat. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/hackage-search\">Hackage search: Regex-based online code search<\/a>. ~ Vladislav Zavialov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/soupi\/haskell-study-plan\">Haskell study plan<\/a>. ~ Gil Mizrahi. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/ojs.elte.hu\/cejntrep\/article\/view\/965\/1042\">Classical programming topics with functional programming<\/a>. ~ Visnovitz M\u00e1rton #FunctionalProgramming #TypeScript<\/li>\n<li><a href=\"https:\/\/www.logicmatters.net\/wp-content\/uploads\/2020\/12\/LogicStudyGuide.pdf\">Logic: A study guide<\/a>. ~ Peter Smith. #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2012.09388\">Formalization of PAL\u22c5S5 in proof assistant<\/a>. ~ Jiatu Li. #ITP #LeanProver #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/ljt12138\/Proof-of-Surreal\">Formal proof of the main theorem for surreal<\/a>. ~ Jiatu Li. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/jesper.sikanda.be\/posts\/quickcheck-intro.html\">An introduction to property-based testing with QuickCheck<\/a>. ~ Jesper Cockx. #Haskell #FunctionalProgramming #QuickCheck<\/li>\n<li><a href=\"https:\/\/nliu.net\/posts\/2020-11-06-bytestring.html\">Beauty and the bytestring<\/a>. ~ Norman Liu. #Haskell #FunctionalProgramming #AdventOfHaskell<\/li>\n<li><a href=\"https:\/\/bor0.wordpress.com\/2020\/12\/11\/haskell-memoization-and-evaluation-model\/\">Haskell memoization and evaluation model<\/a>. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2012.08990\">A novice-friendly induction tactic for Lean<\/a>. ~ Jannis Limperg. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/gist.github.com\/serras\/bb33947855f539761d4873a3d18313c3\">Talking about Toys<\/a>. ~ Alejandro Serrano. #Haskell #FunctionalProgramming #AdventOfHaskell<\/li>\n<li><a href=\"https:\/\/arifordsham.com\/haskell-doomed-to-succeed\/\">Haskell &#8211; Doomed to succeed?<\/a> ~ Ari Fordsham. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2012.08231v1\">A new perspective of paramodulation complexity by solving massive 8 puzzles<\/a>. ~ Ruo Ando, Yoshiyasu Takefuji. #ATP #Otter<\/li>\n<li><a href=\"https:\/\/www.math3ma.com\/blog\/fibonacci-sequence\">The Fibonacci sequence as a functor<\/a>. ~ Tai-Danae Bradley. #CategoryTheory<\/li>\n<li><a href=\"https:\/\/vivid-synth.com\/advent-2020\/\">A vivid christmas carol<\/a>. #Haskell #FuncionalProgramming #AdventOfHaskell<\/li>\n<li><a href=\"https:\/\/blog.jpolak.org\/?p=2281\">On the Lean proof assistant, Part 1<\/a>. ~ Jason Polak. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/13422\/pdf\/OASIcs-FMBC-2020-9.pdf\">On the formal verification of the Stellar Consensus Protocol<\/a>. ~ G. Losa, M. Dodds. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/13412\/pdf\/oasics-vol084-fmbc2020-complete.pdf#page=67\">Authenticated data structures as functors in Isabelle\/HOL<\/a>. ~ A. Lochbihler, O. Mari\u0107. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-03053930\/document\">On the use of formal methods to model and verify neuronal archetypes<\/a>. ~ E. de Maria et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/13412\/pdf\/oasics-vol084-fmbc2020-complete.pdf#page=83\">Mechanized formal model of bitcoin&#8217;s blockchain validation procedures<\/a>. ~ K. Rupi\u0107, L. Ro\u017ei\u0107, A. Derek. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2020-12-14-enumerating-trees.html\">Enumerating trees<\/a>. ~ Donnacha Ois\u00edn Kidney. #Haskell #FunctionalProgramming #Agda<\/li>\n<li><a href=\"https:\/\/www.fpcomplete.com\/blog\/pattern-matching\/\">Pattern matching<\/a>. ~ Michael Snoyman. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2004.05631\">At the interface of algebra and statistics<\/a>. ~ Tai-Danae Bradley. #Math #CategoryTheory<\/li>\n<li><a href=\"https:\/\/thibaultmarin.github.io\/blog\/posts\/2016-11-13-Personal_website_in_org.html\">Personal website in org<\/a>. #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/potocpav.github.io\/programming\/2020\/12\/11\/functional-programming.html\">Precise typing implies functional programming<\/a>. ~ Pavel Poto\u010dek. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/jelv.is\/blog\/Structure-your-Errors\/\">Structure your errors<\/a>. ~ Tikhon Jelvis. #Haskell #FunctionalProgramming #AdventOfHaskell<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/holly-jolly-streaming-combinators.html\">Roll your own Holly Jolly streaming combinators with Free<\/a>. ~ Justin Le. #Haskell #FunctionalProgramming #AdventOfHaskell<\/li>\n<li><a href=\"https:\/\/www21.in.tum.de\/~eberlm\/pdfs\/diss.pdf\">Asymptotic reasoning in a proof assistant<\/a>. ~ Manuel Eberl. #PhD_Thesis #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2012.04400\">An answer to the Bose-Nelson sorting problem for 11 and 12 channels<\/a>. ~ Jannis Harder. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.college-de-france.fr\/media\/xavier-leroy\/UPL5416659662307063394_9.pdf\">Programmer = d\u00e9montrer? La correspondance de Curry-Howard aujourd\u2019hui<\/a>. ~ Xavier Leroy. #Logic #Math #CompSci #ITP<\/li>\n<li><a href=\"https:\/\/cronokirby.com\/posts\/2020\/11\/haskell-in-haskell-0\">(Haskell in Haskell) 0<\/a>. Introduction. ~ L\u00fac\u00e1s Meier. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cronokirby.com\/posts\/2020\/11\/haskell-in-haskell-1\">(Haskell in Haskell) 1<\/a>. Setup. ~ L\u00fac\u00e1s Meier. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cronokirby.com\/posts\/2020\/12\/haskell-in-haskell-2\/\">(Haskell in Haskell) 2<\/a>. Lexing. ~ L\u00fac\u00e1s Meier #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/functional.christmas\/2020\">Functional Christmas (2020)<\/a>. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.elm.christmas\/2020\">Elm Christmas (2020)<\/a>. #Elm #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/the-busy-beaver-game-illuminates-the-fundamental-limits-of-math-20201210\/\">How the slowest computer programs illuminate math\u2019s fundamental limits<\/a>. ~ John Pavlus. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/johncarlosbaez.wordpress.com\/2018\/09\/20\/patterns-that-eventually-fail\/\">Patterns that eventually fail<\/a>. ~ John Baez. #Math<\/li>\n<li><a href=\"http:\/\/texteditors.org\/cgi-bin\/wiki.pl?EmacsFamily\">Emacs family editors<\/a>. #Emacs<\/li>\n<li><a href=\"https:\/\/rjlipton.wordpress.com\/2020\/12\/10\/the-future-of-mathematics\/\">The future of Mathematics?<\/a> ~ R.J. Lipton. #ITP #Math<\/li>\n<li><a href=\"https:\/\/wjwh.eu\/posts\/2020-12-11-haskell-retries.html\">The &#8216;retry&#8217; package<\/a>. ~ Wander Hillen. #Haskell #FunctionalProgramming #AdventOfHaskell<\/li>\n<li><a href=\"https:\/\/anardil.net\/2020\/haskell-coreutils-tee.html\">Haskell coreutils: tee<\/a>. ~ Austin Gandalf. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/hasura.io\/blog\/parser-combinators-walkthrough\/\">Parser combinators: a walkthrough (Or: Write you a Parsec for great good)<\/a>. ~ Antoine Leblanc. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/blog\/2020-12-03-shrinks-applicative\/\">The shrinks applicative<\/a>. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/NorfairKing\/sydtest\">sydtest: An experimental testing framework for Haskell<\/a>. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2012.04715\">A SAT-based resolution of Lam&#8217;s problem<\/a>. ~ Curtis Bright, Kevin K. H. Cheung, Brett Stevens, Ilias Kotsireas, Vijay Ganesh. #ATP #SAT_Solvers #Math<\/li>\n<li><a href=\"https:\/\/www.cs.au.dk\/~spitters\/Concert2.pdf\">Extracting smart contracts tested and verified in Coq<\/a>. ~ D. Annenkov, M. Milo, J.B. Nielsen, B. Spitters. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/chrispenner.ca\/posts\/gadt-design\">Simpler and safer API design using GADTs<\/a>. ~ Chris Penner. #Haskell #FunctionalProgramming #AdventOfHaskell<\/li>\n<li><a href=\"https:\/\/arstechnica.com\/features\/2020\/12\/a-damn-stupid-thing-to-do-the-origins-of-c\/\">&#8220;A damn stupid thing to do&#8221; &#8211; the origins of C<\/a>. ~ Richard Jensen. #Programming<\/li>\n<li><a href=\"https:\/\/github.com\/bolt12\/advent-of-haskell-dd\">Denotational design<\/a>. ~ Armando Santos. #Haskell #FunctionalProgramming #AdventOfHaskell<\/li>\n<li><a href=\"https:\/\/www.oreilly.com\/radar\/what-is-functional-programming\/\">What is functional programming? ~ Mike Loukides<\/a>. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/emacsredux.com\/blog\/2020\/12\/08\/favorite-emacs-packages\/\">Favorite Emacs packages<\/a>. ~ Bozhidar Batsov. #Emacs<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/browser_info\/current\/AFP\/Relational_Method\/document.pdf\">The relational method with message anonymity for the verification of cryptographic protocols<\/a>. ~ Pasquale Noce. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/browser_info\/current\/AFP\/Relational_Minimum_Spanning_Trees\/document.pdf\">Relational minimum spanning tree algorithms (in Isabelle\/HOL)<\/a>. ~ Walter Guttmann, Nicolas Robinson-O&#8217;Brien. #ITP #IsabelleHOL #Algorithms<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/13291\/pdf\/LIPIcs-FSTTCS-2020-50.pdf\">Computable analysis for verified exact real computation<\/a>. ~ M. Kone\u010dn\u00fd, F. Steinberg, H. Thies. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.cs.au.dk\/~birke\/papers\/mpmc-queue.pdf\">Mechanized verification of a fine-grained concurrent queue from Facebook&#8217;s Folly library<\/a>. ~ S.F. Vindum, D. Frumin, L. Birkedal. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/raw.githubusercontent.com\/jonaprieto\/the-pigeonhole-principle\/master\/The-pigeonhole-principle-HoTT.pdf\">The Pigeonhole principle<\/a>. ~ Jonathan Prieto-Cubides. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/boarders.github.io\/posts\/halting1.html\">The halting problem (part 1)<\/a>. ~ Callan McGill. #Haskell #FunctionalProgramming #Logic #Math<\/li>\n<li><a href=\"https:\/\/boarders.github.io\/posts\/halting2.html\">The halting problem (part 2)<\/a>. ~ Callan McGill. #ITP #Agda #Logic #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2012.01150v1\">Voevodsky&#8217;s unachieved project<\/a>. ~ Andrei Rodin. #ITP #Math<\/li>\n<li><a href=\"https:\/\/kowainik.github.io\/posts\/haddock-tips\">Haskell documentation with Haddock: Wishes&#8217;n&#8217;tips<\/a>. ~ Veronika Romashkina, Dmitrii Kovanikov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/proof-theory-development\/\">The development of proof theory<\/a>. ~ Jan von Plato. #Logic #ATP<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/reasoning-automated\/\">Automated reasoning<\/a>. ~ Frederic Portoraro. #ATP #ITP #Logic #Math #LogicProgramming<\/li>\n<li><a href=\"https:\/\/carboncloud.com\/2020\/12\/07\/tech-knowledge-as-code\/\">Benefits of statically typed functional programming? Wrong question<\/a>. ~ Mikael T\u00f6nnberg. #FunctionalProgramming #AdventOfHaskell<\/li>\n<li><a href=\"http:\/\/tomasp.net\/academic\/drafts\/cultures\/%20\">Cultures of programming: Understanding the history of programming through controversies and technical artifacts<\/a>. ~ Tomas Petricek. #Programming #Emacs<\/li>\n<li><a href=\"https:\/\/schooloffp.co\/2020\/12\/05\/whirlwind-tour-of-stack-for-beginners.html\">Whirlwind tour of Stack for beginners<\/a>. ~ School of FP. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/kenta.blogspot.com\/2020\/12\/orptuqka-bits-instance-of-integer.html\">Bits instance of Integer<\/a>. ~ Ken T Takusagawa. #Haskell #FuncionalProgramming<\/li>\n<li><a href=\"https:\/\/gelisam.blogspot.com\/2020\/12\/capturing-magic-of-preludeinteract.html\">Capturing the magic of Prelude<\/a>.interact. ~ Samuel. #Haskell #FuncionalProgramming #AdventOfHaskell<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2020\/12\/05\/liquid-tensor-experiment\/\">Liquid tensor experiment<\/a>. ~ Peter Scholze. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.joachim-breitner.de\/blog\/777-Named_goals_in_Coq\">Named goals in Coq<\/a>. ~ Joachim Breitner. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/hackage.haskell.org\/package\/group-theory\">The group-theory package<\/a>. ~ Emily Pillmore. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/gilmi.me\/blog\/post\/2020\/12\/05\/scotty-bulletin-board\">Building a bulletin board using Scotty and friend<\/a>. ~ Gil Mizrahi. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/logicday.vcla.at\/\">Ambassadors of Logic<\/a>. #Logic<\/li>\n<li><a href=\"https:\/\/www.hindawi.com\/journals\/mpe\/2020\/6191537\/\">Lolisa: Formal syntax and semantics for a subset of the Solidity programming language in mathematical tool Coq<\/a>. ~ Zheng Yang. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/harporoeder.com\/posts\/haskell-runtime\/\">The Haskell runtime is what sets it apart from the competition<\/a>. ~ Harpo Roeder. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blind.guru\/blog\/2020-12-05-codeblock.html\">Processing CodeBlocks in Hakyll<\/a>. ~ Mario Lang. #Haskell #FunctionalProgramming #Hakyll #AdventOfHaskell<\/li>\n<li><a href=\"https:\/\/www.microsiervos.com\/archivo\/matematicas\/algoritmos-calcular-valor-numero-pi.html\">Una recopilaci\u00f3n de algoritmos para calcular el valor del n\u00famero \u03c0<\/a>. ~ @Alvy. #Matem\u00e1ticas #Algoritmos #Programaci\u00f3n<\/li>\n<li><a href=\"https:\/\/thomas-joly.com\/yet-another-pi-computation-algorithms\/\">Yet another \u03c0 computation algorithms<\/a>. ~ Thomas Joly. #Math #Algorithms #Programming<\/li>\n<li><a href=\"https:\/\/www.microsiervos.com\/archivo\/ordenadores\/nandgame-juego-logica-binaria-circuitos.html\">NandGame: un juego de l\u00f3gica binaria en el que hay que construir circuitos cada vez m\u00e1s complejos<\/a>. ~ @Alvy. #L\u00f3gica #Computaci\u00f3n<\/li>\n<li><a href=\"http:\/\/nandgame.com\/\">The Nand Game<\/a>. #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/hackage.haskell.org\/package\/numhask-free-0.0.3\/docs\/NumHask-FreeAlgebra.html\">The Free Num is a Sequence of Bags<\/a>. ~ Tony Day. #Haskell #FunctionalProgramming #AdventOfHaskell<\/li>\n<li><a href=\"https:\/\/medium.com\/@terezk_a\/haskell-in-elm-terms-type-classes-415f1612b335\">Haskell, in Elm terms: Type Classes<\/a>. ~ @terezk_a #Haskell #FuncionalProgramming #Elm<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2012.00856\">Another tool in the box: Why use formal methods for autonomous systems?<\/a> ~ Matt Luckcuck. #FormalMethods<\/li>\n<li><a href=\"https:\/\/gustavofranke.github.io\/posts\/2020-12-01-my-journey-into-haskell.html\">My journey into Haskell<\/a>. ~ Gustavo Franke. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/juliu.is\/complicated-haskell-words-isomorphism\/\">Complicated Haskell words &#8211; Isomorphism<\/a>. ~ Ju Liu. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/3fx.ch\/blog\/2020\/12\/03\/composition-in-trick-taking-card-games\/\">Composition in trick-taking card games<\/a>. ~ Ben Fiedler. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/redtachyon.me\/post\/aoc-haskell\/%20\">Advent of Code 2020 with Haskell<\/a>. ~ Ariel Kwiatkowski. #Haskell #FunctionalProgramming #AdventOfCode<\/li>\n<li><a href=\"https:\/\/pit-claudel.fr\/clement\/papers\/koika-dsls-CoqPL21.pdf\">An experience report on writing usable DSLs in Coq<\/a>. ~ Cl\u00e9ment Pit-Claudel, Thomas Bourgeat. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/www.lix.polytechnique.fr\/Labo\/Samuel.Mimram\/teaching\/INF551\/course.pdf\">Program = Proof<\/a>. ~ Samuel Mimram. #eBook #Logic #Math #ITP #Agda<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/browser_info\/current\/AFP\/Finite-Map-Extras\/document.pdf\">Finite map extras (in Isabelle\/HOL)<\/a>. ~ Javier D\u00edaz. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/github.com\/haskelling\/aoc2020\">Haskell solutions to Advent of Code 2020<\/a>. #Haskell #FunctionalProgramming #AdventOfCode<\/li>\n<li><a href=\"https:\/\/github.com\/mstksg\/advent-of-code-2020\">Haskell solutions to Advent of Code 2020<\/a>. ~ Justin Le. #Haskell #FunctionalProgramming #AdventOfCode<\/li>\n<li><a href=\"https:\/\/github.com\/rwbarton\/advent-of-lean-4\">Advent of Code 2020 solutions in Lean 4<\/a>. ~ Reid Barton. #LeanProver #ITP #FuncionalProgramming<\/li>\n<li><a href=\"https:\/\/eprint.iacr.org\/2020\/1477.pdf\">Machine-checking the universal verifiability of Election Guard<\/a>. ~ Thomas Haines, Rageev Gor\u00e9, Jack Stodart. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/pu.edu.pk\/images\/journal\/maths\/PDF\/Paper_4_52_11_2020.pdf%20\">A note on right abelian distributive AG-groupoids<\/a>. ~ Bashar Khan et als. #ATP #Prover9 #Mace4 #Math<\/li>\n<\/ul>\n<\/div>\n<div id=\"postamble\" class=\"status\"><\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante diciembre 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\/7595"}],"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=7595"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7595\/revisions"}],"predecessor-version":[{"id":7596,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7595\/revisions\/7596"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7595"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7595"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7595"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}