{"id":6073,"date":"2018-01-01T12:54:47","date_gmt":"2018-01-01T11:54:47","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6073"},"modified":"2018-07-10T10:08:24","modified_gmt":"2018-07-10T08:08:24","slug":"resumen-de-lecturas-compartidas-diciembre-de-2017","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-diciembre-de-2017\/","title":{"rendered":"Resumen de lecturas compartidas (diciembre de 2017)"},"content":{"rendered":"<div id=\"content\">Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante diciembre de 2017, en <a href=\"https:\/\/twitter.com\/Jose_A_Alonso\">Twitter<\/a> 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.<br \/>\n<!--more--><\/p>\n<ul>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/sumas-de-dos-cuadrados\">Exercitium: &#8220;Sumas de dos cuadrados&#8221;<\/a>. #Haskell #I1M2017 #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/www.risc.jku.at\/research\/formal\/software\/RISCAL\/papers\/ThEdu17.pdf\">Teaching the formalization of mathematical theories and algorithms via the automatic checking of finite models<\/a>. ~ W. Schreiner, A. Brunhuemer, C. F\u00fcrst #ITP #Math #RISCAL<\/li>\n<li><a href=\"http:\/\/hojaynumeros.blogspot.com.es\/2017\/11\/numeros-piramidales-de-cuatro.html\">N\u00fameros piramidales de cuatro dimensiones<\/a>. ~ Antonio Rold\u00e1n (@Connumeros) #Matem\u00e1ticas #Programaci\u00f3n<\/li>\n<li><a href=\"http:\/\/logicaltypes.blogspot.com.es\/2017\/11\/november-2017-1haskelladay-problems-and.html\">November 2017 1HaskellADay problems and solutions<\/a>. ~ Douglas M. Auclair (@geophf) | Typed Logic #Haskell #1HaskellADay<\/li>\n<li><a href=\"http:\/\/userweb.fct.unl.pt\/~lmp\/publications\/online-papers\/lp_app_mach_ethics.pdf\">From logic programming to machine ethics<\/a>. ~ A. Saptawijaya, L.M. Pereira #LogicProgramming #KRR #AI<\/li>\n<li><a href=\"https:\/\/www.irif.fr\/~gradanne\/papers\/phdthesis.pdf\">Tierless Web programming in ML<\/a>. ~ G. Radanne #PhD_Thesis #FunctionalProgramming #OCaml<\/li>\n<li><a href=\"http:\/\/bit.ly\/2AmpaCD\">A domain specific language for drum beat programming<\/a>. ~ A.R. Du Bois, R. Ribeiro #Haskell #DSL #Music<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2017-ejercicios-de-razonamiento-detallado-sobre-programas-en-isabellehol\">RA2017: Ejercicios de razonamiento detallado sobre programas en Isabelle\/HOL<\/a>. #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2017-razonamiento-por-casos-y-por-induccion-en-isabellehol\">RA2017: Razonamiento por casos y por inducci\u00f3n en Isabelle\/HOL<\/a>. #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/i1m2017-2o-examen-de-programacion-con-haskell\">I1M2017: 2\u00ba examen de programaci\u00f3n funcional con Haskell<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/i1m2017-evaluacion-perezosa-en-haskell\">I1M2017: Evaluaci\u00f3n perezosa en Haskell<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-01639819\/document\">A formal proof in Coq of a control function for the inverted pendulum<\/a>. ~ D. Rouhling #ITP #Coq #Math #Physics<\/li>\n<li><a href=\"https:\/\/hackernoon.com\/writing-code-like-a-mathematical-proof-f5838fc27382\">Writing code like a mathematical proof<\/a>. ~ Spiro Sideris #Math #Programming<\/li>\n<li><a href=\"https:\/\/www.snoyman.com\/blog\/2016\/11\/haskell-for-dummies\">Haskell for dummies<\/a>. ~ M. Snoyman (@snoyberg) #Haskell<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-01643290\/file\/ERTS_2018_paper_59.pdf\">CompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler<\/a>. ~ D. K\u00e4stner et als. #ITP #Coq #CompCert<\/li>\n<li><a href=\"http:\/\/www.stephendiehl.com\/posts\/haskell_2018.html\">Reflecting on Haskell in 2017<\/a>. ~ Stephen Diehl (@smdiehl) #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/conjunto-de-relaciones-binarias-entre-dos-conjuntos\">Exercitium: &#8220;Conjunto de relaciones binarias entre dos conjuntos&#8221;<\/a>. #Haskell #I1M2017 #I1M2017<\/li>\n<li><a href=\"https:\/\/github.com\/jagajaga\/FP-Course-ITMO\">Slides and other materials for functional programming lectures ITMO university<\/a>. ~ D. Kovanikov, A. Seroka #Haskell<\/li>\n<li><a href=\"https:\/\/youtu.be\/Cy7jBYr3Zvc\">Point-free or die: tacit programming in Haskell and beyond<\/a>. ~ Amar Shah #Haskell<\/li>\n<li><a href=\"http:\/\/dss.in.tum.de\/files\/brandt-research\/stratset.pdf\">Voting with ties: Strong impossibilities via SAT solving<\/a>. ~ F. Brandt, C. Saile, C. Stricker #SAT_solving<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/menor-x-tal-que-los-x-multiplos-de-n-contienen-todos-los-digitos\">Exercitium: &#8220;Menor x tal que los x m\u00faltiplos de n contienen todos los d\u00edgitos&#8221;<\/a>. #Haskell #I1M2017 elementos&#8221;]]. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-01643919\/document\">A constructive formalisation of semi-algebraic sets and functions<\/a>. ~ B. Djalal #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/patternsinfp.wordpress.com\/2017\/12\/05\/arithmetic-coding\/\">Arithmetic coding<\/a>. ~ Jeremy Gibbons (@jer_gib) #Haskell #Math<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/reconocimiento-de-relaciones-funcionales-entre-dos-conjuntos\">Exercitium: &#8220;Reconocimiento de relaciones funcionales entre dos conjuntos&#8221;<\/a>. #Haskell #I1M2017 #I1M2017<\/li>\n<li><a href=\"http:\/\/www.joachim-breitner.de\/blog\/734-Finding_bugs_in_Haskell_code_by_proving_it\">Finding bugs in Haskell code by proving it<\/a>. ~ J. Breitner (@nomeata) #Haskell<\/li>\n<li><a href=\"http:\/\/blog.vmchale.com\/article\/haskell-frontend\">Using Haskell on the frontend<\/a>. ~ Vanessa McHale #Haskell<\/li>\n<li><a href=\"http:\/\/www.eldiario.es\/cultura\/tecnologia\/noticias-Reuters-escritas-programa-informatico_0_715328666.html\">La inteligencia artificial que caza noticias para Reuters en Twitter<\/a>. ~ David Sarabia (@DSRELD) #IA<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1711.04068\">Reuters Tracer: toward automated news production using large scale social media data<\/a>. ~ X. Liu et als. #AI #BigData<\/li>\n<li><a href=\"https:\/\/github.com\/dwyl\/learn-elm\">learn elm: discover why people are switching to Elm and how you can get started today!<\/a> #elm<\/li>\n<li><a href=\"http:\/\/www.microsiervos.com\/archivo\/ciencia\/bestiario-fractal-curvas.html\">Un bestiario fractal de curvas para rellenar el espacio (y el cerebro)<\/a>. ~ @Alvy #Fractales<\/li>\n<li><a href=\"http:\/\/archive.org\/stream\/BrainfillingCurves-AFractalBestiary\/BrainFilling#page\/n0\/mode\/2up\">Brainfilling curves: a fractal bestiary<\/a>. ~ Jeffrey Ventrella<\/li>\n<li><a href=\"http:\/\/www.fractalcurves.com\/\">A complete taxonomy of plane-filling curves<\/a>. ~ Jeffrey Ventrella #Fractal<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1712.01485\">Analyzing individual proofs as the basis of interoperability between proof systems<\/a>. ~ G. Dowek #ITP #Coq #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/blog.vmchale.com\/article\/integer-partitions\">Functional pearl: integer partitions and QuickCheck<\/a>. ~ Vanessa McHale #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/expresiones-equilibradas\">Exercitium: &#8220;Expresiones equilibradas&#8221;<\/a>. #Haskell #I1M2017 #I1M2017<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/secret-link-uncovered-between-pure-math-and-physics-20171201\">Secret link uncovered between pure math and physics<\/a>. ~ Kevin Hartnett #Math #Physics<\/li>\n<li><a href=\"http:\/\/revistasuma.es\/IMG\/pdf\/33-como_compartir.pdf\">C\u00f3mo compartir un secreto usando sistemas de ecuaciones lineales<\/a>. ~ A. Cano, J.M. LunA, A. Rojas #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1712.01093\">The mind as a computational system<\/a>. ~ Christoph Adami #AI<\/li>\n<li><a href=\"https:\/\/openlibra.com\/es\/book\/geometria-axiomatica\">Geometr\u00eda axiom\u00e1tica<\/a>. ~ Gerard Romo Garrido #Matem\u00e1ticas<\/li>\n<li><a href=\"http:\/\/blog.vmchale.com\/article\/sum\">Variations on a theme: A set of curated examples meant to show Haskell&#8217;s expressiveness<\/a>. ~ Vanessa McHale #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/conjunto-de-funciones-entre-dos-conjuntos\">Exercitium: &#8220;Conjunto de funciones entre dos conjuntos&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/rjlipton.wordpress.com\/2017\/12\/08\/pnp-perhaps-i-change-my-mind\">P = NP: Perhaps I change my mind<\/a>. (An old result put a new way). ~ R.J. Lipton, K.W. Regan #Math #CompSci<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/mathematicians-crack-the-cursed-curve-20171207\">Mathematicians crack the cursed curve<\/a>. ~ Kevin Hartnett #Math<\/li>\n<li><a href=\"http:\/\/www.maths.ed.ac.uk\/~cbarwick\/papers\/style.pdf\">Notes on mathematical writing<\/a>. ~ Clark Barwick #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1712.02329\">Rings: an efficient Java\/Scala library for polynomial rings<\/a>. ~ S. Poslavsky #Scala #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1611.00692v1\">Towards automatic resource bound analysis for OCaml<\/a>. ~ J. Hoffmann, A. Das, S.C. Weng #OCaml<\/li>\n<li><a href=\"https:\/\/machinethoughts.wordpress.com\/2017\/12\/08\/the-role-of-theory-in-deep-learning\">The role of theory in Deep Learning<\/a>. ~ David McAllester #AI #DeepLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1612.06526v1\">Computation in Logic and Logic in Computation<\/a>. ~ S. Salehi #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/mayusculas-y-minusculas-alternadas\">Exercitium: &#8220;May\u00fasculas y min\u00fasculas alternadas&#8221;<\/a>. #Haskell #I1M2017 #I1M2017<\/li>\n<li><a href=\"http:\/\/fixpt.de\/blog\/2017-12-04-strictness-analysis-part-1.html\">All about strictness analysis (part 1)<\/a>. ~ Sebastian Graf (@sgraf1337) #Haskell<\/li>\n<li><a href=\"https:\/\/www.matchilling.com\/introduction-to-logic-programming-with-prolog\">Introduction to logic programming with Prolog<\/a>. ~ Mathias Schilling (@MatChilling) #Prolog<\/li>\n<li><a href=\"http:\/\/blog.functorial.com\/posts\/2017-12-10-Co-Finds-A-Pairing.html\">Co finds a pairing<\/a>. ~ Phil Freeman (@paf31) #Haskell<\/li>\n<li><a href=\"https:\/\/patternsinfp.wordpress.com\/2017\/12\/11\/streaming-arithmetic-coding\/\">Streaming arithmetic coding<\/a>. ~ Jeremy Gibbons (@jer_gib) #Haskell #Math<\/li>\n<li><a href=\"https:\/\/lmcs.episciences.org\/4098\/pdf\">A framework for certified self-stabilization<\/a>. ~ S. Devismes, P. Corbineau, K. Altisen #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/jaspervdj\/talks\/blob\/master\/2017-haskell-exchange-getting-things-done\/slides.md\">Getting things done in Haskell<\/a>. ~ Jasper Van der Jeugt (@jaspervdj) #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/aplicacion-de-lista-de-funciones-a-lista-de-elementos\">Exercitium: &#8220;Aplicaci\u00f3n de lista de funciones a lista de elementos&#8221;<\/a>. #Haskell #I1M2017 #I1M2017<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1107.1130\">Dismal arithmetic<\/a>. ~ D. Applegate, M. LeBrun, N.J.A. Sloane #Math<\/li>\n<li><a href=\"https:\/\/patrickmn.com\/software\/the-haskell-pyramid\/\">The Haskell pyramid<\/a>. ~ Patrick Nielsen (@pmylund) #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/jaspervdj\/fugacious\">fugacious: An example Haskell Web application<\/a>. ~ Jasper Van der Jeugt (@jaspervdj) #Haskell<\/li>\n<li><a href=\"http:\/\/www.swmath.org\/about_contact\">swMATH: An information service for mathematical software<\/a>. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/maximo-de-las-rotaciones-restringidas\">Exercitium: &#8220;M\u00e1ximo de las rotaciones restringidas&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1712.04375\">Computational Logic: its origins and applications<\/a>. ~ L.C Paulson #Logic #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/web.engr.oregonstate.edu\/~erwig\/papers\/Monadify_SCP04.pdf\">Monadification of functional programs<\/a>. ~ M. Erwig, D. Ren #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/caminos-minimales-en-un-arbol-numerico\">Exercitium: &#8220;Caminos minimales en un \u00e1rbol num\u00e9rico&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"http:\/\/davidbkemp.github.io\/QuantumComputingArticle\">An interactive introduction to quantum computing (or what do you mean they can be both zero and one at the same time!)<\/a> ~ D. Kemp #CompSci<\/li>\n<li><a href=\"https:\/\/www.johndcook.com\/blog\/2017\/12\/12\/efficiency-is-not-associative-for-matrix-multiplication\">Efficiency is not associative for matrix multiplication<\/a>. ~ J.D. Cook @JohnDCook #Math #CompSci<\/li>\n<li><a href=\"http:\/\/wiki.di.uminho.pt\/twiki\/pub\/Education\/ACMSD\/WebHome\/acmsd1718-dh.pdf\">A brief introduction to category theory<\/a>. ~ D. Hofmann #CategoryTheory<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/i1m2017-ejercicios-de-evaluacion-perezosa-y-listas-infinitas-en-haskell-1\">I1M2017: Ejercicios de evaluaci\u00f3n perezosa y listas infinitas en Haskell (1)<\/a>. #Haskell<\/li>\n<li><a href=\"http:\/\/www.cl.cam.ac.uk\/~jrh13\/slides\/lyon-04feb14\/slides.pdf\">Applications of automated reasoning<\/a>. ~ J. Harrison #AutomatedReasoning<\/li>\n<li><a href=\"http:\/\/www.variablenotfound.com\/2011\/10\/el-tao-de-la-programacion.html\">El Tao de la programaci\u00f3n<\/a>. #Programaci\u00f3n<\/li>\n<li><a href=\"http:\/\/www.mit.edu\/~xela\/tao.html\">The Tao of programming<\/a>. #Programming<\/li>\n<li><a href=\"https:\/\/lars.hupel.info\/pub\/verified-iptables.pdf\">Verified iptables firewall analysis &amp; verification<\/a>. ~ C. Diekmann, L. Hupel, J. Michaelis, M. Haslbeck, G. Carle #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/a-tour-of-go-in-haskell.syocy.net\/en_US\/index.html\">A tour of Go in Haskell<\/a>. ~ Osanai Kazuyoshi #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/ordenacion-valle\">Exercitium: &#8220;Ordenaci\u00f3n valle&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/soupi.github.io\/rfc\/reading_simple_haskell\">Reading simple Haskell<\/a>. ~ Gil Mizrahi #Haskell<\/li>\n<li><a href=\"https:\/\/deque.blog\/2017\/12\/08\/continuation-passing-style-free-monads-and-direct-style-free-monads\/\">Continuation passing style Free Monads and direct style Free Monads<\/a>. ~ Quentin Duval @quduval #Idris<\/li>\n<li><a href=\"http:\/\/www.artfulmaths.com\/blog\/folding-christmas-fractals\">Folding Christmas fractals<\/a>. ~ Clarissa Grandi (@c0mplexnumber) #Math<\/li>\n<li><a href=\"https:\/\/turingmachinesimulator.com\/\">Online Turing machine simulator<\/a>. ~ Mart\u00edn Ugarte #CompSci #Turing<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2017-ejercicios-de-cuantificadores-sobre-listas-en-isabellehol\/\">RA2017: Ejercicios dec uantificadores sobre listas en Isabelle\/HOL<\/a>. #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2017-razonamiento-sobre-arboles-y-bosques-en-isabellehol\/\">RA2017: Razonamiento sobre \u00e1rboles y bosques en Isabelle\/HOL<\/a>. #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/i1m2017-programas-interactivos-en-haskell\/\">I1M2017: Programas interactivos en Haskell<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/i1m2017-definiciones-de-la-lista-infinita-de-factoriales-en-haskell\">I1M2017: Definiciones de la lista infinita de factoriales en Haskell<\/a>. #Haskell #Matem\u00e1ticas<\/li>\n<li><a href=\"http:\/\/iris-project.org\/pdfs\/2018-popl-runST-final.pdf\">A logical relation for monadic encapsulation of state (proving contextual equivalences in the presence of runST)<\/a>. ~ A. Timany et als. #ITP #Coq #Haskell<\/li>\n<li><a href=\"https:\/\/www.snoyman.com\/blog\/2017\/12\/what-makes-haskell-unique\">What makes Haskell unique<\/a>. ~ M. Snoyman (@snoyberg) #Haskell<\/li>\n<li><a href=\"https:\/\/ren.zone\/articles\/safe-money\">safe-money: Money in the type system where it belongs<\/a>. ~ Renzo Carbonara #Haskell<\/li>\n<li><a href=\"http:\/\/ergoemacs.org\/emacs\/emacs_org_babel_literate_programing.html\">Emacs: Org mode, programing language code markup<\/a>. ~ Xah Lee (@xah_lee) #Emacs #Programming #OrgMode<\/li>\n<li><a href=\"https:\/\/github.com\/smallhadroncollider\/taskell\">taskell: A command line task manager written in Haskell<\/a>. ~ Mark Wales #Haskell<\/li>\n<li><a href=\"http:\/\/www.logicmatters.net\/2017\/12\/14\/logic-books-of-the-year-2\/\">Logic books of the year?<\/a> ~ Peter Smith #Logic<\/li>\n<li><a href=\"https:\/\/songbird-prover.github.io\/lemma-synthesis\">SLS: Songbird + Lemma Synthesis (a separation logic prover which can automatically synthesize inductive lemmas on-the-fly)<\/a>. #ATP #OCaml<\/li>\n<li><a href=\"https:\/\/bitbucket.org\/prl_tokyo\/bigul\/raw\/logic\/POPL18\/logic.pdf\">An axiomatic basis for bidirectional programming<\/a>. ~ H.S. Ko, Z. Hu #ITP #Agda<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1708.00551\">Bonsai: synthesis-based reasoning for type systems<\/a>. ~ K. Chandra, R. Bodik #Racket<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/numero-de-viajeros-en-el-autobus\">Exercitium: &#8220;N\u00famero de viajeros en el autob\u00fas&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"http:\/\/cs.purdue.edu\/~rompf\/papers\/amin-draft2017a.pdf\">Collapsing towers of interpreters<\/a>. ~ N. Amin, T. Rompf #Lisp #Scala<\/li>\n<li><a href=\"https:\/\/github.com\/ndmitchell\/debug\">Debug: Haskell library for debugging<\/a>. ~ Neil Mitchell #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/owickstrom\/fast-and-fearless-evolution-of-server-side-webapps\">Fast and fearless evolution of server-side Web applications<\/a>. ~ Oskar Wickstr\u00f6m (@owickstrom) #Haskell<\/li>\n<li><a href=\"https:\/\/sinews.siam.org\/Details-Page\/a-water-based-solution-of-polynomial-equations\">A water-based solution of polynomial equations<\/a>. ~ Mark Levi #Math<\/li>\n<li><a href=\"http:\/\/andreipopescu.uk\/pdf\/conserv_HOL_IsabelleHOL.pdf\">Safety and conservativity of definitions in HOL and Isabelle\/HOL<\/a>. ~ O. Kun\u010dar, A. Popescu #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Knuth_Morris_Pratt.html\">The string search algorithm by Knuth, Morris and Pratt in Isabelle\/HOL<\/a>. ~ F. Hellauer, P. Lammich #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/blog.ramdoot.in\/monadic-do-block-yet-again-a98cf0237b25\">Monadic &#8220;do&#8221; block, yet again (What should get into your &#8220;do&#8221; block?)<\/a> ~ Arvind Devarajan #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/reconocimiento-de-recorridos-correctos\">Exercitium: &#8220;Reconocimiento de recorridos correctos&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/codurance.com\/2017\/12\/14\/lambda-calculus-in-clojure\">Lambda calculus in Clojure (part 1)<\/a>. ~ Sergio Rodrigo Royo #LambdaCalculus #Clojure<\/li>\n<li><a href=\"https:\/\/clementd-files.cellar-c2.services.clever-cloud.com\/scala-io-haskell.html#1.0\">Haskell in production in a startup in 2017? Yup<\/a>. ~ Fr\u00e9d\u00e9ric Menou (@ptit_fred), Cl\u00e9ment Delafargue (@clementd) #Haskell<\/li>\n<li><a href=\"https:\/\/futtetennismo.me\/posts\/algorithms-and-data-structures\/2017-12-08-functional-graphs.html\">Functional programming with graphs<\/a>. ~ @futtetennista #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1712.06587\">Solving satisfiability using inclusion-exclusion<\/a>. ~ A. Zaleski #Logic #Sat #Maple<\/li>\n<li><a href=\"https:\/\/github.com\/haskell-perf\/checklist\/blob\/master\/README.md\">The Haskell performance checklist<\/a>. ~ Chris Done (@christopherdone) #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/arbol-de-recorridos-del-autobus\">Exercitium: &#8220;Bosque de recorridos del autob\u00fas&#8221;<\/a>. #Haskell #I1M2017 #I1M2017<\/li>\n<li><a href=\"https:\/\/github.com\/haskell-perf\/numbers\">Benchmarks for numbers: ints, doubles, bignums, rationals, etc.<\/a> ~ Chris Done (@christopherdone) #Haskell<\/li>\n<li><a href=\"https:\/\/ucsd-progsys.github.io\/liquidhaskell-blog\/2017\/12\/15\/splitting-and-splicing-intervals-I.lhs\">Splitting and splicing intervals (part 1)<\/a>. ~ R. Jhala (@RanjitJhala) #Haskell #LiquidHaskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/2DfofTS\">De Lutero a Voevodsky, pasando por Brouwer: Reformas en matem\u00e1ticas<\/a>. ~ J. Ferreir\u00f3s #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/aplicaciones-biyectivas\">Exercitium: &#8220;Aplicaciones biyectivas&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/i1m2017-representacion-grafica-de-funciones-en-haskell-con-gnuplot\">I1M2017: Representaci\u00f3n gr\u00e1fica de funciones en Haskell con GNUplot<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/i1m2017-programacion-de-dibujos-por-comprension-en-codeworldhaskell\">I1M2017: Programaci\u00f3n de dibujos por comprensi\u00f3n en CodeWorld\/Haskell<\/a>. #Haskell #CodeWorld<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/i1m2017-programacion-de-dibujos-por-recursion-en-codeworldhaskell\/\">I1M2017: Programaci\u00f3n de dibujos por recursi\u00f3n en CodeWorld\/Haskell<\/a>. #Haskell #CodeWorld<\/li>\n<li><a href=\"https:\/\/jfr.unibo.it\/article\/download\/7235\/7332\">A library for algorithmic game theory in Ssreflect\/Coq<\/a>. ~ A. Bagnall, S. Merten, G. Stewart #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.fpcomplete.com\/blog\/2017\/12\/building-haskell-apps-with-docker\">Building Haskell apps with Docker<\/a>. ~ D. Bertovic #Haskell via @FPComplete<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/menor-con-suma-de-digitos-dada\">Exercitium: &#8220;Menor con suma de d\u00edgitos dada&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"http:\/\/www.tweag.io\/posts\/2017-12-21-reflection-tutorial.html\">All about reflection: a tutorial<\/a>. ~ A. Spiwack #Haskell<\/li>\n<li><a href=\"http:\/\/kvardek-du.kerno.org\/2017\/12\/a-lisp-repl-in-your-pocket.html\">A Lisp REPL in your pocket<\/a>. ~ Kvardek Du #Lisp #Android<\/li>\n<li><a href=\"http:\/\/dev.stephendiehl.com\/types_behavior.pdf\">Reasoning about program behavior algebraically<\/a>. ~ Stephen Diehl (@smdiehl) #Haskell<\/li>\n<li><a href=\"https:\/\/medium.com\/@danrobinson\/understanding-simplicity-implementing-a-smart-contract-language-in-30-lines-of-haskell-827521bfeb4d\">Understanding simplicity: implementing a smart contract language in 30 lines of Haskell<\/a>. ~ Dan Robinson #Haskell<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/news\/223727-evolutionary-programming-converts-darwinism-into-algorithms\/fulltext\">Evolutionary programming converts darwinism into algorithms<\/a>. ~ R. Colin Johnson #Programming #AI<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Mason_Stothers.html\">The Mason\u2013Stother&#8217;s theorem<\/a>. ~ Manuel Eberl #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/blog.infinitenegativeutility.com\/2017\/12\/some-notes-about-how-i-write-haskell\">Some notes about how I write Haskell<\/a>. ~ Getty Ritter (@aisamanra) #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/cadenas-opuestas\">Exercitium: &#8220;Cadenas opuestas&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/github.com\/c-cube\/zipperposition\">Zipperposition: An automatic theorem prover in OCaml for typed logic with equality, datatypes and arithmetic<\/a>. ~ Simon Cruanes #OCaml #ATP #Logic<\/li>\n<li><a href=\"http:\/\/cedeela.fr\/~simon\/files\/thesis.pdf\">Extending superposition with integer arithmetic, structural induction, and beyond<\/a>. ~ Simon Cruanes #PhD_Thesis #OCaml #ATP #Logic<\/li>\n<li><a href=\"http:\/\/www.microsiervos.com\/archivo\/ordenadores\/programas-artistico-matematicos-280-caracteres.html\">Programas art\u00edstico-matem\u00e1ticos en menos de 280 caracteres<\/a>. ~ @Alvy #Programaci\u00f3n #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/introduction-to-singletons-1.html\">Introduction to singletons (Part 1)<\/a>. ~ Justin Le (@mstk) #Haskell<\/li>\n<li><a href=\"http:\/\/atcm.mathandtech.org\/EP2017\/contributed\/4202017_21470.pdf\">On possible use of quantifier elimination software in upper secondary mathematics education<\/a>. ~ Y. Sato, R. Fukasaku #Math #Logic<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Median_Of_Medians_Selection.html\">The median-of-medians selection algorithm<\/a>. ~ Manuel Eberl #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/vecino-en-lista-circular\">Exercitium: &#8220;Vecino en lista circular&#8221;<\/a>. #Haskell #I1M2017 primos&#8221;]]. #Haskell #I1M2017<\/li>\n<li><a href=\"http:\/\/www2.ing.unipi.it\/~a009435\/issw\/extra\/cosim-cps_cr.pdf\">Integrated simulation and formal verification of a simple autonomous vehicle<\/a>. ~ A_ Domenici, A. Fagiolini, M. Palmieri #Formal_verification #ITP #PVS<\/li>\n<li><a href=\"https:\/\/github.com\/serokell\/importify\">importify: manage Haskell imports quickly<\/a>. ~ Dmitry Kovanikov et als. #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/suma-de-las-hojas-de-minimo-nivel\">Exercitium: &#8220;Suma de las hojas de m\u00ednimo nivel&#8221;<\/a>. #Haskell #I1M2017 #Haskell #I1M2017<\/li>\n<li><a href=\"http:\/\/homerhanumat.com\/r-notes\/r-notes.pdf\">Beginning Computer Science with R<\/a>. ~ H. White #CompSci #Rstats<\/li>\n<li><a href=\"https:\/\/github.com\/sdiehl\/protolude\">Protolude: A sensible starting Prelude for building custom Preludes<\/a>. ~ Stephen Diehl (@smdiehl) #Haskell<\/li>\n<li><a href=\"http:\/\/sketis.net\/wp-content\/uploads\/2017\/12\/Isabelle_Scaling_Dec-2017.pdf\">Scaling Isabelle proof document processing<\/a>. ~ M. Wenzel #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/sumable-sin-vecinos\">Exercitium: &#8220;Sumable sin vecinos&#8221;<\/a>. #Haskell #I1M2017.<\/li>\n<li><a href=\"https:\/\/bookdown.org\/chesterismay\/rbasics\/\">Getting used to R, RStudio, and R Markdown<\/a>. ~ C. Ismay #Rstats<\/li>\n<li><a href=\"https:\/\/www.r-bloggers.com\/tiny-art-in-less-than-280-characters\">Tiny art in less than 280 characters<\/a>. ~ Antonio S. Chinch\u00f3n (@aschinchon) #Rstats<\/li>\n<li><a href=\"https:\/\/aschinchon.github.io\/estalmat_2017\/#1\">Programar (en R) te da alas<\/a>. ~ Antonio S. Chinch\u00f3n (@aschinchon) #Rstats<\/li>\n<li><a href=\"https:\/\/hugo.feree.fr\/cpp2018.pdf\">Formal proof of polynomial-time complexity with quasi-interpretations<\/a>. ~ H. F\u00e9r\u00e9e et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/rotaciones-divisibles-por-8\">Exercitium: &#8220;Rotaciones divisibles por 8&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/jfr.unibo.it\/article\/download\/7235\/7332\">A library for algorithmic game theory in Ssreflect\/Coq<\/a>. ~ A- Bagnall, S. Merten, G. Stewart #ITP #Coq<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-01656404\/file\/final_version_plas17_cabon_schmitt.pdf\">Annotated multisemantics to prove Non-Interference analyses<\/a>. ~ G. Cabon, A. Schmitt #ITP #Coq<\/li>\n<\/ul>\n<\/div>\n<div id=\"postamble\"><\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante diciembre de 2017, en Twitter 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.<\/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\/6073"}],"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=6073"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6073\/revisions"}],"predecessor-version":[{"id":6157,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6073\/revisions\/6157"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6073"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6073"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6073"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}