{"id":6732,"date":"2019-06-01T11:31:14","date_gmt":"2019-06-01T09:31:14","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6732"},"modified":"2019-09-01T11:32:12","modified_gmt":"2019-09-01T09:32:12","slug":"resumen-de-lecturas-compartidas-durante-mayo-de-2019","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-mayo-de-2019\/","title":{"rendered":"Resumen de lecturas compartidas durante mayo de 2019"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante mayo de 2019, en <a href=\"https:\/\/twitter.com\/Jose_A_Alonso\">Twitter<\/a> fundamentalmente sobre programaci\u00f3n funcional y demostraci\u00f3n asistida por ordenador.<\/p>\n<p>Las lecturas est\u00e1n ordenadas seg\u00fan su fecha de publicaci\u00f3n en <a href=\"https:\/\/twitter.com\/Jose_A_Alonso\">Twitter<\/a>.<\/p>\n<p>Al final de cada art\u00edculo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.<\/p>\n<p>Una recopilaci\u00f3n de todas las lecturas compartidas se encuentra en <a href=\"https:\/\/github.com\/jaalonso\/Lecturas_GLC\">GitHub<\/a>.<br \/>\n<!--more--><\/p>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/arxiv.org\/abs\/1904.10759.pdf\">Ordinal notations via simultaneous definitions<\/a>. ~ F.N. Forsberg, C. Xu. #ITP #Agda #Logic #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1904.10570.pdf\">A formalization of forcing and the unprovability of the continuum hypothesis<\/a>. ~ J.M. Han, F. van Doorn. #ITP #LeanProver #Logic #Math<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2019\/04\/30\/code-style-and-moral-absolutes\">Code style and moral absolutes<\/a>. ~ Brent Yorgey. #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.00325\">QKD (Quantum Key Distribution) algorithm in Isabelle: Bayesian calculation<\/a>. ~ Florian Kamm\u00fcller. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.00276\">Warshall&#8217;s algorithm (survey and applications)<\/a>. ~ Zolt\u00e1n K\u00e1sa. #Algorithms<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1711.10455\">Backprop as Functor: A compositional perspective on supervised learning<\/a>. ~ B. Fong, D.I. Spivak, R. Tuy\u00e9ras. #MachineLearning #CategoryTheory<\/li>\n<li><a href=\"https:\/\/opensourc.es\/blog\/mip-tsp\">MIP: Travelling Salesman<\/a>. ~ Ole Kr\u00f6ger. #Algorithms #JuliaLang<\/li>\n<li><a href=\"https:\/\/opensourc.es\/blog\/minlp-tspn\">MINLP: Travelling Salesman with Neighborhoods<\/a>. ~ Ole Kr\u00f6ger. #Algorithms #JuliaLang<\/li>\n<li><a href=\"http:\/\/marco-lopes.com\/articles\/Currying-and-Partial-Application\/\">Currying and partial application<\/a>. ~ M. Lopes. #Haskell #Scala<\/li>\n<li><a href=\"http:\/\/www3.risc.jku.at\/publications\/download\/risc_5919\/Paper.pdf\">Formalization of Dub\u00e9&#8217;s degree bounds for Gr\u00f6bner bases in Isabelle\/HOL<\/a>. ~ A. Maletzky. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/oleg.fi\/gists\/posts\/2019-04-28-tabular.html\">Formatting tabular data<\/a>. ~ Oleg Grenrus. #Haskell<\/li>\n<li><a href=\"https:\/\/aearnus.github.io\/2019\/04\/26\/good-symbolic-differentiation-requires-multidimensional-wobbliness\">Good symbolic differentiation requires multidimensional wobbliness<\/a>. #Haskell #Math<\/li>\n<li><a href=\"https:\/\/blog.poisson.chat\/posts\/2019-04-03-system-f-in-coq.html\">Formalization of Reynolds&#8217;s parametricity theorem in Coq<\/a>. ~ Li-yao Xia. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/www.cs.cmu.edu\/~fp\/talks\/plmw19-talk.pdf\">How to think about types: Insights from a personal journey<\/a>. ~ F. Pfenning. #Logic #Programming #CompSci<\/li>\n<li><a href=\"https:\/\/aearnus.github.io\/2019\/04\/26\/good-symbolic-differentiation-requires-multidimensional-wobbliness\">Good symbolic differentiation requires multidimensional wobbliness<\/a>. ~ @Aearnus. #Haskell #Math<\/li>\n<li><a href=\"https:\/\/medium.com\/barely-functional\/do-we-need-effects-to-get-abstraction-7d5dc0edfbef\">Do we need effects to get abstraction?<\/a> ~ Eric Torreborre. #Haskell<\/li>\n<li><a href=\"https:\/\/www.well-typed.com\/blog\/2018\/03\/oop-in-haskell\/\">Object oriented programming in Haskell<\/a>. ~ Edsko de Vries. #Haskell<\/li>\n<li><a href=\"https:\/\/medium.com\/@olxc\/catamorphisms-and-f-algebras-b4e91380d134\">Catamorphisms and F-Algebras<\/a>. ~ Alex Avramenko. #Haskell<\/li>\n<li><a href=\"https:\/\/chrispenner.ca\/posts\/hkd-options\">Higher kinded option parsing<\/a>. ~ Chris Penner. #Haskell<\/li>\n<li><a href=\"https:\/\/web.archive.org\/web\/20140222124650\/http:\/\/chris-taylor.github.io\/blog\/2013\/02\/10\/the-algebra-of-algebraic-data-types\/\">The algebra of algebraic data types, part 1<\/a>. ~ Chris Taylor #Haskell<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/lens-as-a-divisibility-relation-goofin-off-with-the-algebra-of-types\/\">Lens as a divisibility relation: Goofin\u2019 off with the algebra of types<\/a>. ~ Philip Zucker. #Haskell<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=216\">PageRank y el surfista aleatorio<\/a>. ~ F. Sancho. #Algoritmos #IA<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/5\/6\/making-arrays-mutable\">Making arrays mutable!<\/a> ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.01735\">Interaction with formal mathematical documents in Isabelle\/PIDE<\/a>. ~ M. Wenzel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2019\/05\/06\/m1f-imperial-undergraduates-and-lean\/\">M1F, Imperial undergraduates, and Lean<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/medium.com\/@elizarov\/functional-programing-is-on-the-rise-ebd5c705eaef\">Functional programming is on the rise<\/a>. ~ Roman Elizarov. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/programminglanguages.info\/influence-network\">An interactive network graph showing the connections of programming languages based on their influences relations<\/a>. ~ Ramiro G\u00f3mez. #Programming<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell_Vol7\/raw\/master\/Libro\/Examenes_de_PF_con_Haskell_Vol7.pdf\">Ex\u00e1menes de programaci\u00f3n funcional con Haskell. Vol. 7 (Curso 2015-16)<\/a>. #Haskell #Programaci\u00f3nFuncional<\/li>\n<li><a href=\"http:\/\/aitp-conference.org\/2019\/abstract\/paper%2014.pdf\">Can neural networks learn symbolic rewriting?<\/a> ~ B. Piotrowski, C Brown, J. Urban, C. Kaliszyk. #ATP #MachineLearning<\/li>\n<li><a href=\"http:\/\/aitp-conference.org\/2019\/abstract\/AITP_2019_paper_34.pdf\">Tactic learning for Coq<\/a>. ~ L. Blaauwbroek. #ITP #Coq #MachineLearnig<\/li>\n<li><a href=\"http:\/\/aitp-conference.org\/2019\/abstract\/paper%2026.pdf\">Making set theory great again: The Naproche-SAD project<\/a>. ~ S. Frerix, P. Koepke. #ITP #Math<\/li>\n<li><a href=\"http:\/\/aitp-conference.org\/2019\/abstract\/invited%20paper%201.pdf\">Experiments with connection method provers<\/a>. ~ W. Bibel, J. Otten. #ATP<\/li>\n<li><a href=\"https:\/\/mathformachines.com\/files\/okcfp.pdf\">An introduction to categories with Haskell and databases<\/a>. ~ R. Holbrook. #CategoryTheory #Haskell #Databases<\/li>\n<li><a href=\"https:\/\/blogs.oracle.com\/developers\/the-power-of-functional-programming\">The power of functional programming<\/a>. ~ Arvind Kumar GS. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell_Vol8\/raw\/master\/Libro\/Examenes_de_PF_con_Haskell_Vol8.pdf\">Ex\u00e1menes de programaci\u00f3n funcional con Haskell. Vol. 8 (Curso 2016-17)<\/a>. #Haskell #Programaci\u00f3nFuncional<\/li>\n<li><a href=\"https:\/\/lance.fortnow.com\/papers\/files\/thesis.pdf\">Complexity-theoretic aspects of interactive proof systems<\/a>. ~ Lance Jeremy Fortnow. #PhD_Thesis #ITP #ComputationalComplexity<\/li>\n<li><a href=\"http:\/\/aitp-conference.org\/2019\/abstract\/AITP_2019_paper_8.pdf\">Neural guidance for SAT solving<\/a>. ~ S. Jaszczur, M. \u0141uszczyk, H. Michalewski. #ATP #SAT #MachineLearning<\/li>\n<li><a href=\"https:\/\/files.sketis.net\/Isabelle_Workshop_2018\/Isabelle_2018_paper_6.pdf\">Using Isabelle\/UTP for the verification of sorting algorithms (A case study)<\/a>. ~ J.A. Bockenek, P. Lammich, Y. Nemouchi, B. Wolff. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/www.jonmsterling.com\/pdfs\/algebraic-type-theory-tutorial.pdf\">Algebraic type theory and the gluing construction<\/a>. ~ J. Sterling. #CompSci #TypeTheory<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/the-subtle-art-of-the-mathematical-conjecture-20190507\/\">The subtle art of the mathematical conjecture<\/a>. ~ R. Dijkgraaf. #Math<\/li>\n<li><a href=\"https:\/\/dev.to\/gonzooo\/api-constraints-a-la-carte-in-haskell-purescript-3aba\">API constraints a&#8217;la carte in Haskell &amp; PureScript<\/a>. ~ R. Andersson. #Haskell #PureScript<\/li>\n<li><a href=\"https:\/\/blog.ch3m4.org\/2019\/04\/16\/que-es-un-coconut\/\">\u00bfQu\u00e9 es un coconut?<\/a> ~ Chema Cort\u00e9s. #Coconut #FunctionalProgramming #Python<\/li>\n<li><a href=\"https:\/\/blog.ch3m4.org\/2019\/05\/02\/coconut-primeros-pasos\/\">Coconut &#8211; Primeros pasos<\/a>. ~ Chema Cort\u00e9s. #Coconut #FunctionalProgramming #Python<\/li>\n<li><a href=\"https:\/\/blog.ch3m4.org\/2019\/05\/07\/monadas-con-coco\/\">Monadas con coco<\/a>. ~ Chema Cort\u00e9s. #Coconut #FunctionalProgramming #Python<\/li>\n<li><a href=\"https:\/\/qfpl.io\/posts\/fp-cheat-sheet\">Functional Programming Cheat Sheet<\/a>. ~ Tony Morris. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2019-05-08-list-manipulation-tricks.html\">Some tricks for list manipulation<\/a>. ~ Donnacha Ois\u00edn Kidney. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/typeclasses.com\/python\/islice\">Transition to Haskell from Python: Iterator slicing<\/a>. ~ Chris Martin, Julie Moronuki. #Python #Haskell<\/li>\n<li><a href=\"https:\/\/typeclasses.com\/python\/iteration-to-infinity\">Transition to Haskell from Python: Iteration to infinity<\/a>. ~ Chris Martin, Julie Moronuki. #Python #Haskell<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2019-05-09-inline-js.html\">Inline-JS: Seamless JavaScript\/Haskell interop<\/a>. ~ Shao Cheng. #Haskell #JavaScript<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell_Vol9\/raw\/master\/Libro\/Examenes_de_PF_con_Haskell_Vol9.pdf\">Ex\u00e1menes de programaci\u00f3n funcional con Haskell. Vol. 9 (Curso 2017-18)<\/a>. #Haskell #Programaci\u00f3nFuncional<\/li>\n<li><a href=\"https:\/\/medium.com\/code-gin\/logic-programming-a94fa0997eec\">Understanding logic programming<\/a>. #LogicProgramming #Python<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.03334\">SMT-based constraint answer set solver EZSMT+<\/a>. ~ D. Shen, Y. Lierler. #ASP #CASP<\/li>\n<li><a href=\"https:\/\/kunigami.blog\/2019\/05\/09\/constructing-trees-from-a-distance-matrix\/\">Constructing trees from a distance matrix<\/a>. ~ Guilherme Kunigami. #Algorithms<\/li>\n<li><a href=\"https:\/\/medium.com\/syncedreview\/alan-turing-institute-releases-ml-framework-written-in-julia-ac649f7c1f04\">Alan Turing Institute releases ML framework written in Julia<\/a>. #MachineLearning #JuliaLang<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell_Vol10\/raw\/master\/Libro\/Examenes_de_PF_con_Haskell_Vol10.pdf\">Ex\u00e1menes de programaci\u00f3n funcional con Haskell. Vol. 10 (Curso 2018-19)<\/a>. #Haskell #Programaci\u00f3nFuncional<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=217\">Teor\u00eda de la probabilidad: Lo m\u00ednimo<\/a>. ~ F. Sancho. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/rjlipton.wordpress.com\/2019\/05\/10\/making-elections-safe\/\">Making elections safe (A new proof that MAJORITY is not in AC\u2070)<\/a>. ~ R.J. Lipton. #CompSci<\/li>\n<li><a href=\"https:\/\/blog.klipse.tech\/clojure\/2019\/05\/10\/java-is-confusing-clojure-is-simple.html\">Java is confusing, Clojure is simple<\/a>. ~ Yehonathan Sharvit. #Programming #Java #Clojure<\/li>\n<li><a href=\"https:\/\/medium.com\/duomly-blockchain-online-courses\/introduction-to-functional-programming-with-python-examples-83f33308856a\">Introduction to functional programming with Python examples<\/a>. ~ Radoslaw Fabisiak. #FunctionalProgramming #Python<\/li>\n<li><a href=\"https:\/\/mathigon.org\/timeline\/\">Timeline of mathematics<\/a>. #Math<\/li>\n<li><a href=\"https:\/\/mroman42.github.io\/ctlc\/ctlc.pdf\">Category theory and lambda calculus<\/a>. ~ Mario Rom\u00e1n Garc\u00eda. #LambdaCalculus #CategoryTheory #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/mroman42\/mikrokosmos\">Mikrokosmos: a educational \u03bb-calculus interpreter<\/a>. ~ Mario Rom\u00e1n Garc\u00eda. #LambdaCalculus #Haskell<\/li>\n<li><a href=\"http:\/\/save.seecs.nust.edu.pk\/pubs\/2019\/ICCCS_2019_1.pdf\">Formalization of asymptotic notations in HOL4<\/a>. ~ N. Iqbal et als. #ITP #HOL4<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.01473.pdf\">A denotational engineering of programming languages<\/a>. ~ Andrzej Jacek Blikle. #eBook #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2019-05-11-concatenative-free.html\">Concatenative programming; the free monoid of programming languages<\/a>. ~ Donnacha Ois\u00edn Kidney. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/casperbp.net\/posts\/2019-04-nondeterminism-using-a-free-monad\/index.html\">Interpreters with non-determinism using a free monad<\/a>. ~ Casper Bach Poulsen. #Agda #Haskell<\/li>\n<li><a href=\"http:\/\/www.cs.utexas.edu\/~moore\/publications\/milestones.pdf\">Milestones from the pure lisp theorem prover to ACL2<\/a>. ~ J Strother Moore. #ITP #ACL2<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/Christoph_Benzmueller\/publication\/332786587_IO_Logic_in_HOL\/links\/5cc9c196299bf120978f2f1b\/I-O-Logic-in-HOL.pdf\">I\/O logic in HOL<\/a>. ~ C- Benzm\u00fcller, A. Farjami, P. Meder, X. Parent. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/5\/13\/quicksort-with-haskell\">Quicksort with Haskell!<\/a> ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.well-typed.com\/blog\/2019\/05\/integrated-shrinking\/\">Integrated versus manual shrinking<\/a>. ~ Edsko de Vries. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cvlad.info\/functor-of\">Functor-Of<\/a>. ~ Vladimir Ciobanu. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.05500\">Unifying semantic foundations for automated verification tools in Isabelle\/UTP<\/a>. ~ S. Foster et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/LambdaAuth.html\">Formalization of generic authenticated data structures in Isabelle\/HOL<\/a>. ~ M. Brun, D. Traytel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2019\/05\/14\/lightweight-efficiently-sampleable-enumerations-in-haskell\/\">Lightweight, efficiently sampleable enumerations in Haskell<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2019-05-14-corecursive-implicit-queues.html\">Implicit corecursive queues<\/a>. ~ Donnacha Ois\u00edn Kidney. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.05970\">holpy: Interactive theorem proving in Python<\/a>. ~ Bohua Zhan. #ITP #Logic #Python<\/li>\n<li><a href=\"http:\/\/qfpl.io\/share\/talks\/ghc-language-extensions\/\">GHC language extensions<\/a>. ~ Andrew McMiddlin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/qfpl.io\/share\/talks\/laws\/slides.pdf\">Laws!<\/a> ~ George Wilson. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/qfpl.io\/share\/talks\/appetite-for-dysfunction\/\">Appetite for dysfunction<\/a>. ~ Andrew McMiddlin #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/qfpl.io\/share\/talks\/reflexive-art\/composeconf.html\">Reflexive art<\/a>. ~ Sean Chalmers. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/qfpl.io\/share\/talks\/comma-police\/sv.pdf\">Comma police: The design and implementation of a CSV library<\/a>. ~ George Wilson. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/qfpl.io\/share\/talks\/state-machine-testing\">State machine testing<\/a>. ~ Andrew McMiddlin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/qfpl.io\/share\/talks\/contravariant-functors\/contravariant.pdf\">Contravariant functors: The other side of the coin<\/a>. ~ George Wilson. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1406.4823\">Notions of computation as monoids<\/a>. ~ E. Rivas, M. Jaskelioff. #Haskell #CategoryTheory<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02127698\/document\">Graph theory in Coq: Minors, treewidth, and isomorphisms<\/a>. ~ C. Doczkal, D. Pous. #ITP #Coq #Math<\/li>\n<li><a href=\"http:\/\/qfpl.io\/share\/talks\/cargo-culting-lenses\/talk.html\">Cargo culting lenses for fun &amp; profit<\/a>. ~ Sean Chalmers. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/qfpl.io\/share\/talks\/your-first-haskell-app\/\">Your first Haskell app<\/a>. ~ Andrew McMiddlin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/qfpl.io\/share\/talks\/typeclass-the-ultimate-ad-hoc\/slides.pdf\">Type class: The ultimate ad-hoc<\/a>. ~ George Wilson. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/discourse.haskell.org\/t\/a-note-on-the-connections-between-the-foldable-methods\/685\">A note on the connections between the Foldable methods<\/a>. ~ Daniel Mlot. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/kaygun\/18-Fall-Math388E\">Data science for fundamental sciences<\/a>. Atabey Kaygun #DataScience<\/li>\n<li><a href=\"https:\/\/rjlipton.wordpress.com\/2019\/05\/18\/an-app-proof\/\">An app proof<\/a>. R.J. Lipton. #Math<\/li>\n<li><a href=\"http:\/\/citeseerx.ist.psu.edu\/viewdoc\/download?doi=10.1.1.121.1890&amp;rep=rep1&amp;type=pdf\">Techniques for embedding postfix languages in Haskell<\/a>. ~ Chris Okasaki. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.07244\">Isabelle technology for the Archive of Formal Proofs<\/a>. ~ Makarius Wenzel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/aperez4.blogspot.com\/2019\/05\/la-geometria-se-hizo-arte-las-claves.html\">La Geometr\u00eda se hizo Arte: las claves secretas de Escher<\/a>. ~ Antonio P\u00e9rez Sanz. #Matem\u00e1ticas #Escher<\/li>\n<li><a href=\"http:\/\/andreipopescu.uk\/pdf\/ITP2015.pdf\">A consistent foundation for Isabelle\/HOL<\/a>. ~ O. Kun\u010dar, A. Popescu. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.06192\">Mechanised assurance cases with integrated formal methods in Isabelle<\/a>. ~ Y. Nemouchi et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.07961\">Guiding theorem proving by recurrent neural networks<\/a>. ~ B. Piotrowski, J. Urban. #ATP #NeuralNetworks<\/li>\n<li><a href=\"https:\/\/soupi.github.io\/rfc\/pfgames\/\">Purely functional games (How I built a game in Haskell &#8211; pure functional style)<\/a>. ~ Gil Mizrahi. #Haskell #FunctionalProgramming #Game<\/li>\n<li><a href=\"http:\/\/philsci-archive.pitt.edu\/16024\/\">For cybersecurity, Computer Science must rely on strongly-typed actors<\/a>. ~ C. Hewitt. #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/5\/20\/running-from-enemies\">Running from enemies!<\/a> ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/themattchan.com\/blog\/2019-05-19-cps-and-embeddings.html\">A correspondence between deep\/shallow embeddings and CPS\/first order evaluators<\/a>. ~ Matthew Chan. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/themattchan.com\/blog\/2018-12-22-code-style.html\">Thoughts on code style<\/a>. ~ Matthew Chan. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.cs.ru.nl\/bachelors-theses\/2018\/Timo_Maarse___4416295___Parsing_with_derivatives_in_Haskell.pdf\">Parsing with derivatives in Haskell<\/a>. ~ Timo Maarse. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.azavea.com\/blog\/2019\/05\/20\/functional-api-development-haskell\">Lessons in functional API development from Haskell\u2019s servant and Http4s<\/a>. ~ James Santucci. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/ieeexplore.ieee.org\/iel7\/8465565\/8488986\/08489371.pdf\">Formalization and certification of software for smart cities<\/a>. ~ E.S. Grilo, B. Lopes. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-19823-7_39\">EduBAI: An educational platform for logic-based reasoning<\/a>. ~ D. Arampatzis et als. #Teaching #Logic #ASP<\/li>\n<li><a href=\"http:\/\/www.di.uminho.pt\/~jno\/ps\/pdbc_part.pdf\">Program design by calculation<\/a>. ~ J.N. Oliveira. #eBook #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/riptutorial.com\/ebook\/haskell\">Learning Haskell language eBook<\/a>. #eBook #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2019\/05\/22\/competitive-programming-in-haskell-scanner\/\">Competitive programming in Haskell: Scanner<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.jez.io\/profiling-in-haskell\/\">Profiling in Haskell for a 10x speedup<\/a>. ~ Jake Zimmerman. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.ploeh.dk\/2019\/05\/20\/maybe-catamorphism\">Maybe catamorphism<\/a>. ~ Mark Seemann. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/flypitch\/flypitch-itp-2019\/releases\/download\/1.0\/flypitch-itp-2019.pdf\">A formalization of forcing and the consistency of the failure of the continuum hypothesis<\/a>. ~ Jesse Michael Han and Floris van Doorn. #ITP #LeanProver #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/flypitch\/flypitch\">Flypitch: A formal proof of the independence of the continuum hypothesis<\/a>. ~ Jesse Michael Han and Floris van Doorn. #ITP #LeanProver #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.09381\">Learning to prove theorems via interacting with proof assistants<\/a>. ~ K. Yang, J. Deng. #ITP #Coq #MachineLearning<\/li>\n<li><a href=\"https:\/\/github.com\/princeton-vl\/CoqGym\">CoqGym: A learning environment for theorem proving with the Coq proof assistant<\/a>. ~ K. Yang, J. Deng. #ITP #Coq #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.09565\">ENIGMAWatch: ProofWatch meets ENIGMA<\/a>. ~ Z. Goertzel, J. Jakub\u016fv, J. Urban. #ATP #MachineLearnig<\/li>\n<li><a href=\"https:\/\/reasonablypolymorphic.com\/blog\/faking-fundeps\/\">Faking fundeps with typechecker plugins<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.johndcook.com\/blog\/applied-category-theory\/\">Applied category theory<\/a>. ~ John D. Cook. #CategoryTheory<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2019\/05\/21\/equality-part-1-definitional-equality\/\">Equality part 1: definitional equality<\/a>. ~ Kevin Buzzard. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2019\/05\/25\/equality-part-2-syntactic-equality\/\">Equality part 2: syntactic equality<\/a>. ~ Kevin Buzzard. #ITP #LeanProver<\/li>\n<li><a href=\"http:\/\/www.javiercasas.com\/articles\/codata-in-action\">Codata in action, or how to connect Functional Programming and Object Oriented Programming<\/a>. ~ J. Casas. #Haskell #FunctionalProgramming #CategoryTheory<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/dimensions-and-haskell-introduction\">Dimensions and Haskell: Introduction<\/a>. ~ D. Rogozin. #Haskell #FunctionalProgramming #MachineLearnig #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.10006\">Graph representations for Higher-Order Logic and theorem proving<\/a>. ~ A. Paliwal et als. #ITP #ATP #MachineLearning<\/li>\n<li><a href=\"https:\/\/github.com\/david-christiansen\/pie-hs\">Pie-hs: an implementation of Pie, the language from &#8220;The little typer&#8221;, in Haskell<\/a>. ~ D.T. Christiansen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/5\/27\/smarter-enemies-with-bfs\">Smarter enemies with BFS!<\/a> ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/people.inf.ethz.ch\/trayteld\/papers\/cade19-incompleteness\/incompleteness.pdfw\">A formally verified abstract account of G\u00f6del&#8217;s incompleteness theorems<\/a>. ~ A. Popescu, D. Traytel. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/people.inf.ethz.ch\/trayteld\/papers\/lambdaauth\/lambdaauth.pdfw\">Generic authenticated data structures, formally<\/a>. ~ M. Brun, D. Traytel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.10501\">Learning to reason in large theories without imitation<\/a>. ~ K. Bansal et als. #ATP #MachineLearning<\/li>\n<li><a href=\"http:\/\/pirlea.net\/papers\/toychain-thesis.pdfw\">Toychain: Formally verified blockchain consensus<\/a>. ~ G. P\u00eerlea. #ITP #Coq #Blockchain<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.10728\">Programming with applicative-like expressions<\/a>. ~ J. Malakhovski, S. Soloviev. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2019-05-28-linear-phases.html\">Deriving a linear-time applicative traversal of a rose tree<\/a>. ~ Donnacha Ois\u00edn Kidney. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/noschinl\/cypw\">CYP: Checker for &#8220;morally correct&#8221; induction proofs about Haskell programs<\/a>. #ITP #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cs.nott.ac.uk\/~psztxa\/publ\/fomus19.pdfw\">Na\u00efve type theory<\/a>. ~ T. Altenkirch. #Logic #Math #TypeTheory #HoTT<\/li>\n<li><a href=\"https:\/\/interstices.info\/la-theorie-de-la-complexite-algorithmique\">La th\u00e9orie de la complexit\u00e9 algorithmique pour calculer efficacement<\/a>. ~ G. Lagarde #Algorithmes<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.12149\">SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver<\/a>. ~ P.W. Wang et als. #ATP #SAT #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.13100\">Towards finding longer proofs<\/a>. ~ Z. Zombori et als. #ATP #MachineLearning<\/li>\n<li><a href=\"http:\/\/www.cs.nott.ac.uk\/~psxmah\/liquidate.pdf\">Liquidate your assets (Reasoning about resource usage in Liquid Haskell)<\/a>. ~ M.A.T. Handley, N. Vazou, G. Hutton. #Haskell #LiquidHaskell<\/li>\n<li><a href=\"https:\/\/williamyaoh.com\/posts\/2019-05-27-string-interpolation-and-overlapping-instances.html\">String interpolation and overlapping instances<\/a>. ~ William Yao. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/bit.ly\/2JOlNdc\">Sobre cribas y matem\u00e1ticas<\/a>. ~ Juan Arias de Reyna. #Matem\u00e1ticas<\/li>\n<\/ul>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante mayo de 2019, en Twitter fundamentalmente sobre programaci\u00f3n funcional y demostraci\u00f3n asistida por ordenador. Las lecturas est\u00e1n ordenadas seg\u00fan su fecha de publicaci\u00f3n en Twitter. Al final de cada art\u00edculo se encuentran etiquetas relativas a los sistemas que usa o a su contenido. Una recopilaci\u00f3n de&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[6],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6732"}],"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=6732"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6732\/revisions"}],"predecessor-version":[{"id":6733,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6732\/revisions\/6733"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6732"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6732"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6732"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}