{"id":6077,"date":"2018-02-01T13:01:47","date_gmt":"2018-02-01T12:01:47","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6077"},"modified":"2018-07-10T10:07:50","modified_gmt":"2018-07-10T08:07:50","slug":"resumen-de-lecturas-compartidas-enero-de-2018","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-enero-de-2018\/","title":{"rendered":"Resumen de lecturas compartidas (enero de 2018)"},"content":{"rendered":"<div>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante enero de 2018, en <a href=\"https:\/\/twitter.com\/Jose_A_Alonso\">Twitter<\/a> sobre programaci\u00f3n funcional y demostraci\u00f3n asistida por ordenador fundamentalmente.<\/div>\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\/posiciones-de-las-mayusculas\">Exercitium: &#8220;Posiciones de las may\u00fasculas&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/sucesion-de-raices-enteras-de-los-numeros-primos\">Exercitium: &#8220;Sucesi\u00f3n de ra\u00edces enteras de los n\u00fameros primos&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/recorrido-por-niveles-de-arboles-binarios\">Exercitium: &#8220;Recorrido por niveles de \u00e1rboles binarios&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"http:\/\/books.goalkicker.com\/HaskellBook\">Haskell notes for professionals book<\/a>. #eBook #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1712.09288\">An extensible ad hoc interface between Lean and Mathematica<\/a>. ~ R.Y. Lewis #ITP #Lean #Mathematica<\/li>\n<li><a href=\"https:\/\/markkarpov.com\/tutorial\/th.html\">Template Haskell tutorial<\/a>. ~ M. Karpov (@mrkkrp) #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/factorial-modulo\">Exercitium: &#8220;Factorial m\u00f3dulo&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=189\">Algoritmo de Monte Carlo aplicado a b\u00fasquedas en espacios de estados<\/a>. ~ F. Sancho (@sanchocaparrini) #IA<\/li>\n<li><a href=\"https:\/\/github.com\/A1kmm\/proofsweeper\">ProofSweeper: Play Minesweeper by formally proving your moves in Idris<\/a>. ~ Andrew Miller #Idris #Haskell<\/li>\n<li><a href=\"https:\/\/m-renaud-haskell-containers.readthedocs.io\/en\/docs\/\">Haskell containers package<\/a>. ~ Matt Renaud #Haskell<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Falling_Factorial_Sum.html\">The falling factorial of a sum<\/a>. ~ L. Bulwahn #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/ordenacion-segun-una-cadena\">Exercitium: &#8220;Ordenaci\u00f3n seg\u00fan una cadena&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2017-panorama-de-la-demostracion-asistida-por-ordenador\/\">RA2017: Panorama de la demostraci\u00f3n asistida por ordenador<\/a>. #Prover9 #ACL2 #PVS #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/i1m2017-manejo-de-ficheros-en-haskell\/\">I1M2017: Manejo de ficheros en Haskell<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/matthias-endler.de\/2018\/functional-mathematics\/\">Functional programming for mathematical computing<\/a>. ~ Matthias Endler (@matthiasendler) #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell\/raw\/master\/Examenes_de_PF_con_Haskell.pdf\">Libro de ex\u00e1menes de programaci\u00f3n funcional con Haskell (versi\u00f3n del 6 de enero de 2018)<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/www.math.wisc.edu\/~miller\/old\/m771-10\/kunen770.pdf\">The foundations of mathematics<\/a>. ~ K. Kunen #eBook #Logic #Math<\/li>\n<li><a href=\"http:\/\/comonad.com\/reader\/2018\/the-state-comonad\/\">Is State a Comonad?<\/a> ~ Edward Kmett (@kmett) #Haskell<\/li>\n<li><a href=\"https:\/\/pron.github.io\/posts\/computation-logic-algebra-pt1\">Finite of sense and infinite of thought: a history of computation, logic and algebra, part I<\/a>. ~ Ron Pressler #Logic #Math #CompSci<\/li>\n<li><a href=\"https:\/\/raywang.tech\/2017\/12\/20\/Formal-Verification:-The-Gap-between-Perfect-Code-and-Reality\">Formal verification: the gap between perfect code and reality<\/a>. ~ Ray Wang #Formal_methods<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/numeros-apocalipticos\">Exercitium: N\u00fameros apocal\u00edpticos<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/media.ccc.de\/v\/34c3-9105-coming_soon_machine-checked_mathematical_proofs_in_everyday_software_and_hardware_development\">Coming soon: machine-checked mathematical proofs in everyday software and hardware development<\/a>. ~ Adam Chlipala #ITP<\/li>\n<li><a href=\"http:\/\/ace.cs.ohio.edu\/~gstewart\/papers\/snaarkl.pdf\">Sn\u00e5rkl: Somewhat practical, pretty much declarative verifiable computing in Haskell<\/a>. ~ G. Stewart, S. Merten, L. Leland #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1801.00471\">TWAM: A certifying abstract machine for logic programs<\/a>. ~ B. Bohrer, K. Crary #ITP #LF<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Kuratowski_Closure_Complement.html\">The Kuratowski closure-complement theorem in Isabelle\/HOL<\/a>. ~ P. Gammie, G. Gioiosa #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/enumeracion-de-los-numeros-enteros\">Exercitium: Enumeraci\u00f3n de los n\u00fameros enteros<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"http:\/\/kaygun.tumblr.com\/post\/169392012379\/the-shoelace-formula-for-the-area-of-a-polygon\">The Shoelace formula for the area of a polygon<\/a>. ~ Atabey Kaygun (@Atabey_Kaygun) #CommonLisp #Math<\/li>\n<li><a href=\"https:\/\/blog.merovius.de\/2018\/01\/08\/monads-are-just-monoids.html\">Monads are just monoids in the category of endofunctors<\/a>. ~ Axel Wagner (@TheMerovius) #Haskell #Math<\/li>\n<li><a href=\"https:\/\/medium.freecodecamp.org\/10-awkward-moments-in-math-history-d364706d902d\">10 awkward moments in math history<\/a>. ~ Elena Nisioti (@elennisioti1) #Math #History<\/li>\n<li><a href=\"https:\/\/github.com\/joom\/hezarfen\">Hezarfen: a theorem prover for intuitionistic propositional logic in Idris<\/a>. ~ Joomy Korkut #Idris #Haskell #Logic<\/li>\n<li><a href=\"https:\/\/m.magnet.xataka.com\/preguntas-no-tan-frecuentes\/las-universidades-de-eeuu-al-fin-lo-han-reconocido-empezar-a-programar-por-java-es-una-mala-idea\">Las universidades de EEUU al fin lo han reconocido: empezar a programar por Java es una mala idea<\/a>. ~ Esther Miguel Trula<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/ejercicios\/ejercicios-I1M-2017.pdf\">Libro con las soluciones de las 16 primeras relaciones de ejercicios de programaci\u00f3n con Haskell<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/numeros-somirp\">Exercitium: N\u00fameros somirp<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/medium.com\/@ptitfred\/haskell-and-fp-a83b5b22f67f\">Haskell et programmation fonctionnelle, ma conviction<\/a>. ~ Fr\u00e9d\u00e9ric Menou (@ptit_fred) #Haskell<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Taylor_Models.html\">A formally verified implementation of multivariate Taylor models in Isabelle\/HOL<\/a>. ~ C. Traut, F. Immler #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/ordenacion-por-frecuencia\">Exercitium: Ordenaci\u00f3n por frecuencia<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/numeros-malvados-y-odiosos\">Exercitium: N\u00fameros malvados y odiosos<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Green.html\">An Isabelle\/HOL formalisation of Green&#8217;s theorem<\/a>. ~ M. Abdulaziz, L.C. Paulson #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/introduction-to-singletons-2.html\">Introduction to Singletons (Part 2)<\/a>. ~ Justin Le (@mstk) #Haskell<\/li>\n<li><a href=\"https:\/\/openlibra.com\/es\/book\/a-friendly-introduction-to-mathematical-logic\">A friendly introduction to mathematical logic<\/a>. ~ Christopher C. Leary #eBook #Logic<\/li>\n<li><a href=\"https:\/\/jeremykun.com\/2017\/12\/29\/np-hard-does-not-mean-hard\/\">NP-hard does not mean hard<\/a>. ~ Jeremy Kun (@jeremyjkun) | Math \u2229 Programming #CompSci<\/li>\n<li><a href=\"http:\/\/oeuf.uwplse.org\/oeuf-cpp18.pdf\">\u0152uf: Minimizing the Coq extraction TCB<\/a>. ~ E. Mullen et als. #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/conal\/talk-2018-essence-of-ad\">The simple essence of automatic differentiation<\/a>. ~ Conal Elliott (@conal) #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/leftaroundabout\/linearmap-family\">linearmap-family: Purely-functional, coordinate-free linear algebra<\/a>. ~ Justus Sagem\u00fcller #Haskell #Math<\/li>\n<li><a href=\"https:\/\/github.com\/mandubian\/neurocat\">From neural networks to the Category of composable supervised learning algorithms in Scala with compile-time matrix checking based on singleton-types<\/a>. ~ Pascal Voitot (@mandubian) #Scala<\/li>\n<li><a href=\"https:\/\/docs.google.com\/presentation\/d\/1Zc2A7nkpuxnCRlILPeKRJCWIqv-gtsMJIizDQ9a3vPo\">CodeWorld: The why, what, and how of teaching Haskell to children<\/a>. ~ Chris Smith #Haskell<\/li>\n<li><a href=\"http:\/\/blog.stephenwolfram.com\/2016\/09\/how-to-teach-computational-thinking\">How to teach computational thinking<\/a>. ~ Stephen Wolfram #Teaching #CompSci<\/li>\n<li><a href=\"https:\/\/blogs.ams.org\/matheducation\/2017\/01\/09\/integrating-computer-science-in-math-the-potential-is-great-but-so-are-the-risks\">Integrating computer science in math: the potential is great, but so are the risks<\/a>. ~ Emmanuel Schanzer #Teaching #CompSci #Math<\/li>\n<li><a href=\"http:\/\/www.bootstrapworld.org\/\">Bootstrap<\/a>: a research project at Brown University that offers a series of curricular modules built around purely mathematical programming. #Teaching #CompSci #Math<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/sumas-parciales-de-nicomaco\">Exercitium: Sumas parciales de Nic\u00f3maco<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"http:\/\/publicdomainreview.org\/2016\/11\/10\/let-us-calculate-leibniz-llull-and-computational-imagination\">&#8220;Let us calculate!&#8221;: Leibniz, Llull, and the computational imagination<\/a>. ~ Jonathan Gray<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1801.04163\">A tableaux calculus for reducing proof size<\/a>. ~ M.P. Lettmann, N. Peltier #Logic #ATP<\/li>\n<li><a href=\"http:\/\/wiki.science.ru.nl\/tfpie\/images\/3\/32\/Alegre.pdf\">Haskell in middle and high school mathematics<\/a>. ~ F. Alegre, J. Moreno #Haskell #Math<\/li>\n<li><a href=\"https:\/\/github.com\/alphalambda\/k12math\">Mathematics for middle and high school in Haskell<\/a>. #Haskell #Math<\/li>\n<li><a href=\"https:\/\/codurance.com\/2018\/01\/11\/applicatives-validation\">Applicative functors and data validation, part II<\/a>. ~ Carlos Morera de la Chica #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/enumeracion-de-los-numeros-enteros\/\">Exercitium: &#8220;Enumeraci\u00f3n de los n\u00fameros enteros&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-01673518\/file\/dissertation.pdf\">Extending higher-order logic with predicate subtyping: application to PVS<\/a>. ~ Fr\u00e9d\u00e9ric Gilbert #ITP #PVS<\/li>\n<li><a href=\"http:\/\/www.cs.nott.ac.uk\/~psxjb5\/publications\/2017-BrackerNilsson-SupermonadsAndSuperapplicatives-UnderConsideration.pdf\">Supermonads and superapplicatives<\/a>. ~ J. Bracker, H. Nilsson #Haskell #Agda<\/li>\n<li><a href=\"http:\/\/rewriting.gforge.inria.fr\/1-33\/main.pdf\">Lecture notes on rewriting theory<\/a>. ~ F. Blanqui<\/li>\n<li><a href=\"http:\/\/www.ssrg.nicta.com.au\/publications\/csiro_full_text\/Amani_BSB_18.pdf\">Towards verifying Ethereum smart contract bytecode in Isabelle\/HOL<\/a>. ~ S. Amani, M. B\u00e9gel, M. Bortin, M. Staples #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/youtu.be\/X_jVcWEgp4A\">Gu\u00eda tur\u00edstica de Sevilla con Scratch<\/a>. ~ @programamos #Scratch<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/numeros-somirp\">Exercitium: &#8220;N\u00fameros somirp&#8221;<\/a>. #Haskell #I1M2017 #I1M2017<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/cek\/docs\/18\/jpck-cpp18.pdf\">Formal microeconomic foundations and the First Welfare Theorem<\/a>. ~ C. Kaliszyk, J. Parsert #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/homes.cs.washington.edu\/~emina\/blog\/2017-06-23-a-primer-on-sat.html\">A primer on boolean satisfiability<\/a>. ~ Emina Torlak #Logic #SAT #Racket via @ozanerdem<\/li>\n<li><a href=\"https:\/\/courses.cs.washington.edu\/courses\/cse507\/17wi\/calendar.html\">Course: Computer-aided reasoning for software<\/a>. ~ E. Torlak #AutomatedReasoning #Logic<\/li>\n<li><a href=\"https:\/\/lamp.epfl.ch\/files\/content\/sites\/lamp\/files\/teaching\/progfun\/slides\/week1-1-annot.pdf\">Functional programming principles in Scala<\/a>. ~ Martin Odersky #FunctionalProgramming #Scala<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/ordenacion-por-frecuencia\">Exercitium: &#8220;Ordenaci\u00f3n por frecuencia&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"http:\/\/www.cs.unc.edu\/~amos\/data\/csci2017-isse.pdf\">Formalizing data management systems: a case study of Syndicate protocol<\/a>. ~ C.K. Wang, H. Xu #ITP #Coq<\/li>\n<li><a href=\"http:\/\/comonad.com\/reader\/2018\/computational-quadrinitarianism-curious-correspondences-go-cubical\/\">Computational Quadrinitarianism (Curious Correspondences go Cubical)<\/a>. ~ Gershom Bazerman #CompSci<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1801.05423\">A random walk through experimental mathematics<\/a>. ~ E.Y.S. Chan, R.M. Corless #Math #Programming<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/teaching\/ws17\/fp\/pdfs\/lambda.pdf\">\u03bb-calculus<\/a>. ~ Christian Sternagel #Logic #Haskell #CompSci<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/numeros-malvados-y-odiosos\">Exercitium: &#8220;N\u00fameros malvados y odiosos&#8221;<\/a>. #Haskell #I1M2017 #I1M2017<\/li>\n<li><a href=\"http:\/\/www.cs.princeton.edu\/~olivierb\/papers\/shrink.pdf\">Shrink fast correctly!<\/a> ~ Olivier Savary B\u00e9langer, Andrew W. Appel #ITP #Coq<\/li>\n<li><a href=\"http:\/\/kaygun.tumblr.com\/post\/169730814509\/hofstadters-q-sequence\">Hofstadter\u2019s Q sequence<\/a>. ~ Atabey Kaygun (@Atabey_Kaygun) #CommonLisp #Math<\/li>\n<li><a href=\"http:\/\/admission.cs.cityu.edu.hk\/CommonMyths\">Ten common myths about Computer Science<\/a>. #CompSci<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/teaching\/ws17\/fp\/pdfs\/reasoning.pdf\">Reasoning about functional programs<\/a>. ~ Christian Sternagel #Logic #Haskell<\/li>\n<li><a href=\"https:\/\/avigad.github.io\/formal_methods_in_education\">Resources for teaching with formal methods<\/a>. ~ Jeremy Avigad #FormalMethods<\/li>\n<li><a href=\"http:\/\/arg.ciirc.cvut.cz\/fmpa\/slides\/intro1.pdf\">Computer understandable mathematics<\/a>. ~ Josef Urban #ATP #ITP #Math<\/li>\n<li><a href=\"https:\/\/repositorio.inesctec.pt\/bitstream\/123456789\/5441\/1\/P-00M-T6A.pdf\">The specification and analysis of use properties of a nuclear control system<\/a>. ~ M.D. Harrison, P.M. Masci, J. Creissac Campos and P. Curzon #ITP #PVS<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/teaching\/ws17\/fp\/pdfs\/efficiency.pdf\">Efficiency of functional programs<\/a>. ~ Christian Sternagel and Harald Zankl #Haskell<\/li>\n<li><a href=\"http:\/\/www.cl.cam.ac.uk\/~jrh13\/papers\/joerg.pdf\">History of interactive theorem proving<\/a>. ~ John Harrison, Josef Urban and Freek Wiedijk #ITP<\/li>\n<li><a href=\"https:\/\/es.slideshare.net\/TiinaPartanen\/computational-thinking-as-an-emergent-learning-trajectory-of-mathematics\">Computational thinking as an emergent learning trajectory of mathematics<\/a>. ~ Tiina Partanen #Math #CompSci<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/tel-01680213\/document\">Verification of a concurrent garbage collector<\/a>. ~ Yannick Zakowski #PhDThesis #ITP #Coq<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/teaching\/ws17\/fp\/pdfs\/typing.pdf\">Typing of functional programs<\/a>. ~ Christian Sternagel #Logic #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/programamos.es\/creando-un-videojuego-paso-a-paso-con-scratch-desde-cero\">Creando un videojuego paso a paso con Scratch desde cero<\/a>. ~ Jes\u00fas Moreno Le\u00f3n (@J_MorenoL) #Scratch<\/li>\n<li><a href=\"https:\/\/coda.wickstrom.tech\/episodes\/2018-01-19-domain-modelling-with-haskell-data-structures.html\">Domain modelling with Haskell: data structures<\/a>. ~ Oskar Wickstr\u00f6m #Haskell<\/li>\n<li><a href=\"https:\/\/popl18.sigplan.org\/event\/plmw-popl-2018-liquidhaskell-overview\">Liquid Haskell: refinement types for Haskell<\/a>. ~ Niki Vazou (@nikivazou) #Haskell #LiquidHaskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/sumas-parciales-de-nicomaco\">Exercitium: &#8220;Sumas parciales de Nic\u00f3maco&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1801.05206\">Sequences, yet functions: the dual nature of data-stream processing<\/a>. ~ S. Herbst, J. Tenschert, A.M. Wahl, K. Meyer-Wegener #ITP #Coq<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/teaching\/ws17\/fp\/content.php\">Course: Functional programming<\/a>. ~ Christian Sternagel et als. #Haskell<\/li>\n<li><a href=\"https:\/\/dbp.io\/essays\/2018-01-16-how-to-prove-a-compiler-correct.html\">How to prove a compiler correct<\/a>. ~ Daniel Patterson #Haskell<\/li>\n<li><a href=\"http:\/\/ozark.hendrix.edu\/~yorgey\/pub\/explaining-errors-slides.pdf\">Explaining type errors<\/a>. ~ B. Yorgey, R. Eisenberg, H. Eades #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/fractal-hexagonal\">Exercitium: &#8220;Fractal hexagonal&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1801.04026\">Relational characterisations of paths<\/a>. ~ R. Berghammer, H. Furusawa, W. Guttmann, P. H\u00f6fner #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2018\/1\/22\/functors-done-quick\">Functors done quick!<\/a> ~ James Bowen (@james_OWA) #Haskell<\/li>\n<li><a href=\"https:\/\/programamos.es\/laberinto-principiantes\">Programando un laberinto con Scratch, \u00a1para principiantes!<\/a> ~ Alejandra S\u00e1nchez Acosta #Scratch v\u00eda @programamos<\/li>\n<li><a href=\"https:\/\/popl18.sigplan.org\/event\/plmw-popl-2018-dafny-overview\">Dafny overview<\/a>. ~ K. Rustan M. Leino #Dafny<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/interpreters-a-la-carte-duet.html\">&#8220;Interpreters a la Carte&#8221; in Advent of Code 2017 Duet<\/a>. ~ Justin Le (@mstk) #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/numeros-como-diferencias-de-potencias\">Exercitium: &#8220;N\u00fameros como diferencias de potencias&#8221;<\/a>. #Haskell #I1M2017 #I1M2017<\/li>\n<li><a href=\"http:\/\/matryoshka.gforge.inria.fr\/pubs\/rp_paper.pdf\">Formalization of Bachmair and Ganzinger&#8217;s ordered resolution prover<\/a>. ~ A. Schlichtkrull, J.C. Blanchette, D. Traytel and U. Waldmann (<a href=\"https:\/\/www.isa-afp.org\/entries\/Ordered_Resolution_Prover.html\">Code<\/a>) #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/eli.thegreenplace.net\/2018\/haskell-functions-as-functors-applicatives-and-monads\">Haskell functions as functors, applicatives and monads<\/a>. ~ Eli Bendersky (@elibendersky) #Haskell<\/li>\n<li><a href=\"https:\/\/argumatronic.com\/posts\/2018-01-23-the-nesting-instinct.html\">The nesting instinct<\/a>. ~ Julie Moronuki (@argumatronic) #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1801.06566\">Model theory and machine learning<\/a>. ~ H. Chase, J. Freitag #Logic #AI<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/escalada-hasta-un-primo\">Exercitium: &#8220;Escalada hasta un primo&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1801.07528\">Computer-assisted proving of combinatorial conjectures over finite domains: a case study of a chess conjecture<\/a>. ~ P. Jani\u010di\u0107, F. Mari\u0107, M. Malikovi\u0107 #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/bartoszmilewski.com\/2018\/01\/23\/pointwise-kan-extensions\">Pointwise Kan extensions<\/a>. ~ Bartosz Milewski (@BartoszMilewski) #CategoryTheory #Haskell<\/li>\n<li><a href=\"http:\/\/inventwithpython.com\/cracking\">Cracking codes with Python: An introduction to building and breaking ciphers<\/a>. ~ Al Sweigart #eBook #Programming #Python<\/li>\n<li><a href=\"http:\/\/www.redprl.org\/\">RedPRL: a proof assistant for Computational Higher-Dimensional Type Theory<\/a>. #ITP #RedPRL #SML<\/li>\n<li><a href=\"http:\/\/www.cs.cmu.edu\/~rwh\/talks\/POPL18-Tutorial.pdf\">Computational (higher) type theory<\/a>. ~ R. Harper and C. Angiuli #RedPRL #SML<\/li>\n<li><a href=\"https:\/\/www.contextfreeart.org\/gallery2\/\">Context Free\/cfdg<\/a>: a simple language for generating stunning images. With only a few lines you can describe abstract art, beautiful organic scenery, and many kinds of fractals.<\/li>\n<li><a href=\"https:\/\/github.com\/ucsd-progsys\/elsa\">Elsa: a lambda calculus evaluator<\/a>. ~ R. Jhala @RanjitJhala #Haskell #Logic #LambdaCalculus<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/terna-pitagorica-a-partir-de-un-lado\">Exercitium: &#8220;Terna pitag\u00f3rica a partir de un lado&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/www.nature.com\/articles\/d41586-018-00604-6\">China enters the battle for AI talent<\/a>. #AI<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1801.05950\">Toward scalable verification for safety-critical deep networks<\/a>. ~ L. Kuper et als. #NeuralNetworks #SMT<\/li>\n<li><a href=\"https:\/\/elpais.com\/elpais\/2018\/01\/24\/el_aleph\/1516812203_870138.amp.html\">El curioso caso de la secuencia de Goodstein<\/a>. ~ M.A. Morales (@gaussianos) | El Aleph #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/plus.maths.org\/content\/conversation-stephen-cook-0\">A conversation with Stephen Cook<\/a>. #CompSci<\/li>\n<li><a href=\"http:\/\/kaygun.tumblr.com\/post\/170044995839\/collatz-sequence-yet-again\">Collatz sequence (yet again)<\/a>. ~ Atabey Kaygun (@Atabey_Kaygun) #CommonLisp #Math<\/li>\n<li><a href=\"https:\/\/www.dataquest.io\/blog\/introduction-functional-programming-python\/\">Introduction to functional programming in Python<\/a>. ~ Spiro Sideris #FunctionalProgramming #Python<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1801.08441\">Finitary-based domain theory in Coq: An early report<\/a>. ~ M.A. AbdelGawad #ITP #Coq<\/li>\n<li><a href=\"https:\/\/coda.wickstrom.tech\/episodes\/2018-01-22-domain-modelling-with-haskell-generalizing-with-foldable-and-traversable.html\">Domain modelling with Haskell: Generalizing with Foldable and Traversable<\/a>. ~ Oskar Wickstr\u00f6m #Haskell<\/li>\n<li><a href=\"https:\/\/storm-country.com\/blog\/LambdaCase\">LambdaCase in the wild<\/a>. ~ Matt Noonan (@BanjoTragedy) #Haskell<\/li>\n<li><a href=\"http:\/\/blog.sumtypeofway.com\/recursion-schemes-part-41-2-better-living-through-base-functors\">Recursion schemes, Part 4\u00bd: Better living through base functors<\/a>. ~ Patrick Thomson (@importantshock) #Haskell<\/li>\n<li><a href=\"https:\/\/codurance.com\/2018\/01\/25\/lambda-calculus-in-clojure-part-2\/\">Lambda calculus in Clojure (Part 2)<\/a>. ~ Sergio Rodrigo Royo #LambdaCalculus #Clojure<\/li>\n<li><a href=\"http:\/\/www.openculture.com\/2017\/08\/free-you-can-now-read-classic-books-by-mit-press-on-archive-org.html\">Free: You can now read classic books by MIT Press on archive.org<\/a> #eBooks<\/li>\n<li><a href=\"https:\/\/www.forbes.com\/sites\/quora\/2018\/01\/24\/when-is-haskell-more-useful-than-r-or-python-in-data-science\/#6e0cdcc069e4\">When is Haskell more useful than R or Python in Data Science?<\/a> ~ Tikhon Jelvis (@tikhonjelvis) #Haskell #Rstats #Python #DataScience<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2015-09-08-programming-r-at-native-speed-in-haskell.html\">Programming R at native speed using Haskell<\/a>. ~ M. Boespflug, F. Dom\u00ednguez, A. Vershilov #Haskell #Rstats<\/li>\n<li><a href=\"https:\/\/github.com\/patrickdoc\/hash-graph\">A hashing-based graph implementation in Haskell<\/a>. ~ Patrick Dougherty #Haskell<\/li>\n<li><a href=\"http:\/\/www.usrsb.in\/selling-laziness.html\">Selling laziness<\/a>. ~ Alex Beal (@beala) #Programming<\/li>\n<li><a href=\"https:\/\/www.cs.kent.ac.uk\/people\/staff\/dat\/miranda\/whyfp90.pdf\">Why functional programming matters<\/a>. ~ John Hughes #FunctionalProgramming #Miranda<\/li>\n<li><a href=\"http:\/\/community.wolfram.com\/groups\/-\/m\/t\/943405\">A toy Wolfram Language interpreter in Haskell<\/a>. ~ Yonghao Jin #Haskell<\/li>\n<li><a href=\"http:\/\/www.usrsb.in\/org-mode.html\">Org-mode: An integrated language and editor<\/a>. ~ Alex Beal (@beala) #Emacs #Haskell<\/li>\n<li><a href=\"https:\/\/medium.com\/@willkurt\/why-sum-types-matter-in-haskell-ba2c1ab4e372\">Why sum types matter in Haskell<\/a>. ~ Will Kurt (@willkurt) #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/complemento-potencial\">Exercitium: &#8220;Complemento potencial&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/ft_gateway.cfm?id=3158104&amp;ftid=1936978&amp;dwn=1&amp;CFID=3130691&amp;CFTOKEN=c3031a6fe3e8c92e-6E2750E0-9DA8-6D3C-4BBD90D8137A463D\">Intrinsically-typed definitional interpreters for imperative languages<\/a>. ~ C. Bach Poulsen, A. Rouvoet, A. Tolmach, R. Krebbers #ITP #Agda<\/li>\n<li><a href=\"http:\/\/tomasp.net\/academic\/drafts\/monads\/paper.pdf\">Monads are not what they seem (Uncovering the hidden nature of programming concepts)<\/a>. ~ T. Petricek #Math #CompSci<\/li>\n<li><a href=\"http:\/\/www.cs.tufts.edu\/comp\/116\/archive\/fall2017\/xqi.pdf\">Securing complex software systems using formal verification and specification<\/a>. ~ X. Qi #FormalVerification<\/li>\n<li><a href=\"https:\/\/youtu.be\/z3pm1dFvhMQ\">Programaci\u00f3n funcional: la programaci\u00f3n del futuro<\/a>. ~ Moises V\u00e1zquez #ProgramacionFuncional #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/sumas-parciales-de-juzuk\">Exercitium: &#8220;Sumas parciales de Juzuk&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9448-y.pdf\">A verified ODE solver and the Lorenz attractor<\/a>. ~ F. Immler #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/youtu.be\/0u3lY2eUHpA\">Un vistazo al futuro: revisando demostraciones matem\u00e1ticas con la computadora<\/a>. ~ Mois\u00e9s V\u00e1zquez #DAO<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/sucesion-de-digitos-0-y-1-alternados\">Exercitium: &#8220;Sucesi\u00f3n de d\u00edgitos 0 y 1 alternados&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"http:\/\/www.mathnet.or.kr\/mathnet\/thesis_file\/JKMS-54-5-1521-1536.pdf\">Formalizing the meta-theory of first-order predicate logic<\/a>. ~ H. Herberlin, S.Y. Kim, G. Lee #ITP #Coq #Logic<\/li>\n<li><a href=\"http:\/\/www.logicmatters.net\/2018\/01\/29\/category-theory-a-gentle-introduction\">Category theory: a gentle introduction<\/a>. ~ Peter Smith (@PeterSmith) #CategoryTheory<\/li>\n<li><a href=\"https:\/\/pastel.archives-ouvertes.fr\/tel-01691185\/document\">Investigations in computer-aided mathematics: experimentation, computation, and certification<\/a>. ~ Thomas Sibut Pinote #PhDThesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/pps2018.soic.indiana.edu\/files\/2017\/12\/dselsam_pps_2018.pdf\">Formal methods for probabilistic programming<\/a>. ~ D. Selsam, P. Liang, D.L. Dill #ITP #Lean<\/li>\n<li><a href=\"https:\/\/github.com\/dselsam\/certigrad\">Certigrad: Bug-free machine learning on stochastic computation graphs<\/a>. ~ D. Selsam #ITP #Lean<\/li>\n<\/ul>\n<div id=\"postamble\"><\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante enero de 2018, en Twitter sobre programaci\u00f3n funcional y demostraci\u00f3n asistida por ordenador fundamentalmente. 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\/6077"}],"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=6077"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6077\/revisions"}],"predecessor-version":[{"id":6156,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6077\/revisions\/6156"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6077"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6077"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6077"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}