{"id":6721,"date":"2019-02-01T11:10:17","date_gmt":"2019-02-01T10:10:17","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6721"},"modified":"2019-09-01T11:11:56","modified_gmt":"2019-09-01T09:11:56","slug":"resumen-de-lecturas-compartidas-durante-enero-de-2019","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-enero-de-2019\/","title":{"rendered":"Resumen de lecturas compartidas durante enero de 2019"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante enero de 2019, 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=\"http:\/\/fse.studenttheses.ub.rug.nl\/8724\/1\/verslag.pdf\">Evaluation of Isabelle with a proof of the perfect number theorem<\/a>. ~ Mark IJbema. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/publications.lib.chalmers.se\/records\/fulltext\/256404\/256404.pdf\">Univalent categories (A formalization of category theory in Cubical Agda)<\/a>. ~ F.H. Iversen #Msc_Thesis #ITP #Agda<\/li>\n<li><a href=\"https:\/\/www.cs.uoregon.edu\/research\/summerschool\/summer13\/lectures\/Kinds_and_GADTs.pdf\">Fun with kinds and GADTS<\/a>. ~ Simon Peyton Jones. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cse.unt.edu\/~tarau\/research\/2019\/tprover.pdf\">A combinatorial testing framework for intuitionistic propositional theorem provers<\/a>. ~ P. Tarau. #ATP #Logic #Prolog<\/li>\n<li><a href=\"https:\/\/github.com\/alexwl\/haskell-code-explorer\/blob\/master\/README.md\">Haskell Code Explorer: Web application for exploring and understanding Haskell libraries<\/a>. ~ Alexey Kiryushin. #Haskell<\/li>\n<li><a href=\"https:\/\/blog.poisson.chat\/posts\/2018-08-06-one-type-family.html\">Haskell with only one type family<\/a>. ~ Xia Li-yao. #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/MWRuszczycky\/rubiks\">3D-Rubik&#8217;s cube simulator written in Haskell using Gloss<\/a>. ~ Mark W. Ruszczycky. #Haskell<\/li>\n<li><a href=\"http:\/\/blog.klipse.tech\/prolog\/2019\/01\/01\/blog-prolog.html\">A new way of blogging about Prolog<\/a>. ~ Yehonathan Sharvit. #Prolog #Klipse #Clojure<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Concurrent_Revisions.html\">Formalization of concurrent revisions in Isabelle\/HOL<\/a>. ~ R. Overbeek. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/blog.clement.delafargue.name\/posts\/2018-12-27-a-tale-of-servant-clients.html\">A tale of servant clients<\/a>. ~ C. Delafargue. #Haskell<\/li>\n<li><a href=\"http:\/\/fixpt.de\/blog\/2018-12-30-strictness-analysis-part-2.html\">All about strictness analysis (part 2)<\/a>. ~ Sebastian Graf. #Haskell<\/li>\n<li><a href=\"https:\/\/jappieklooster.nl\/lens-into-wrapped-newtypes.html\">Lens into wrapped newtypes<\/a>. ~ Jappie Klooster. #Haskell<\/li>\n<li><a href=\"https:\/\/www.wjwh.eu\/posts\/2019-01-01-parsing-infinite-streams.html\">Parsing infinite streams with attoparsec<\/a>. ~ Wander Hillen. #Haskell<\/li>\n<li><a href=\"https:\/\/lin-techdet.blogspot.com\/2018\/12\/type-annotations-vs-partial-type.html\">Type annotations vs partial type signatures vs visible type applications<\/a>. ~ Alexey Radkov. #Haskell<\/li>\n<li><a href=\"https:\/\/cs.vu.nl\/~jhl890\/pub\/hoelzl2011measuretheory.pdf\">Three chapters of measure theory in Isabelle\/HOL<\/a>. ~ J. H\u00f6lzl, A. Heller. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/medium.com\/@hgiasac\/typeable-a-long-journey-to-type-safe-dynamic-type-representation-9070eac2cf8b\">Typeable:\u200aA long journey to type-safe dynamic type representation<\/a>. ~ Toan Nguyen. #Haskell<\/li>\n<li><a href=\"http:\/\/matryoshka.gforge.inria.fr\/pubs\/schlichtkrull_phd_thesis.pdf\">Formalization of logic in the Isabelle proof assistant<\/a>. ~ A. Schlichtkrull. #PhD_Thesis #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/lean-forward.github.io\/logical-verification\/2018\/index.html\">Course: Logical verification (2018-2019)<\/a>. ~ J. Blanchette et als. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/liquid.kosmikus.org\">Liquid Haskell tutorial<\/a>. ~ Andres L\u00f6h. #Haskell #LiquidHaskell<\/li>\n<li><a href=\"http:\/\/dld.bz\/hmaAS\">The QED Manifesto revisited<\/a>. ~ Freek Wiedijk. #ITP<\/li>\n<li><a href=\"http:\/\/ftp.science.ru.nl\/CSI\/CompMath.Found\/Barendregt-Wiedijk.pdf\">The challenge of computer mathematics<\/a>. ~ H. Barendregt, F. Wiedijk. #ITP<\/li>\n<li><a href=\"https:\/\/github.com\/fsestini\/zsyntax\">Zsyntax: Automated theorem prover for a linear logic-based calculus for molecular biology<\/a>. ~ Filippo Sestini. #ATP #Logic #Haskell<\/li>\n<li><a href=\"https:\/\/journals.plos.org\/plosone\/article?id=10.1371\/journal.pone.0009511\">Zsyntax: A formal language for molecular biology with projected applications in text mining and biological prediction<\/a>. ~ G. Boniolo, M. D&#8217;Agostino, P.P. di Fiore. #ATP #Logic #Haskell<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Core_DOM.html\">A formal model of the Document Object Model (DOM) in Isabelle\/HOL<\/a>. ~ A.D. Brucker, M, Herzberg. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/yudkowsky.net\/assets\/44\/LobsTheorem.pdf\">(The Cartoon Guide to) Lob&#8217;s Theorem<\/a>. ~ Eliezer Yudkowsky. #Logic<\/li>\n<li><a href=\"https:\/\/identicalsnowflake.github.io\/Cantor.html\">Cantor pairing<\/a>. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/1\/7\/why-haskell-i-simple-data-types\">Why Haskell I: Simple data types!<\/a> ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/epogrebnyak\/haskell-intro\">Short overview of Haskell concepts<\/a>. ~ E. Pogrebnyak et als. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.nature.com\/articles\/d41586-019-00083-3\">Machine learning leads mathematicians to unsolvable problem<\/a>. ~ D. Castelvecchi. #AI #Math #MachineLearnig<\/li>\n<li><a href=\"https:\/\/www.nature.com\/articles\/d41586-019-00012-4\">Unprovability comes to machine learning<\/a>. ~ L. Reyzin #AI #Math #MachineLearnig<\/li>\n<li><a href=\"http:\/\/cs.engr.uky.edu\/~mirek\/stuff\/kr-2018-gm.pdf\">Answer Set Programming (A story of default negation, definitions and informal semantics) <\/a>. ~ M. Truszczynski #ASP #Logic #Programming #KR<\/li>\n<li><a href=\"https:\/\/taeer.bar-yam.me\/blog\/posts\/hakyll-tikz\/\">Hakyll + TikZ<\/a>. ~ Taeer Bar-Yam. #Haskell<\/li>\n<li><a href=\"https:\/\/haskell-at-work.com\/episodes\/2019-01-10-purely-functional-gtk-part-1-hello-world.html\">Purely functional GTK+, Part 1: Hello World<\/a>. ~ Oskar Wickstr\u00f6m. #Haskell<\/li>\n<li><a href=\"https:\/\/k-bx.github.io\/articles\/Validating-Form-Data-via-Applicative-Functors.html\">Validating form data via applicative functors<\/a>. ~ Kostiantyn Rybnikov. #Haskell<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Store_Buffer_Reduction.html\">A reduction theorem for store buffers<\/a>. ~ E. Cohen, N. Schirmer. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/project-archive.inf.ed.ac.uk\/msc\/20182958\/msc_proj.pdf\">HaskellQuest: a game for teaching functional programming in Haskell<\/a>. ~ R. Fu. #Teaching #Haskell<\/li>\n<li><a href=\"http:\/\/www.joachim-breitner.de\/blog\/750-Teaching_to_read_Haskell\">Teaching to read Haskell<\/a>. ~ Joachim Breitner. #Haskell<\/li>\n<li><a href=\"http:\/\/haskell-for-readers.nomeata.de\/\">Haskell for readers<\/a>. ~ Joachim Breitner. #Haskell<\/li>\n<li><a href=\"https:\/\/www.logicmatters.net\/resources\/pdfs\/ProofSystems.pdf\">Types of proof system<\/a>. ~ Peter Smith. #Logic #ITP<\/li>\n<li><a href=\"https:\/\/www.aurelienalvarez.org\/my-app\/dist\/assets\/pdf\/ALVAREZ_nombres-premiers-Euclide-Coq_Quadrature_2019.pdf\">Nombres premiers, Euclide et Coq<\/a>. ~ A. Alvarez. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2019\/01\/12\/column-addition\">Column addition<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/medium.com\/javascript-scene\/the-forgotten-history-of-oop-88d71b9b2d9f\">The forgotten history of OOP<\/a>. ~ Eric Elliott. #Programming #History<\/li>\n<li><a href=\"https:\/\/blog.po.et\/building-the-verifiable-web-cb1b93a40b11\">Building the verifiable Web<\/a>. ~ Kevin Buzzard. #Blockchain<\/li>\n<li><a href=\"https:\/\/t.co\/ENeTmK25iN\">The compactness theorem and applications<\/a>. ~ B. Call #Logic<\/li>\n<li><a href=\"http:\/\/cgi.csc.liv.ac.uk\/~frank\/MLHandbook\/\">Handbook of modal logic<\/a>. ~ P. Blackburn, J. van Benthem, F. Wolter. #Logic<\/li>\n<li><a href=\"http:\/\/www.iiisci.org\/Journal\/CV$\/sci\/pdfs\/MA079VM12.pdf\">A comparison of functional and imperative programming techniques for mathematical software development<\/a>. ~ S. Frame, J.W. Coffey. #Haskell #Cpp #Math<\/li>\n<li><a href=\"https:\/\/www.youtube.com\/watch?v=ofUAlkYHFsI\">HaskellRank 11: Treating lists as monads<\/a>. ~ @tsoding. #Haskell #HaskellRank<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/1\/14\/why-haskell-ii-sum-types\">Why Haskell II: Sum types<\/a>. ~ James Bowen. #Haskell #Java #Python<\/li>\n<li><a href=\"https:\/\/jespercockx.github.io\/popl19-tutorial\/\">Correct by construction programming in Agda<\/a>. ~ Jesper Cockx. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Higher_Order_Terms.html\">An algebra for higher-order terms in Isabelle\/HOL<\/a>. ~ Lars Hupel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/www.tpflug.me\/2019\/01\/14\/haskell-nix-vim\">Haskell, Nix and Vim: Getting started<\/a>. ~ Tobias Pflug. #Haskell #Nix #Vim<\/li>\n<li><a href=\"http:\/\/www.people.cs.uchicago.edu\/~soare\/History\/handbook.pdf\">The history and concept of computability<\/a>. ~ Robert I. Soare. #CompSci<\/li>\n<li><a href=\"https:\/\/www.cis.upenn.edu\/~llamp\/pdf\/urns.pdf\">Ode on a random urn (Functional pearl)<\/a>. ~ L. Lampropoulos, A. Spector-Zabusky, K. Foner, #Haskell<\/li>\n<li><a href=\"https:\/\/denibertovic.com\/posts\/haskell-showroom-how-to-switch-between-kubernetes-clusters\">Haskell Showroom: How to switch between multiple kubernetes clusters and namespaces<\/a>. ~ Deni Bertovic #Haskell<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/a-touch-of-topological-quantum-computation-in-haskell-pt-ii-automating-drudgery\/\">A touch of topological quantum computation in Haskell Pt. II: Automating drudgery<\/a>. ~ Philip Zucker. #Haskell<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/IMP2.html\">IMP2: Simple program verification in Isabelle\/HOL<\/a>. ~ Peter Lammich and Simon Wimmer. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-01977585\/document\">Verifiable certificates for predicate subtyping<\/a>. ~ F. Gilbert. #ITP #PVS<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1901.03313\">Mechanization of separation in generic extensions<\/a>. ~ E- Gunther, M. Pagano, P.S Terraf. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.p%C3%A9drot.fr\/articles\/coqpl2019.pdf\">Ltac2: Tactical warfare<\/a>. ~ P.M. P\u00e9drot. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.xn--pdrot-bsa.fr\/articles\/thesis.pdf\">A materialist dialectica<\/a>. ~ P.M. P\u00e9drot. #PhD_Thesis #Logic #CompSci<\/li>\n<li><a href=\"http:\/\/bit.ly\/2RNTMGw\">L\u00f6b and m\u00f6b: strange loops in Haskell<\/a>. ~ David Luposchainsky. #Haskell<\/li>\n<li><a href=\"http:\/\/neilmitchell.blogspot.com\/2019\/01\/ignoring-hlint.html\">Ignoring HLint (HLint now has more ways to ignore hints you don&#8217;t like)<\/a>. ~ Neil Mitchell. #Haskell<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2019-01-15-binomial-urn.html\">A binomial urn<\/a>. ~ Donnacha Ois\u00edn Kidney. #Haskell<\/li>\n<li><a href=\"https:\/\/jaspervdj.be\/posts\/2019-01-11-dynamic-graphs.html\">Dynamic graphs: A Haskell library for the dynamic connectivity problem<\/a>. ~ Jasper Van der Jeugt. #Haskell<\/li>\n<li><a href=\"https:\/\/phaazon.net\/blog\/aoc-18-hindsight\">Hindsight on Advent of Code 2018<\/a>. ~ Dimitri Sabadie. #Haskell<\/li>\n<li><a href=\"https:\/\/lean-forward.github.io\/\">Lean Forward: Usable computer-checked proofs and computations for number theorists<\/a>. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover\/mathlib\">mathlib: Lean mathematical components library<\/a>. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/lean-forward.github.io\/lean-together\/2019\/slides\/buzzard.pdf\">Using Lean with undergraduate mathematicians<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3294093\">Smooth manifolds and types to sets for linear algebra in Isabelle\/HOL<\/a>. ~ F. Immler, B. Zhan. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/elpais.com\/elpais\/2019\/01\/15\/eps\/1547557079_800501.html\">Las mentes matem\u00e1ticas mueven el mundo<\/a>. ~ G. Abril. #Matem\u00e1ticas<\/li>\n<li><a href=\"http:\/\/robertylewis.com\/files\/icms\/WMFarmer-new-proof-style-icms-2018.pdf\">A new style of mathematical proof<\/a>. ~ William Farmer. #Logic #Math #ITP<\/li>\n<li><a href=\"https:\/\/avigad.github.io\/formal_methods_in_education\/\">Resources for teaching with formal methods<\/a>. ~ Jeremy Avigad. #Logic #Math #CompSci #ITP<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3294104\">Dynamic class initialization semantics: a Jinja extension<\/a>. ~ S. Mansky, E.L. Gunter. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/www.cs.pomona.edu\/~michael\/courses\/csci054s18\/book\/\">Discrete Math in Coq<\/a>. ~ B.C. Pierce et als. #ITP #Coq Math<\/li>\n<li><a href=\"http:\/\/www.cs.pomona.edu\/~michael\/papers\/coqpl2019.pdf\">Teaching discrete mathematics to early undergraduates with &#8220;Software Foundations&#8221;<\/a>. ~ M. Greenberg, J.C. Osborn. #ITP #Coq #Math<\/li>\n<li><a href=\"http:\/\/www.cs.pomona.edu\/~michael\/courses\/csci054s18\">Course: Discrete mathematics and functional programming<\/a>. ~ M. Greenberg. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3294102\">Formally verified big step semantics out of x86-64 binaries<\/a>. ~ I. Roessle, F. Verbeek, B. Ravindran. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/tinselcity.net\/pensando-en-programar\">Pensando en programar<\/a>. ~ Gonzalo Garc\u00eda Braschi. #Programaci\u00f3n<\/li>\n<li><a href=\"https:\/\/github.com\/sjoerdvisscher\/data-category\">Data-category: a collection of categories, and some categorical constructions on them<\/a>. ~ Sjoerd Visscher. #Haskell<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/1\/21\/why-haskell-iii-parametric-types\">Why Haskell III: Parametric types<\/a>. ~ James Bowen. #Haskell #Java #Cpp #Python<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Farkas.html\">Farkas&#8217; lemma and Motzkin&#8217;s transposition theorem in Isabelle\/HOL<\/a>. ~ R. Bottesch, M.W. Haslbeck, R. Thiemann. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/vanemden.wordpress.com\/2018\/07\/21\/dijkstra-and-logic\/\">A bridge too far: E.W. Dijkstra and logic<\/a>. ~ Maarten van Emden. #Logic<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Auto2_Imperative_HOL.html\">Verifying imperative programs using auto2<\/a>. ~ B. Zhan. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/gupea.ub.gu.se\/bitstream\/2077\/53339\/1\/gupea_2077_53339_1.pdf\">Proof editor for natural deduction in first-order logic (The evaluation of an educational aiding tool for students learning logic)<\/a>. ~ E. Bj\u00f6rnsson et als. #Logic #Teaching #RA2018<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1901.06567.pdf\">Tarski&#8217;s relevance logic<\/a>. R. D. Maddux. #Logic<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2019-01-23-jupyterlab-ihaskell.html\">Towards interactive Data Science in Haskell: Haskell in JupyterLab<\/a>. ~ Matthias Meschede, Juan Sim\u00f5es. #Haskell<\/li>\n<li><a href=\"https:\/\/www.well-typed.com\/blog\/2019\/01\/qsm-in-depth\">An in-depth look at quickcheck-state-machine<\/a>. ~ Edsko de Vries. #Haskell<\/li>\n<li><a href=\"http:\/\/www.cs.ox.ac.uk\/people\/bernard.sufrin\/personal\/jape.org\/OXFORDIFP\/Jape\/JapeForIFP.pdf\">Using Jape for &#8220;Introduction to formal proof&#8221;<\/a>. ~ Bernard Sufrin. #ITP #Jape #Logic<\/li>\n<li><a href=\"https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0890540104001804\">Proving pointer programs in higher-order logic<\/a>. ~ F. Mehta, T. Nipkow. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/interstices.info\/la-revolution-de-lapprentissage-profond\/\">La r\u00e9volution de l\u2019apprentissage profond<\/a>. ~ Y. Bengio. #AI<\/li>\n<li><a href=\"https:\/\/vitez.me\/haskell-error-reduction\">A beginner\u2019s guide to the ways Haskell helps us avoid errors<\/a>. ~ Mitchell Vitez. #Haskell<\/li>\n<li><a href=\"https:\/\/oisdk.github.io\/agda-ring-solver\/README.html\">Solving rings in Aga<\/a>. ~ Donnacha Ois\u00edn Kidney. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1401.7694\">Experience implementing a performant category-theory library in Coq<\/a>. ~ J. Gross, A. Chlipala, D.I. Spivak. #ITP #Coq #CategoryTheory<\/li>\n<li><a href=\"https:\/\/owickstrom.github.io\/domain-modelling-with-haskell-workshop\/\">Domain modelling with Haskell<\/a>. ~ Oskar Wickstr\u00f6m. #Haskell<\/li>\n<li><a href=\"https:\/\/www.datasciencecentral.com\/profiles\/blogs\/r-python-julia-and-polyglot\">R, Python, Julia \u2026 and Polyglot<\/a>. ~ Steve Miller. #Programming #Rstats #Python #Julia #Jupyter<\/li>\n<li><a href=\"http:\/\/dropbox.com\/s\/joaq7m9v75blrw5\/pl-notation-lambdaconf-2018.pdf?dl=1\">Crash course on notation in programming language theory<\/a>. ~ Jeremy G. Siek. #CompSci<\/li>\n<li><a href=\"http:\/\/bit.ly\/haskell-tt-fby\">Haskell and type theory: better together<\/a>. ~ V. Bragilevsky. #Haskell #TypeTheory #LambdaCalculus<\/li>\n<li><a href=\"https:\/\/research-repository.st-andrews.ac.uk\/bitstream\/handle\/10023\/15729\/Barwell_2017_FGCS_ParallelFunctionalPearls_AAM.pdf\">Finding parallel functional pearls: Automatic parallel recursion scheme detection in Haskell functions via anti-unification<\/a>. ~ A.D. Barwell, C. Brown, K. Hammond. #Haskell<\/li>\n<li><a href=\"http:\/\/www2.sf.ecei.tohoku.ac.jp\/~kztk\/papers\/kztk_jfp_am_2018.pdf\">Applicative bidirectional programming (Mixing lenses and semantic bidirectionalization)<\/a>. ~ K. Matsuda, M. Wang. #Haskell<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/bidirectional-applicative-programming-and-automatic-differentation\">Applicative bidirectional programming and automatic differentiation<\/a>. ~ Philip Zucker. #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/google\/haskell-trainings\">Haskell trainings at Google<\/a>. #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/2HCapB6\">Haskell trainings at Google: 101<\/a>. #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/2HyDJIv\">Haskell trainings at Google: 102<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/culturacientifica.com\/2016\/01\/27\/el-origen-de-los-signos-matematico\">El origen de los signos matem\u00e1ticos<\/a>. ~ Ra\u00fal Ib\u00e1\u00f1ez. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/1\/28\/why-haskell-iv-typeclasses-vs-inheritanc\">Why Haskell IV: Typeclasses vs. inheritance<\/a>. ~ James Bowen. #Haskell<\/li>\n<li><a href=\"https:\/\/www.sciencedirect.com\/science\/article\/pii\/016764239190036W\/pdf?md5=b7dedd960214d9191929e6f41f5fd5be&amp;pid=1-s2.0-016764239190036W-main.pdf\">On the expressive power of programming languages<\/a>. ~ M. Felleisen. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/web.stanford.edu\/~kdevlin\/Papers\/DanesiChapter.pdf\">How technology has changed what it means to think mathematically<\/a>. ~ K. Devlin. #Math<\/li>\n<li><a href=\"http:\/\/bit.ly\/2SiIPNe\">A correct compiler from Mini-ML to a big-step machine verified using natural semantics in Coq<\/a>. ~ A. Z\u00faniga, G. Bel-Enguix. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.fpcomplete.com\/blog\/https\/www.fpcomplete.com\/blog\/defining-exceptions-in-haskell\">Defining exceptions in Haskell<\/a>. ~ Chris Done. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.um.edu.mt\/library\/oar\/handle\/123456789\/38118\">Combinatory logic: from philosophy and mathematics to computer science<\/a>. ~ A. Farrugia. #Logic #Math #CompSci #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/rjlipton.wordpress.com\/2019\/01\/29\/primes-and-polynomials\">Primes and polynomials<\/a>. ~ R.J. Lipton, K.W. Regan. #Math<\/li>\n<li><a href=\"http:\/\/www.cl.cam.ac.uk\/~na482\/meta\/lecture-notes.pdf\">Metaprogramming lecture notes<\/a>. ~ Nada Amin. #Programming #Scala #Lisp #Prolog<\/li>\n<li><a href=\"https:\/\/dkwise.wordpress.com\/2019\/01\/18\/fractals-and-monads\">Fractals and monads in Haskell (Part 1)<\/a>. ~ Derek Wise. #Haskell<\/li>\n<li><a href=\"https:\/\/dkwise.wordpress.com\/2019\/01\/30\/fractals-and-monads-part-2\/\">Fractals and monads in Haskell (Part 2)<\/a>. ~ Derek Wise. #Haskell<\/li>\n<\/ul>\n<\/div>\n<div id=\"postamble\" class=\"status\">\n<p class=\"date\">\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante enero de 2019, 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\/6721"}],"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=6721"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6721\/revisions"}],"predecessor-version":[{"id":6722,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6721\/revisions\/6722"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6721"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6721"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6721"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}