{"id":6242,"date":"2018-10-02T19:09:32","date_gmt":"2018-10-02T17:09:32","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6242"},"modified":"2018-10-02T19:11:23","modified_gmt":"2018-10-02T17:11:23","slug":"resumen-de-lecturas-compartidas-durante-septiembre-de-2018","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-septiembre-de-2018\/","title":{"rendered":"Resumen de lecturas compartidas durante septiembre de 2018"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante septiembre de 2018, 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:\/\/alvinalexander.com\/downloads\/HelloScala-FreePreview.pdf\">Hello, Scala (Learn Scala fast with small, easy lessons)<\/a>. ~ A. Alexander (@alvinalexander). #eBook #FunctionalProgramming #Scala<\/li>\n<li><a href=\"https:\/\/tarski.cs.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-julio-de-2018\">GLC: Resumen de lecturas compartidas durante julio de 2018<\/a>. #FunctionalProgramming #ITP<\/li>\n<li><a href=\"https:\/\/tarski.cs.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-agosto-de-2018\/\">GLC: Resumen de lecturas compartidas durante agosto de 2018<\/a>. #FunctionalProgramming #ITP<\/li>\n<li><a href=\"https:\/\/www.geekwire.com\/2018\/top-schools-ai-new-study-ranks-leading-u-s-artificial-intelligence-grad-programs\/\">Top schools for AI: New study ranks the leading U.S. artificial intelligence grad programs<\/a>. #AI<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1808.08329\">When you should use lists in Haskell (mostly, you should not)<\/a>. ~ J. Waldmann. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/www.imn.htwk-leipzig.de\/~waldmann\/talk\/17\/wflp\/main.pdf\">How I teach functional programming<\/a>. ~ J. Waldmann. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.imn.htwk-leipzig.de\/~waldmann\/etc\/untutorial\/data\/\">How do we store data, then?<\/a> ~ J. Waldmann. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.imn.htwk-leipzig.de\/~waldmann\/etc\/untutorial\/lens\/\">Introduction to the Lens Library<\/a>. ~ J. Waldmann. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1808.10690\">On the formalization of higher inductive types and synthetic homotopy theory<\/a>. ~ F. van_Doorn. #ITP #Lean #HoTT<\/li>\n<li><a href=\"https:\/\/owickstrom.github.io\/declarative-gtk-programming-in-haskell\">Declarative GTK+ programming with Haskell<\/a>. ~ O. Wickstr\u00f6m (@owickstrom) #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/owickstrom\/gi-gtk-declarative\">Declarative GTK+ programming in Haskell<\/a>. ~ O. Wickstr\u00f6m (@owickstrom) #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/www.scipy-lectures.org\/\">Scipy Lecture Notes (One document to learn numerics, science, and data with Python)<\/a>. #Programming #Python<\/li>\n<li><a href=\"https:\/\/haskell-containers.readthedocs.io\/en\/latest\/index.html\">Introduction and overview of the main features of the containers package<\/a>. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/www.unirioja.es\/cu\/jodivaso\/publications\/2018\/AISC_2018.pdf\">REGULAR-MT: A formal proof of the computation of Hermite normal form in a general setting<\/a>. ~ J. Divas\u00f3n, J. Aransay. #ITP #IsabelleHOL #Math #Vestigium<\/li>\n<li><a href=\"https:\/\/karl-voit.at\/2017\/09\/23\/orgmode-as-markup-only\/\">Org-Mode is one of the most reasonable markup languages to use for text<\/a>. ~ Karl Voit. #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/ambrevar.xyz\/blog-architecture\">A blog in pure Org\/Lisp (A pamphlet for hackable website systems)<\/a>. ~ Pierre Neidhardt #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2018\/8\/20\/making-the-jump-ii-using-more-monads\">Making the jump II: Using more monads<\/a>. ~ James Bowen (@james_OWA) #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/kenta.blogspot.com\/2018\/09\/fanlevif-cbc-encryption-and-decryption.html\">The CBC (Cipher Block Chaining) encryption and decryption<\/a>. ~ Ken T Takusagawa #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/fun.cs.tufts.edu\/stream-fusion.pdf\">Stream fusion (from lists to streams to nothing at all)<\/a>. ~ D. Coutts, R. Leshchinskiy, D. Stewart. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Budan_Fourier.html\">The Budan-Fourier theorem and counting real roots with multiplicity in Isabelle\/HOL<\/a>. ~ W. Li. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/jaspervdj.be\/posts\/2018-09-04-binomial-heaps-101.html\">Dependent types in Haskell: Binomial heaps 101<\/a>. ~ Jasper Van der Jeugt (@jaspervdj) #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/chrispenner.ca\/posts\/update-monad\">Update monads: Variation on state monads<\/a>. ~ Chris Penner (@chrislpenner) #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/www.well-typed.com\/blog\/2018\/09\/compositional-zooming\/\">Compositional zooming for StateT and ReaderT using lens<\/a>. ~ Edsko de Vries (@EdskoDeVries). #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/h2.jaguarpaw.co.uk\/posts\/demystifying-dlist\/\">Demystifying DList<\/a>. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1809.00508\">A logic-algebraic tool for reasoning with Knowledge-Based Systems<\/a>. ~ J.A. Alonso, G.A. Aranda, J. Borrego, M.M. Fern\u00e1ndez, M.J. Hidalgo #Logic #Math #CompSci<\/li>\n<li><a href=\"https:\/\/enablingmaths.files.wordpress.com\/2017\/12\/bundy_enabling_mathematical_cultures_v3.pdf\">Automated reasoning in the age of the Internet<\/a>. ~ A. Bundy. #ATP<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-a-formal-proof-of-the-computation-of-hermite-normal-form-in-a-general-setting\/\">Vestigium: A formal proof of the computation of Hermite normal form in a general setting<\/a> by J. Divas\u00f3n and J. Aransay. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/matt.might.net\/articles\/books-papers-materials-for-graduate-students\/\">Reading for graduate students<\/a>. Matt Might (@mattmight) #CompSci<\/li>\n<li><a href=\"http:\/\/blog.jpolak.org\/?p=2028\">My top nine favourite math texts<\/a>. ~ Jason Polak #Math<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/logic-intuitionistic\/\">Intuitionistic logic<\/a>. ~ Joan Moschovakis #Logic<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-01866271\/file\/main.pdf\">Formal verification of a geometry algorithm: A quest for abstract views and symmetry in Coq proofs<\/a>. ~ Y. Bertot. #ITP #Coq #Math #Vestigium<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1809.00738\">Categories of optics<\/a>. ~ M. Riley. #CategoryTheory #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/minad\/paripari\">Fast parser combinator library for Haskell with two strategies (Fast acceptor and slower reporter with decent error messages)<\/a>. ~ D. Mendler. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/blog.jpolak.org\/?p=1927\">A very quick tour of R<\/a>. ~ Jason Polak #Rstats<\/li>\n<li><a href=\"http:\/\/blog.jpolak.org\/?p=2027\">On reasonably sure proofs<\/a>. ~ Jason Polak #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/math\/9301202\">Theorems for a price: Tomorrow&#8217;s semi-rigorous mathematical culture<\/a>. ~ D. Zeilberger #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1808.01520.pdf\">Branching processes for QuickCheck generators<\/a>. ~ A. Mista, A. Russo, J. Hughes. #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-comparison-of-two-theorem-provers-isabelle-hol-and-coq\/\">Vestigium: Comparison of two theorem provers: Isabelle\/HOL and Coq<\/a>. #ITP #IsabelleHOL #Coq<\/li>\n<li><a href=\"https:\/\/argumatronic.com\/posts\/2018-09-02-effective-metaphor.html\">The unreasonable effectiveness of metaphor<\/a>. ~ Julie Moronuki (@argumatronic) #Math #Haskell #Linguistics<\/li>\n<li><a href=\"https:\/\/surface.syr.edu\/cgi\/viewcontent.cgi?article=1181&amp;context=eecs_techreports\">A formally veri\ufb01ed heap allocator<\/a>. ~ A. Sahebolamri, S.J. Chapin, S.D. Constable #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/uwspace.uwaterloo.ca\/bitstream\/handle\/10012\/13697\/Arteca_Ellen.pdf\">Formal semantics and mechanized soundness proof for fast gradually typed JavaScript<\/a>. ~ E. Arteca. #ITP #Coq #JavaScript<\/li>\n<li><a href=\"http:\/\/ojs.bibsys.no\/index.php\/NIK\/article\/view\/512\/436\">The pocket reasoner (automatic reasoning on small devices)<\/a>. ~ J. Otten #ATP #Prolog<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1806.03476.pdf\">Type variables in patterns<\/a>. ~ Richard A. Eisenberg, Joachim Breitner, Simon Peyton Jones. #Haskell<\/li>\n<li><a href=\"http:\/\/blog.jpolak.org\/?p=1523\">12 tips for reading math books<\/a>. ~ Jason Polak #Math<\/li>\n<li><a href=\"https:\/\/www.gaussianos.com\/el-yin-yang-y-el-numero-aureo\">El yin-yang y el n\u00famero \u00e1ureo<\/a>. ~ M.A. Morales (@gaussianos). #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/logical-truth\/\">Logical truth<\/a>. ~ M. G\u00f3mez #Logic<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/technology\/\">Philosophy of technology<\/a>. ~ M. Franssen et als. #Logic<\/li>\n<li><a href=\"https:\/\/web.math.unifi.it\/~maggesi\/papers\/2017-quaternions\/gabrielli-maggesi-quaternions-itp-2017.pdf\">Formalizing basic quaternionic analysis<\/a>. ~ A. Gabrielli, M. Maggesi #ITP #HOL_Light #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Quaternions.html\">Quaternions in Isabelle\/HOL<\/a>. ~ L.C. Paulson. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.era.lib.ed.ac.uk\/bitstream\/handle\/1842\/17863\/Papapanagiotou2014.pdf\">A formal verification approach to process modelling and composition<\/a>. ~ P. Papapanagiotou. #PhD_Thesis #ITP #HOL_Light<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1808.05490\">Correct-by-construction process composition using classical linear logic inference<\/a>. ~ P. Papapanagiotou, J. Fleuriot. #ITP #HOL_Light<\/li>\n<li><a href=\"http:\/\/slides.com\/shersh\/picnic\">Picnic: put containers into a backpack<\/a>. ~ D. Kovanikov (@ChShersh). #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/money.cnn.com\/2018\/09\/07\/technology\/darpa-artificial-intelligence\/index.html\">The Pentagon is investing $2 billion into artificial intelligence<\/a>. ~ Matt McFarland (@mattmcfarland) #AI<\/li>\n<li><a href=\"https:\/\/hotair.tech\/blog\/goodbye-vscode\/\">Goodbye VSCode, hello Emacs (again)<\/a>. ~ Bryan Willson Berry (@bryanwb) #Emacs #VSCode #JavaScript<\/li>\n<li><a href=\"https:\/\/youtu.be\/44fb3tI2Cak\">Grandes ideas de la Filosof\u00eda: L\u00f3gica<\/a>. #L\u00f3gica<\/li>\n<li><a href=\"http:\/\/ceur-ws.org\/Vol-2194\/schmid.pdf\">Inductive programming as approach to comprehensible machine learning<\/a>. ~ Ute Schmid #ILP #MachineLearnig<\/li>\n<li><a href=\"http:\/\/metatheorem.org\/includes\/pubs\/GraMSec18.pdf\">On linear logic, functional programming, and attack trees<\/a>. ~ Harley Eades III, Jiaming Jiang, and Aubrey Bryant #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/MonoidalAttackTrees\/ATLL-Formalization\">The formalization of the semantics of the attack tree linear logic<\/a>. ~ Harley D. Eades III #Agda<\/li>\n<li><a href=\"http:\/\/iltp.de\/ARQNL-2018\/download\/ARQNL2018_CEUR_Proceedings.pdf\">Automated reasoning in quantified non-classical logics<\/a>. #AutomatedReasoning<\/li>\n<li><a href=\"http:\/\/ceur-ws.org\/Vol-2095\/invited1.pdf%20\">Implementations of natural logics<\/a>. ~ Lawrence S. Moss #Logic #Sage<\/li>\n<li><a href=\"http:\/\/ceur-ws.org\/Vol-2095\/invited2.pdf\">Some thoughts about FOL-translations in Vampire<\/a>. ~ Giles Reger #AutomatedTheoremProving #Vampire<\/li>\n<li><a href=\"https:\/\/hexagoxel.de\/postsforpublish\/posts\/2018-09-09-cont-part-one.html\">Forking and ContT<\/a>. ~ Lennart Spitzner #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/davidchristiansen.dk\/tutorials\/nbe\/\">Checking dependent types with normalization by evaluation: a tutorial<\/a>. ~ David Thrane Christiansen #FunctionalProgramming #Racket<\/li>\n<li><a href=\"https:\/\/www.theverge.com\/platform\/amp\/2018\/9\/5\/17822562\/google-dataset-search-service-scholar-scientific-journal-open-data-access\">Google launches new search engine to help scientists find the datasets they need<\/a>. ~ James Vincent #DataScience<\/li>\n<li><a href=\"http:\/\/willcrichton.net\/notes\/systems-programming\/\">What is systems programming, really?<\/a> ~ Will Crichton (@wcrichton) #Programming<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/hammer-for-coq-automation-for-dependent-type-theory\/\">Vestigium: Hammer for Coq (automation for dependent type theory)<\/a>. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1809.02193\">Logical rule induction and theory learning using neural theorem proving<\/a>. ~ A. Campero et als. #MachineLearnig #AutomatedTheoremProving<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2018\/8\/27\/common-but-not-so-common-monads\">Common (but not so common) monads<\/a>. ~ James Bowen (@james_OWA) #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/bitbucket.org\/robertmassaioli\/range\">range: An efficient and versatile range library<\/a>. ~ Robert Massaioli #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/teaching\/ss18\/satsmt\/content.php\">Course: SAT\/SMT solving<\/a>. ~ S. Winkler #Logic #ATP #SAT #SMT<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/mfaerber\/documents\/thesis.pdf\">Learning proof search in proof assistants<\/a>. ~ M. F\u00e4rber #PhD_Thesis #ITP #ATP #MachineLearning<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/workspace\/publications\/JN_phdthesis_17.pdf\">Mechanizing confluence: Automated and certified analysis of first- and higher-order rewrite systems<\/a>. ~ J. Nagele #PhD_Thesis #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/upcommons.upc.edu\/bitstream\/handle\/2117\/120914\/134218.pdf\">Automatic inductive equational reasoning<\/a>. ~ J. Mas Rovira #Haskell #Logic #ATP<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/cek\/docs\/18\/jpck-itp18.pdf\">Towards formal foundations for game theory<\/a>. ~ J. Parsert and C. Kaliszyk. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/cah6.github.io\/technology\/nix-haskell-1\/\">Exploring Nix &amp; Haskell (Part 1: project setup)<\/a>. ~ Christian Henry #FunctionalProgramming #Haskell #Nix<\/li>\n<li><a href=\"http:\/\/ceur-ws.org\/Vol-2199\/paper3.pdf\">Towards Coq formalisation of {log} set constraints resolution<\/a>. ~ C. Dubois and S. Weppe. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/research.chalmers.se\/publication\/504640\/file\/504640_Fulltext.pdf\">Automated theorem proving with extensions of first-order logic<\/a>. ~ E. Kotelnikov #PhD_Thesis #ATP #Vampire #Logic<\/li>\n<li><a href=\"https:\/\/scholarsbank.uoregon.edu\/xmlui\/bitstream\/handle\/1794\/23832\/Sullivan_oregon_0171N_12267.pdf\">The essence of codata and its implementations<\/a>. ~ Z. Sullivan #MsC_Thesis #Haskell<\/li>\n<li><a href=\"https:\/\/rodrigogribeiro.github.io\/files\/regexvm-paper.pdf\">Towards certified virtual machine-based regular expression parsing<\/a>. ~ T.A. Delfino and R. Ribeiro (@rodrigogeraldo). #FunctionalProgramming #Haskell #QuickCheck<\/li>\n<li><a href=\"https:\/\/github.com\/rodrigogribeiro\/regexvm\">An operational semantics for greedy regular expression parsing<\/a>. ~ R. Ribeiro (@rodrigogeraldo). #FunctionalProgramming #Haskell #QuickCheck #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/rodrigogribeiro\/coqcourse\/raw\/master\/slides\/01_propositionsastypes.pdf\">O isomorfismo de Curry-Howard (Ou sobre a similaridade entre provas e programas)<\/a>. ~ R. Ribeiro (@rodrigogeraldo). #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/github.com\/rodrigogribeiro\/coqcourse\">Curso: Uma introdu\u00e7\u00e3o ao assistente de provas Coq<\/a>. ~ R. Ribeiro (@rodrigogeraldo). #ITP #Coq #Logic<\/li>\n<li><a href=\"https:\/\/rodrigogribeiro.github.io\/talks\/2014-04-01-agda-talk\">Programa\u00e7\u00e3o com tipos dependentes em Agda<\/a>. ~ R. Ribeiro (@rodrigogeraldo). #FunctionalProgramming #Agda<\/li>\n<li><a href=\"https:\/\/github.com\/rodrigogribeiro\/agda-software-foundations\">A translation of Pierce&#8217;s Coq book &#8220;Software foundations&#8221; to Agda<\/a>. ~ R. Ribeiro (@rodrigogeraldo). #ITP #Agda<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/cek\/docs\/17\/tgck-jsc17.pdf\">Aligning concepts across proof assistant libraries<\/a>. T. Gauthier and C. Kaliszyk. #ITP #MachineLearning<\/li>\n<li><a href=\"http:\/\/rodrigogribeiro.github.io\/files\/unify.pdf\">A mechanized textbook proof of a type unification algorithm<\/a>. ~ R. Ribeiro and C. Camar\u00e3o. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/josephcmac\/Folklore-and-miscellaneous-results-in-number-theory\">Formal verification of folklore and miscellaneous results in number theory<\/a>. ~ Jos\u00e9 Manuel Rodr\u00edguez Caballero #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/news\/231002-darpa-announces-2-billion-in-funding-for-ai-next-campaign\/fulltext\">DARPA announces $2 billion in funding for &#8216;AI next&#8217; campaign<\/a>. #AI<\/li>\n<li><a href=\"https:\/\/kenta.blogspot.com\/2018\/09\/rufudqzr-verifying-compositeness-of.html\">Verifying the compositeness of the 20th Fermat number<\/a>. ~ Ken T Takusagawa. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell\/releases\/download\/v.9.8.1\/Examenes_de_PF_con_Haskell.pdf\">Libro de ex\u00e1menes de programaci\u00f3n funcional con Haskell (versi\u00f3n del 13 de septiembre de 2018)<\/a>. #ProgramacionFuncional #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/prateekvjoshi.com\/2014\/10\/25\/a-beginners-look-at-lambda-calculus\/\">A beginner\u2019s look at lambda calculus<\/a>. ~ Prateek Joshi (@prateekvjoshi) #LambdaCalculus<\/li>\n<li><a href=\"https:\/\/blog.wuct.me\/fun-with-typed-type-level-programming-in-purescript-5f8af42cfec5\">Fun with typed type-level programming in PureScript<\/a>. ~ CT Wu (@wu_ct) #FunctionalProgramming #PureScript<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/cek\/docs\/17\/ckkp-macis17.pdf\">Isabelle formalization of set theoretic structures and set comprehensions<\/a>. ~ C. Kaliszyk and K. P\u0105k. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/github.com\/zziz\/pwc\">Papers with code: list of research papers with links to the source code, updated weekly<\/a>. ~ Zaur Fataliyev (@fvzaur). #MachineLearning<\/li>\n<li><a href=\"http:\/\/bibliotecadigital.ilce.edu.mx\/Colecciones\/ReinaCiencias\/_docs\/Introduccion_filosofia_ciencia.pdf\">Una introducci\u00f3n a la filosof\u00eda de la ciencia<\/a>. ~ R. Carnap #Filosof\u00eda #Ciencia<\/li>\n<li><a href=\"http:\/\/bibliotecadigital.ilce.edu.mx\/Colecciones\/ReinaCiencias\/_docs\/rudolfcarnapylosfundamentos.pdf\">Rudolf Carnap y los fundamentos de la l\u00f3gica y las matem\u00e1ticas<\/a>. ~ A. Church. #Filosof\u00eda #Ciencia<\/li>\n<li><a href=\"http:\/\/www.thibaultgauthier.fr\/tactictoe_jv.pdf\">TacticToe: Learning to prove with tactics<\/a>. ~ T. Gauthier et als. #ITP #HOL4 #MachineLearning<\/li>\n<li><a href=\"https:\/\/medium.com\/@cdsmithus\/the-ups-and-downs-of-stem-standards-f72df0fb6daa\">The ups and downs of STEM standards<\/a>. ~ Chris Smith (@cdsmithus) #Teaching #CompSci<\/li>\n<li><a href=\"https:\/\/dr.library.brocku.ca\/bitstream\/handle\/10464\/13646\/Thesis%20Paper%2020180904.pdf\">Modal and relevance logics for qualitative spatial reasoning<\/a>. ~ Pranab Kumar Ghosh. #Msc_Thesis #ITP #Coq #Logic<\/li>\n<li><a href=\"http:\/\/marmsoler.com\/docs\/Interactive_Verification_ADP.pdf\">A framework for interactive verification of architectural design patterns in Isabelle\/HOL<\/a>. ~ D. Marmsoler. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/jssst.or.jp\/files\/user\/taikai\/2018\/PPL\/ppl2-2.pdf\">Experimenting with monadic equational reasoning in Coq<\/a>. ~ R. Affeldt and D. Nowak. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/jssst.or.jp\/files\/user\/taikai\/2018\/PPL\/ppl3-3.pdf\">Proving tree algorithms for succinct data structures<\/a>. ~ R. Affeldt, J. Garrigue, X. Qi, Kazunari Tanaka. #ITP #Coq #Vestigium<\/li>\n<li><a href=\"http:\/\/www.haskellforall.com\/2014\/03\/introductions-to-advanced-haskell-topics.html\">Introductions to advanced Haskell topics<\/a>. ~ G. Gonzalez (@GabrielG439). #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/blog.sigfpe.com\/2006\/08\/you-could-have-invented-monads-and.html\">You could have invented Monads! (and maybe you already have)<\/a>. ~ Dan Piponi (@sigfpe) #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/page.mi.fu-berlin.de\/scravy\/realworldhaskell\/materialien\/monad-transformers-step-by-step.pdf\">Monad transformers step by step<\/a>. ~ Martin Grabm\u00fcller. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/www.cs.nott.ac.uk\/~pszgmh\/pearl.pdf\">Functional pearls: Monadic parsing in Haskell<\/a>. ~ G. Hutton, E. Meijer. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/www.haskellforall.com\/2012\/06\/you-could-have-invented-free-monads.html\">Why free monads matter<\/a>. ~ G. Gonzalez (@GabrielG439). #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/web.cecs.pdx.edu\/~mpj\/pubs\/springschool95.pdf\">Functional programming with overloading and higher-order polymorphism<\/a>. M.P. Jones. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/concrete-semantics-with-coq-and-coqhammer\">Vestigium: &#8220;Concrete semantics&#8221; with Coq and CoqHammer<\/a>. #ITP #Coq #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Octonions.html\">Octonions in Isabelle\/HOL<\/a>. ~ Angeliki Koutsoukou-Argyraki. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/twanvl.nl\/blog\/haskell\/cps-functional-references\">CPS based functional references<\/a>. ~ Twan van Laarhoven #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/matt.might.net\/articles\/compiling-up-to-lambda-calculus\/\">Compiling to lambda-calculus: Turtles all the way down<\/a>. ~ Matt Might (@mattmight). #FunctionalProgramming #LambdaCalculus<\/li>\n<li><a href=\"https:\/\/www.gaussianos.com\/extensa-coleccion-de-libros-de-matematicas\/\">Extensa colecci\u00f3n de libros de matem\u00e1ticas<\/a>. ~ M.A. Morales (@gaussianos). #Matem\u00e1ticas<\/li>\n<li><a href=\"http:\/\/www.e-booksdirectory.com\/mathematics.php\">Free mathematics books<\/a>. #eBooks #Math<\/li>\n<li><a href=\"https:\/\/www.gaussianos.com\/diez-formas-de-pensar-como-un-matematico\/\">Diez formas de pensar como un matem\u00e1tico<\/a>. ~ M.A. Morales (@gaussianos). #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-formal-verification-of-a-geometry-algorithm-a-quest-for-abstract-views-and-symmetry-in-coq-proofs\">Vestigium: Formal verification of a geometry algorithm (A quest for abstract views and symmetry in Coq proofs)<\/a>. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Aggregation_Algebras.html\">Aggregation algebras in Isabelle\/HOL<\/a>. ~ Walter Guttmann. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/medium.com\/@cdsmithus\/codeworld-update-september-17-2018-5db971ca03df\">CodeWorld update\u200a\u2014\u200aSeptember 17, 2018<\/a>. ~ Chris Smith (@cdsmithus) #FunctionalProgramming #haskell #CodeWorld<\/li>\n<li><a href=\"https:\/\/www.mattkeeter.com\/projects\/constraints\">Numeric constraint solving in Haskell<\/a>. ~ Matt Keeter (@impraxical). #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www-sop.inria.fr\/members\/Yves.Bertot\/videos-coq\/index.html\">Cours vid\u00e9o de Coq<\/a>. ~ Y. Bertot. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-proving-tree-algorithms-for-succinct-data-structures\">#Vestigium: Proving tree algorithms for succinct data structures<\/a>. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/jaycech3n\/Isabelle-HoTT\">Isabelle\/HoTT: An experimental implementation of HoTT in the interactive theorem prover Isabelle<\/a>. ~ Josh Chen (@jaycech3n). #ITP #Isabelle #IsabelleHoTT<\/li>\n<li><a href=\"https:\/\/staff.aist.go.jp\/reynald.affeldt\/documents\/coqws-reals.pdf\">Classical analysis with Coq<\/a>. ~ R. Affeldt, C. Cohen, A. Mahboubi, D. Rouhling, P.Y. Strub. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/perso.crans.org\/cohen\/CoqWS2018.pdf\">Classical analysis with Coq (Slides)<\/a>. ~ R. Affeldt, C. Cohen, A. Mahboubi, D. Rouhling, P.Y. Strub. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/coqworkshop2018.inria.fr\/files\/2018\/08\/180708-coq-workshop.pdf\">Verifying distributed systems (slides)<\/a>. ~ Zachary Tatlock. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/homes.cs.washington.edu\/~ztatlock\/pubs\/diesel-sergey-popl18.pdf\">Programming and proving with distributed protocols<\/a>. ~ I. Sergey, J.R. Wilcox, Z. Tatlock. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/coqworkshop2018.inria.fr\/files\/2018\/07\/main-34.pdf\">A Coq mechanised formal semantics for real life SQL queries: Formally reconciling SQL and (extended) relational algebra (slides)<\/a>. ~ V\u00e9ronique Benzaken and \u00c9velyne Contejean. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-01830255\/document\">A Coq mechanised formal semantics for realistic SQL queries: Formally reconciling SQL and bag relational algebra<\/a>. ~ V. Benzaken, \u00c9. Contejean #ITP #Coq<\/li>\n<li><a href=\"https:\/\/homes.cs.washington.edu\/~ztatlock\/pubs\/reincarnate-nandi-icfp18.pdf\">Functional programming for compiling and decompiling computer-aided design<\/a>. ~ C. Nandi, J.R. Wilcox, P. Panchekha, T. Blau, D. Grossman, Z. Tatlock. #FunctionalProgramming #OCaml<\/li>\n<li><a href=\"http:\/\/gallium.inria.fr\/~agueneau\/publis\/gueneau-chargueraud-pottier-coq-bigO.pdf\">A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification<\/a>. ~ A. Gu\u00e9neau, A. Chargu\u00e9raud, F. Pottier. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/coqworkshop2018.inria.fr\/files\/2018\/07\/slides-3.pdf\">Procrastination: A proof engineering technique (slides)<\/a>. ~ A. Gu\u00e9neau. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.cs.nmsu.edu\/wp\/wp-content\/uploads\/2014\/10\/TR-CS-NMSU-2014-10-24.pdf\">Exploring life through logic programming: Logic programming in bioinformatics<\/a>. ~ A. Dal Pal\u00f9, A. Dovier, A. Formisano, E. Pontelli. #LogicProgramming #ASP #Bioinformatics<\/li>\n<li><a href=\"http:\/\/thomaspietrzak.com\/download.php?f=CoursCOQ.pdf\">Introduction to Coq (slides)<\/a>. ~ T. Pietrzak. #ITP #Coq #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/affeldt\/coq-lille2016\/raw\/master\/logique-cours.pdf\">Le raisonnement logique dans l\u2019assistant de preuve Coq<\/a>. ~ R. Affeldt #ITP #Coq #Logic<\/li>\n<li><a href=\"https:\/\/coqworkshop2018.inria.fr\/files\/2018\/07\/coq2018_talk_boulme.pdf\">What is the foreign function interface of the Coq programming language? (slides)<\/a>. ~ S. Boulm\u00e9. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/coqworkshop2018.inria.fr\/files\/2018\/07\/yalla_web.pdf\">Preliminary report on the Yalla library: Yet Another deep embedding of linear logic in Coq (slides)<\/a>. ~ O. Laurent. #ITP #Coq #Logic<\/li>\n<li><a href=\"https:\/\/coqworkshop2018.inria.fr\/files\/2018\/07\/main-35.pdf\">ComplCoq: Rewrite Hint construction with completion procedures (slides)<\/a>. ~ M. Ikebuchi, K. Nakano. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/t-news.cn\/Floc2018\/FLoC2018-pages\/proceedings_paper_862.pdf\">ComplCoq: Rewrite Hint construction with completion procedures<\/a>. ~ M. Ikebuchi, K. Nakano. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/coqworkshop2018.inria.fr\/files\/2018\/07\/slides-4.pdf\">From guarded to well-founded: Formalizing Coq\u2019s guard condition (slides)<\/a>. ~ C. Mangin, M. Sozeau. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1809.05923\">What is applied category theory?<\/a> ~ Tai-Danae Bradley. #CategoryTheory<\/li>\n<li><a href=\"https:\/\/code.fb.com\/security\/fighting-spam-with-haskell\/\">Fighting spam with Haskell<\/a>. ~ Simon Marlow (@simonmar) #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/thibaultmarin.github.io\/blog\/posts\/2016-11-13-Personal_website_in_org.html\">Personal website in org<\/a>. ~ Thibault Marin. #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/theoremprover-museum.github.io\/\">The Theorem Prover Museum<\/a>. #ATP #ITP #AutomatedReasoning<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Signature_Groebner.html\">Signature-based Gr\u00f6bner basis algorithms<\/a>. ~ A. Maletzky. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.math.nagoya-u.ac.jp\/~garrigue\/papers\/JIP-26_54.pdf\">Safe low-level code generation in Coq using monomorphization and monadification<\/a>. ~ A. Tanaka, R. Affeldt, and J. Garrigue. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/hub.packtpub.com\/what-makes-functional-programming-a-viable-choice-for-artificial-intelligence-projects\">What makes functional programming a viable choice for artificial intelligence projects?<\/a> ~ Prasad Ramesh. #FunctionalProgramming #AI<\/li>\n<li><a href=\"http:\/\/philsci-archive.pitt.edu\/15034\/1\/Univalent_Foundations_and_the_UniMath_library.pdf\">Univalent foundations and the UniMath library (The architecture of mathematics)<\/a>. ~ A. Bordg. #Logic #Math #HoTT #ITP #Coq<\/li>\n<li><a href=\"https:\/\/twanvl.nl\/blog\/haskell\/simple-reflection-of-expressions\">Simple reflection of expressions<\/a>. ~ Twan van Laarhoven #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Prime_Number_Theorem.html\">The prime number theorem<\/a>. ~ M. Eberl and L.C. Paulson. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2018-09-20-agda-tips.html\">Agda tips<\/a>. ~ Donnacha Ois\u00edn Kidney (@oisdk) #ITP #Agda<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3242754\">The Thoralf plugin: for your fancy type needs<\/a>. ~ D. Otwani, R.A. Eisenberg. #FunctionalProgramming #Haskell #ATP #SMT #Z3<\/li>\n<li><a href=\"https:\/\/github.com\/Divesh-Otwani\/the-thoralf-plugin\">the-thoralf-plugin: a type-checker plugin to rule all type checker plugins involving type-equality reasoning using SMT solvers<\/a>. ~ Divesh Otwani. #FunctionalProgramming #Haskell #ATP #SMT #Z3<\/li>\n<li><a href=\"https:\/\/sras.me\/haskell\/what-the-heck-is-typeable.html\">What the heck is Typeable!?<\/a>. ~ Sandeep.C.R #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/snowleopard\/alga\">Alga: a library for algebraic construction and manipulation of graphs in Haskell<\/a>. ~ Andrey Mokhov. #Haskell<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2018\/9\/17\/simple-web-routing-with-spock\">Simple Web Routing with Spock!<\/a>. ~ James Bowen (@james_OWA) #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.westpoint.edu\/eecs\/SiteAssets\/SitePages\/Faculty%20Publication%20Documents\/Okasaki\/jfp98sixth.pdf\">Functional pearls: Even higher-order functions for parsing or why would anyone ever want to use a sixth-order function?<\/a>. ~ Chris Okasaki. #FunctionalProgramming #SML via @Iceland_jack<\/li>\n<li><a href=\"https:\/\/bitbucket.org\/josh-hs-ko\/MetamorphismsInAgda\/raw\/master\/MetamorphismsInAgda.pdf\">Programming metamorphic algorithms in Agda (Functional pearl)<\/a>. ~ Hsiang-Shang Ko. #FunctionalProgramming #ITP #Agda<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3242745\">Generic programming of all kinds<\/a>. ~ A. Serrano, V.C. Miraldo. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/www.staff.science.uu.nl\/~swier004\/publications\/2018-tyde.pdf\">From algebra to abstract machine: a verified generic construction<\/a>. ~ C. Tom\u00e9 Corti\u00f1as, W. Swierstra. #FunctionalProgramming #ITP #Agda<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3242746\">Deriving via (or, how to turn hand-written instances into an anti-pattern)<\/a>. ~ B. Bl\u00f6ndal, A. L\u00f6h, R. Scott. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3241656\">Garnishing Parsec with Parsley<\/a>. ~ J. Willis, N. Wu. #FunctionalProgramming #Scala<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2018\/09\/22\/formalising-mathematics-a-mathematicians-personal-viewpoint\">Formalising mathematics: a mathematician\u2019s personal viewpoint<\/a>. ~ Kevin Buzzard #ITP #Lean #Math<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3264739\">HELIX: a case study of a formal verification of high performance program generation<\/a>. ~ V. Zaliva, F. Franchetti. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1809.08062\">Machine-assisted proofs (ICM 2018 Panel)<\/a>. ~ J. Davenport et als. #ITP #Math<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3242752\">Coherent explicit dictionary application for Haskell<\/a>. ~ T. Winant, D. Devriese. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.maa.org\/sites\/default\/files\/images\/images\/upload_library\/22\/Ford\/Guy697-712.pdf\">The strong law of small numbers<\/a>. ~ R.K. Guy. #Math<\/li>\n<li><a href=\"http:\/\/shmish111.github.io\/2018\/09\/23\/freer-than-free\/\">Freer than free<\/a>. ~ David Smith. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/typeclasses\/assoc-list\">assoc-list: An association list conceptually signifies a mapping, but is represented as a list (of key-value pairs)<\/a>. ~ Chris Martin (@chris__martin). #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/tel.archives-ouvertes.fr\/tel-01874620\/document\">Certified algorithms for program slicing<\/a>. J.C. Le\u0301chenet. #PhD_Thesis #ITP #Coq #Why3<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1809.08304\">onlineSPARC: a programming environment for Answer Set Programming<\/a>. ~ E. Marcopoulos, Y. Zhang. #LogicProgramming #ASP<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/turing-machine\">&#8220;Turing machines&#8221;, The Stanford Encyclopedia of Philosophy<\/a>. ~ Liesbeth De Mol. #CompSci<\/li>\n<li><a href=\"https:\/\/rmonat.fr\/data\/pubs\/2018\/fmcad18.pdf\">A verified certificate checker for finite-precision error bounds in Coq and HOL4<\/a>. ~ H. Becker et als. #ITP #Coq #HOL4<\/li>\n<li><a href=\"https:\/\/kowainik.github.io\/posts\/2018-09-25-co-log\">co-log: Composable contravariant combinatorial comonadic configurable convenient logging<\/a>. ~ Dmitrii Kovanikov #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1809.09550\">A revised and verified proof of the Scalable Commutativity Rule<\/a>. ~ L. Tsai, E. Kohler, M.F. Kaashoek, N. Zeldovich. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/staffwww.dcs.shef.ac.uk\/people\/G.Struth\/mgs2015\/ISA.html\">Course: Building verification tools with Isabelle<\/a>. ~ Georg Struth. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Symmetric_Polynomials.html\">Symmetric polynomials in Isabelle\/HOL<\/a>. ~ Manuel Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/jjoekoullas.github.io\/posts\/2018-09-22-type-tetris-toolbox.html\">The Type Tetris Toolbox<\/a>. ~ J.J. Koullas (@jjoekoullas) #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/rjlipton.wordpress.com\/2018\/09\/26\/reading-into-atiyahs-proof\/\">Reading into Atiyah\u2019s proof<\/a>. ~ R.J. Lipton, K.W. Regan. #Math<\/li>\n<li><a href=\"https:\/\/skemman.is\/bitstream\/1946\/28736\/1\/msc-bjarki-2017-skemman.pdf\">Formalizing the translation method in Agda<\/a>. ~ Bjarki \u00c1g\u00fast Gu\u00f0mundsson. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/github.com\/SuprDewd\/agda-translation-method\">Translate: An Agda library for turning equations into bijections using the translation method<\/a>. ~ Bjarki \u00c1g\u00fast Gu\u00f0mundsson. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/wiki.algo.is\/\">AlgoWiki: a wiki dedicated to competitive programming<\/a>. ~ Bjarki \u00c1g\u00fast Gu\u00f0mundsson. #Programming #Algorithms<\/li>\n<li><a href=\"http:\/\/dev.stephendiehl.com\/rewrite.pdf\">Rewrite combinators<\/a>. ~ Stephen Diehl (@smdiehl). #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/cohomolo-gy\/haskell-resources\">A list of foundational Haskell papers<\/a>. ~ Emily Pillmore (@emi1ypi) #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/engineering.itpro.tv\/2018\/09\/28\/haskell-in-production-a-ghc-upgrade-success-story\/\">Haskell in production: A GHC upgrade success story<\/a>. ~ Trevis Elser (@telser). #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/owickstrom.github.io\/komposition\/\">Komposition: The video editor built for screencasters<\/a>. ~ Oskar Wickstr\u00f6m (@owickstrom). #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/SuprDewd\/T-414-AFLV\">T-414-\u00c1FLV: A competitive programming course<\/a>. ~ Bjarki \u00c1g\u00fast Gu\u00f0mundsson. #Programming #Algorithms<\/li>\n<li><a href=\"https:\/\/aperiodical.com\/2018\/09\/atiyah-riemann-hypothesis-proof-final-thoughts\/\">Atiyah Riemann Hypothesis proof: final thoughts<\/a>. ~ K. Steckles, C. Lawson-Perfect. #Math<\/li>\n<li><a href=\"http:\/\/orbit.dtu.dk\/files\/153818480\/paper_9.pdf\">Formalization of first-order syntactic unification<\/a>. ~ K.F. Brandt, A. Schlichtkrull, J. Villadsen. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/chrispenner.ca\/posts\/mock-effects-with-data-kinds\">Mocking effects using constraints and phantom data kinds<\/a>. ~ Chris Penner (@chrislpenner). #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/blog.poisson.chat\/posts\/2018-09-29-overloaded-families.html\">Overloaded type families<\/a>. ~ Xia Li-yao #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=207\">Metaheur\u00edsticas de b\u00fasquedas y optimizaci\u00f3n (Parte 1)<\/a>. ~ F. Sancho (@sanchocaparrini). #Algoritmos #IA<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=208\">Metaheur\u00edsticas de b\u00fasquedas y optimizaci\u00f3n (Parte 2)<\/a>. ~ F. Sancho (@sanchocaparrini). #Algoritmos #IA<\/li>\n<li><a href=\"https:\/\/ts.data61.csiro.au\/publications\/csiro_full_text\/\/Klein_AKMHF_toappear.pdf\">Formally verified software in the real world<\/a>. ~ G. Klein et als. #FormalVerification #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/enlightened-digital.com\/90-years-of-ai-in-the-movies-whats-changed-and-what-hasnt\/\">90 Years of AI in the movies: what\u2019s changed (and what hasn\u2019t)<\/a>. #AI<\/li>\n<li><a href=\"https:\/\/enlightened-digital.com\/ai-goes-to-the-movies-a-history-of-artificial-intelligence-in-film\/\">AI goes to the movies: A history of Artificial Intelligence in film<\/a>. #AI<\/li>\n<li><a href=\"https:\/\/towardsdatascience.com\/essential-math-for-data-science-why-and-how-e88271367fbd\">Essential Math for Data Science:\u200a&#8217;Why&#8217; and &#8216;How&#8217;<\/a>. ~ Tirthajyoti Sarkar #DataScience<\/li>\n<\/ul>\n<\/div>\n<div id=\"postamble\" class=\"status\">\n<p class=\"author\">\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante septiembre de 2018, 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":[178],"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\/6242"}],"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=6242"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6242\/revisions"}],"predecessor-version":[{"id":6246,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6242\/revisions\/6246"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6242"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6242"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6242"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}