{"id":6200,"date":"2018-09-01T13:00:17","date_gmt":"2018-09-01T11:00:17","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6200"},"modified":"2018-09-01T13:01:13","modified_gmt":"2018-09-01T11:01:13","slug":"resumen-de-lecturas-compartidas-durante-agosto-de-2018","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-agosto-de-2018\/","title":{"rendered":"Resumen de lecturas compartidas durante agosto de 2018"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante agosto 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>.<\/p>\n<p><!--more--><\/p>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0747717118300361\">Formalization of the arithmetization of Euclidean plane geometry and applications<\/a>. ~ P. Boutry, G. Braun, J. Narboux #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1807.11576\">Formal probabilistic analysis of dynamic fault trees in HOL4<\/a>. ~ Y. Elderhalli, W. Ahmad, O. Hasan, S. Tahar #ITP #HOL4<\/li>\n<li><a href=\"http:\/\/compcogscisydney.org\/learning-statistics-with-r\/\">Learning statistics with R (A tutorial for psychology students and other beginners)<\/a>. ~ Danielle Navarro #Statistics #Rstats<\/li>\n<li><a href=\"http:\/\/blog.jpolak.org\/?p=2000\">Art vs. science in mathematical discovery<\/a>. ~ J. Polak #Math<\/li>\n<li><a href=\"https:\/\/deliquus.com\/posts\/2018-07-30-imperative-programming-in-haskell.html\">Making Haskell as fast as C: Imperative programming in Haskell<\/a>. ~ Henri Verroken #Haskell<\/li>\n<li><a href=\"https:\/\/hackernoon.com\/learn-functional-python-in-10-minutes-to-2d1651dece6f\">Learn functional Python in 10 minutes<\/a>. ~ Brandon Skerritt #FunctionalProgramming #Python<\/li>\n<li><a href=\"https:\/\/github.com\/tbanel\/orgaggregate\">Aggregates tables in Org mode<\/a>. ~ Thierry Banel #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1807.11399\">Who needs category theory?<\/a> ~ A. Blass, Y. Gurevich #CategoryTheory<\/li>\n<li><a href=\"https:\/\/github.com\/tchajed\/coq-tricks\">Tricks in Coq: Some tips, tricks, and features in Coq that are hard to discover<\/a>. ~ Tej Chajed #ITP #Coq<\/li>\n<li><a href=\"http:\/\/ceur-ws.org\/Vol-2149\/paper2.pdf\">An Answer Set Programming environment for high-level specification and visualization of FCA<\/a>. ~ L. Bourneuf #ASP #FCA<\/li>\n<li><a href=\"https:\/\/medium.freecodecamp.org\/make-your-code-easier-to-read-with-functional-programming-94fb8cc69f9d\">Make your code easier to read with Functional Programming<\/a>. ~ Cristi Salcescu #FunctionalProgramming #JavaScript<\/li>\n<li><a href=\"https:\/\/hackernoon.com\/two-years-of-functional-programming-in-javascript-lessons-learned-1851667c726\">Two years of functional programming in JavaScript: lessons learned<\/a>. ~ Victor Nakoryakov #FunctionalProgramming #JavaScript<\/li>\n<li><a href=\"https:\/\/www.47deg.com\/blog\/science-behind-functional-programming\/\">The science behind functional programming<\/a>. ~ Rafa Paradela #FunctionalProgramming #CategoryTheory<\/li>\n<li><a href=\"https:\/\/itnext.io\/pros-and-cons-of-functional-programming-32cdf527e1c2\">Pros and cons of functional programming<\/a>. ~ Iren Korkishko #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/opensource.com\/article\/17\/6\/functional-javascript\">An introduction to functional programming in JavaScript<\/a>. ~ Matt Banz #FunctionalProgramming #JavaScript<\/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 ~ V<\/a>. Benzaken, \u00c9. Contejean #ITP #Coq<\/li>\n<li><a href=\"http:\/\/www.lrdc.pitt.edu\/Ashley\/Mexico%20Talks\/Ashley-Tutorial05.pdf\">An introduction to artificial intelligence and law<\/a>. ~ K. Ashley, T. Gordon. #AI<\/li>\n<li><a href=\"https:\/\/hackernoon.com\/top-10-roles-for-your-data-science-team-e7f05d90d961\">Top 10 roles in AI and data science<\/a>. ~ Cassie Kozyrkov #AI #DataScience<\/li>\n<li><a href=\"https:\/\/www.typesofnote.com\/dsss17-slack.html\">Summarized Slack from Deepspec Summer School 2017<\/a>. #DSSS17 #ITP #Coq<\/li>\n<li><a href=\"https:\/\/gilmi.me\/blog\/post\/2018\/07\/24\/pfgames\">Purely functional games<\/a>. ~ Gil Mizrahi #FunctionalProgramming #Haskell #Game<\/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 [Slides] #FunctionalProgramming #Haskell #Game<\/li>\n<li><a href=\"https:\/\/blog.nyarlathotep.one\/2018\/07\/ghc-one-compiler-to-rule-them-all\">GHC, one compiler to RULE them all<\/a>. ~ Alexandre Moine #Haskell<\/li>\n<li><a href=\"https:\/\/haskell-works.github.io\/posts\/2018-08-01-introduction-to-rank-select-bit-string.html\">Introduction to the rank-select bit-string<\/a>. ~ John Ky #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/dselsam.github.io\/quickspec\/\">QuickSpec and the quest for good lemmas<\/a>. ~ Daniel Selsam #Haskell<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3236763\">Parametric polymorphism and operational improvement<\/a>. ~ J. Hackett, G. Hutton. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3236765\">The simple essence of automatic differentiation<\/a>. ~ Conal Elliott #FunctionalProgramming #CategoryTheory #Haskell<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3236777\">Teaching how to program using automated assessment and functional glossy games (experience report)<\/a>. ~ J. Bacelar Almeida et als. #Teaching #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/DAOconCoq\/index.php\/Tema_3:_Datos_estructurados_en_Coq\">DAOconCoq T3: Datos estructurados en Coq<\/a>. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/DAOconCoq\/releases\/download\/v0.3\/DAOconCoq.pdf\">Demostraci\u00f3n Asistida por Ordenador (3 primeros cap\u00edtulos)<\/a>. #DAOconCoq #ITP #Coq<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3236767\">Compositional soundness proofs of abstract interpreters<\/a>. ~ S. Keidel, C. Bach Poulsen, S. Erdweg. #Haskell<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3236770\">Elaborating dependent (co)pattern matching<\/a>. ~ J. Cockx, A. Abel. #Agda<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3236771\">Capturing the future by replaying the past (functional pearl)<\/a>. ~ J. Koppel, G. Scherer, A. Solar-Lezama. #FunctionalProgramming #SML<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3236772\">MoSeL: a general, extensible modal framework for interactive proofs in separation logic<\/a>. ~ R. Krebbers et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3236779\">What you needa know about Yoneda: profunctor optics and the Yoneda lemma (functional pearl)<\/a>. ~ G. Boisseau, J. Gibbons. #FunctionalProgramming #Haskell #CategoryTheory<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3236781\">Relational algebra by way of adjunctions<\/a>. ~ J. Gibbons et als. #FunctionalProgramming #Haskell #CategoryTheory<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3236784\">Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report)<\/a>. ~ J. Breitner et als. #Haskell #Coq<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3236785\">A type and scope safe universe of syntaxes with binding: their semantics and proofs<\/a>. ~ G. Allais et als. #Agda<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/DAOconCoq\/index.php\/Tema_4:_Polimorfismo_y_funciones_de_orden_superior_en_Coq\">DAOconCoq T4: Polimorfismo y funciones de orden superior en Coq<\/a>. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/DAOconCoq\/releases\/download\/v0.4\/DAOconCoq.pdf\">Demostraci\u00f3n Asistida por Ordenador (4 primeros cap\u00edtulos)<\/a>. #DAOconCoq #ITP #Coq<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3236788\">Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of \u03bbProlog\/Makam<\/a>. ~ A. Stampoulis, A. Chlipala. #Metaprogramming #Prolog<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3236787\">Equivalences for free: univalent parametricity for effective transport<\/a>. ~ N. Tabareau, \u00c9. Tanter, M. Sozeau. #Coq #HoTT<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3236791\">Fault tolerant functional reactive programming (functional pearl)<\/a>. ~ I. Perez #FunctionalProgramming #Haskell #Idris<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3236795\">Partially-static data as free extension of algebras<\/a>. ~ J. Yallo et als. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0167642318300273\">Boolean constraints in SWI-Prolog: A comprehensive system description<\/a>. ~ Markus Triska #Prolog #CLP<\/li>\n<li><a href=\"http:\/\/iris-project.org\/tutorial-pdfs\/iris-lecture-notes.pdf\">Lecture notes on Iris: Higher-order concurrent separation logic<\/a>. ~ L. Birkedal, A. Bizjak #ITP #Coq #Logic<\/li>\n<li><a href=\"https:\/\/limperg.de\/ghc-extensions\/\">A guide to GHC&#8217;s extensions<\/a>. ~ Jannis Limperg #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell\/releases\/download\/v.9.7.1\/Examenes_de_PF_con_Haskell.pdf\">Libro de ex\u00e1menes de programaci\u00f3n funcional con Haskell (versi\u00f3n del 4 de agosto de 2018)<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/archive.org\/stream\/MathematicalOlympiadInChinaProblemsAndSolutions\/Mathematical_Olympiad_in_China-Problems_and_Solutions\">Mathematical olympiad in China (problems and solutions)<\/a>. #Math<\/li>\n<li><a href=\"http:\/\/www.math.wustl.edu\/~sk\/eolss.pdf\">The history and concept of mathematical proof<\/a>. ~ S. G. Krantz. #Math<\/li>\n<li><a href=\"https:\/\/en.wikipedia.org\/wiki\/Mathematical_proof\">Mathematical proof<\/a>. ~ Wikipedia #Math<\/li>\n<li><a href=\"https:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m\/ejercicios\/ejercicios-I1M-2017.pdf\">I1M2017: Libro de ejercicios resueltos de programaci\u00f3n funcional en Haskell del curso 2017-18 (versi\u00f3n del 5 de agosto de 2018)<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/mpg.is\/papers\/gissurarson2018suggesting-xp.pdf\">Suggesting valid hole fits for typed-holes (Experience report)<\/a>. ~ Matth\u00edas P\u00e1ll Gissurarson #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/noinia\/hgeometry\">hgeometry: A simple geometry library in Haskell<\/a>. ~ Frank Staals #Haskell #Math<\/li>\n<li><a href=\"http:\/\/mvaled.github.io\/blog\/html\/2018\/08\/01\/composing-iterator-returning-functions.html\">Composing iterator-returning functions<\/a>. ~ Manuel V\u00e1zquez Acosta #Python #Haskell<\/li>\n<li><a href=\"https:\/\/global.handelsblatt.com\/companies\/lidl-software-flop-germany-digital-failure-950223\">Lidl software disaster another example of Germany\u2019s digital failure<\/a>. ~ F. Kolf, C. Kerkmann #Sofware #Bug<\/li>\n<li><a href=\"https:\/\/openstax.org\/subjects\">OpenStax: openly licensed textbooks<\/a>. #eBooks<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1807.11792\">Computing integer sequences: Filtering vs generation (Functional pearl)<\/a>. ~ I. Salvo, A. Pacifico #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1807.11267\">Coherent explicit dictionary application for Haskell: Formalisation and coherence proof<\/a>. ~ T. Winant, D. Devriese #Haskell<\/li>\n<li><a href=\"https:\/\/www.cs.us.es\/~jalonso\/publicaciones\/2018-DAOconIsabelleHOL.pdf\">Demostraci\u00f3n asistida por ordenador con Isabelle\/HOL<\/a>. #DAO #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/sonatsuer.github.io\/evangelism\/2018\/07\/23\/invitation.html\">An invitation to functional programming (for mathematicians)<\/a>. ~ Sonat S\u00fcer #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/danghica.blogspot.com\/2018\/07\/haskell-aint-maths.html\">Haskell ain&#8217;t maths<\/a>. ~ Dan Ghica #Haskell #Maths<\/li>\n<li><a href=\"https:\/\/sonatsuer.github.io\/higher-algebra\/2018\/07\/30\/monoid-homomorphisms-1.html\">Monoid homomorphisms (Part 1 of 2)<\/a>. ~ Sonat S\u00fcer #CategoryTheory #Haskell<\/li>\n<li><a href=\"http:\/\/math.jhu.edu\/~eriehl\/arithmetic.pdf\">Categorifying cardinal arithmetic<\/a>. ~ Emily Riehl #Math #CategoryTheory<\/li>\n<li><a href=\"https:\/\/rjlipton.wordpress.com\/2018\/08\/06\/desperately-seeking-integers\/\">Desperately seeking integers (A few twists on Turing\u2019s proof of undecidability of predicate calculus)<\/a>. ~ R.J. Lipton, K.W. Regan #Logic #Math<\/li>\n<li><a href=\"http:\/\/semantic-domain.blogspot.com\/2018\/08\/category-theory-in-pl-research.html%20\">Category theory in PL research<\/a>. ~ N. Krishnaswami #CategoryTheory #CompSci<\/li>\n<li><a href=\"https:\/\/medium.com\/@jeremyjkun\/habits-of-highly-mathematical-people-b719df12d15e\">Habits of highly mathematical people<\/a>. ~ Jeremy Kun #Math<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/a-short-guide-to-hard-problems-20180716\/\">A short guide to hard problems<\/a>. ~ Kevin Hartnett #Math #CompSci<\/li>\n<li><a href=\"http:\/\/www.openculture.com\/?p=1034777\">Discover \u201cUnpaywall,\u201d a new (and legal) browser extension that lets you read millions of science articles normally locked up behind paywalls<\/a>.<\/li>\n<li><a href=\"http:\/\/blog.poisson.chat\/posts\/2018-08-06-one-type-family.html\">Haskell with only one type family<\/a>. ~ Xia Li-yao #Haskell<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2018\/8\/6\/keeping-it-clean-haskell-code-formatters\">Keeping it clean: Haskell code formatters<\/a>. ~ James Bowen #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1808.01270v2\">Topological models of arithmetic<\/a>. ~ A. Enayat, J.D. Hamkins, B. Wcis\u0142o #Logic #Math<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/cek\/submitted\/ckkp-jar17.pdf\">Semantics of Mizar as an Isabelle object logic<\/a>. ~ C. Kaliszyk, K. P\u0105k #ITP IsabelleHOL #Mizar #Logic<\/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.T. Corti\u00f1as, W. Swierstra #FunctionalProgramming #ITP #Agda<\/li>\n<li><a href=\"https:\/\/www.mimuw.edu.pl\/~lukaszcz\/cicm2018.pdf\">&#8220;Concrete semantics&#8221; with Coq and CoqHammer<\/a>. ~ \u0141. Czajka, B. Ekici, C. Kaliszyk #ITP #Coq #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/github.com\/lukaszcz\/COQ-IMP%20\">Coq version of (part of) the HOL-IMP theories accompanying the book &#8220;Concrete Semantics with Isabelle\/HOL&#8221;<\/a>. Formalized using CoqHammer. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/www.mdpi.com\/2224-2708\/7\/3\/34\/pdf\">Enif-Lang: A specialized language for programming network functions on commodity hardware<\/a>. ~ N. Bonelli, S. Giordano, G. Procissi #Haskell<\/li>\n<li><a href=\"https:\/\/haskell-works.github.io\/posts\/2018-08-08-data-parallel-rank-select-bit-string-construction.html\">Data-parallel rank-select bit-string construction<\/a>. ~ John Ky #Haskell<\/li>\n<li><a href=\"https:\/\/sonatsuer.github.io\/higher-algebra\/2018\/08\/09\/monoid-homomorphisms-2.html\">Monoid homomorphisms (Part 2 of 2)<\/a>. ~ Sonat S\u00fcer #CategoryTheory #Haskell<\/li>\n<li><a href=\"https:\/\/sras.me\/haskell\/miscellaneous-enlightenments.html\">Learning Haskell: Miscellaneous enlightenments<\/a>. ~ Sandeep C R #Haskell<\/li>\n<li><a href=\"https:\/\/markkarpov.com\/tutorial\/th.html\">Template Haskell tutorial<\/a>. ~ Mark Karpov #Haskell<\/li>\n<li><a href=\"https:\/\/www.onlineuniversities.com\/blog\/2009\/07\/100-best-websites-for-mathletes\/\">100 best websites for mathletes<\/a>. #Math<\/li>\n<li><a href=\"https:\/\/www.dropbox.com\/s\/i0qgfoye6artcp8\/untyped_lambda.pdf?dl=0\">Lambda calculus &#8211; step by step<\/a>. ~ Helmut Brandl #LambdaCalculus #Logic #Math<\/li>\n<li><a href=\"https:\/\/leanpub.com\/outsidefp\">An outsider&#8217;s guide to statically typed functional programming<\/a>. ~ Brian Marick #FunctionalProgramming #Elm #PureScript<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/DAOconCoq\/index.php\/Tema_5:_T%C3%A1cticas_b%C3%A1sicas_de_Coq\">DAOconCoq T5: T\u00e1cticas b\u00e1sicas de Coq<\/a>. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/DAOconCoq\/releases\/download\/v0.5\/DAOconCoq.pdf\">Demostraci\u00f3n Asistida por Ordenador con Coq (5 primeros cap\u00edtulos)<\/a>. #DAOconCoq #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.johndcook.com\/blog\/2018\/08\/11\/currying\/\">Currying in calculus, PDEs, programming, and categories<\/a>. ~ J.D. Cook #Math #FunctionalProgramming #Haskell #CategoryTheory<\/li>\n<li><a href=\"https:\/\/medium.com\/@krystal.maughan\/breaking-the-space-time-barrier-with-haskell-time-traveling-and-debugging-in-codeworld-a-google-e87894dd43d7\">Breaking the space-time barrier with Haskell: Time-traveling and debugging in CodeWorld<\/a>. ~ Krystal Maughan #Haskell #CodeWorld<\/li>\n<li><a href=\"https:\/\/www.fceia.unr.edu.ar\/~mauro\/pubs\/cm-conf.pdf\">Improving typeclass relations by being open<\/a>. ~ G. Mart\u00ednez, M. Jaskelioff, G. De Luca #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/lortabac\/versioning\">Type-safe data versioning in Haskell<\/a>. ~ Lorenzo Tabacchini #Haskell<\/li>\n<li><a href=\"https:\/\/www.fpcomplete.com\/hubfs\/Haskell-User-Survey-Results.pdf\">State of Haskell 2018<\/a>. ~ Aaron Contorer #Haskell<\/li>\n<li><a href=\"https:\/\/www.nature.com\/news\/paradox-at-the-heart-of-mathematics-makes-physics-problem-unanswerable-1.18983\">Paradox at the heart of mathematics makes physics problem unanswerable<\/a>. ~ Davide Castelvecch #Logic #Math #Physics<\/li>\n<li><a href=\"https:\/\/abhinavsarkar.net\/posts\/fast-sudoku-solver-in-haskell-3\/\">Fast Sudoku solver in Haskell #3: Picking the right data structures<\/a>. ~ Abhinav Sarkar #Haskell<\/li>\n<li><a href=\"http:\/\/matryoshka.gforge.inria.fr\/pubs\/deep_learning_article.pdf\">A formal proof of the expressiveness of deep learning<\/a>. ~ A. Bentkamp, J.C. Blanchette, D. Klakow. #ITP #IsabelleHOL #DeepLearning<\/li>\n<li><a href=\"http:\/\/cattheory.com\/extensibleTypeDirectedEditing.pdf\">Extensible type-directed editing<\/a>. ~ J. Korkut, D.T. Christiansen #FunctionalProgramming #Idris<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/approximating-compiling-categories-using-typelevel-haskell-take-2\/\">Approximating compiling to categories using type-level Haskell: Take 2<\/a>. ~ Philip Zucker #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/matryoshka.gforge.inria.fr\/pubs\/wagemaker_bsc_thesis.pdf\">A formally verified proof of the Mason-Stothers theorem in Lean<\/a>. ~ J. Wagemaker #ITP #Lean #Math<\/li>\n<li><a href=\"http:\/\/kataskeue.com\/gdp.pdf\">Ghosts of departed proofs (Functional pearl)<\/a>. ~ Matt Noonan #Haskell<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~patrikj\/papers\/TypeTheory4ModProg_preprint_2018-05-19.pdf\">Type theory as a framework for modelling and programming<\/a>. ~ C. Ionescu, P. Jansson, N. Botta. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/proof-theory\/\">Proof theory<\/a>. ~ Michael Rathjen #Logic<\/li>\n<li><a href=\"https:\/\/divisbyzero.com\/2010\/08\/18\/mathematical-surprises\/\">Mathematical surprises<\/a>. ~ Dave Richeson #Math<\/li>\n<li><a href=\"https:\/\/link.springer.com\/article\/10.1007\/s10817-018-9455-7\">A verified SAT solver framework with learn, forget, restart, and incrementality<\/a>. ~ J.C. Blanchette et als. #ITP #IsabelleHOL #SAT<\/li>\n<li><a href=\"https:\/\/towardsdatascience.com\/newbies-guide-to-deep-learning-6bf601c5a98e\">Newbie\u2019s guide to Deep Learning (Taking baby steps when starting DL)<\/a>. ~ Arkar Min Aung #DeepLearning<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Minsky_Machines.html?utm_source=dlvr.it&amp;utm_medium=twitter\">Minsky machines in Isabelle\/HOL<\/a>. ~ Bertram Felgenhauer #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1807.08416v1\">Some fundamental theorems in Mathematics<\/a>. ~ Oliver Knill #Math<\/li>\n<li><a href=\"https:\/\/medium.com\/brandons-computer-science-notes\/divide-and-conquer-algorithms-4e83d9999ffa\">Divide and conquer algorithms<\/a>. ~ Brandon Skerritt #Algorithms<\/li>\n<li><a href=\"https:\/\/mzabani.github.io\/posts\/2018-08-13.html\">Typeclass induction and developing a QuickCheck-like library<\/a>. ~ Marcelo Zabani #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/patternsinfp.wordpress.com\/2018\/08\/14\/folds-on-lists\/\">Folds on lists<\/a>. ~ Jeremy Gibbons #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/sharkdp\/cube-composer\">Cube composer: A puzzle game inspired by functional programming<\/a>. ~ David Peter #FunctionalProgramming #PureScript #Game<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1808.04251v1\">Proof simplification and automated theorem proving<\/a>. ~ Michael Kinyon #ATP #Prover9<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1808.03810\">The Boyer-Moore waterfall model revisited<\/a>. ~ P. Papapanagiotou, J. Fleuriot #ITP #HOL_Light<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~algehed\/blogpostsHTML\/SAT.html\">A very small SAT solver<\/a>. ~ Maximilian Algehed #FunctionalProgramming #Haskell #Logic #SAT<\/li>\n<li><a href=\"http:\/\/argo.matf.bg.ac.rs\/publications\/2018\/2018-InformalToFormal.pdf\">From informal to formal proofs in euclidean geometry<\/a>. ~ S Stojanovic-\u00d0ur #ATP #TPTP #Math<\/li>\n<li><a href=\"https:\/\/medium.com\/@baseerhk\/pearls-of-scala-functional-programming-part-i-ab4b76ba0b43\">Pearls of Scala functional programming, Part I (1. Smallest free number: array-based solution)<\/a>. ~ Baseer Al-Obaidy #FunctionalProgramming #Scala<\/li>\n<li><a href=\"https:\/\/binx.io\/blog\/2018\/08\/09\/functional-programming-in-python\/\">Functional programming in Python (Creating transformation pipelines in Python)<\/a>. ~ Dennis Vriend #FunctionalProgramming #Python<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1808.03274\">Introducing computer science to high school students through logic programming<\/a>. ~ T.T. Yuen, M. Reyes, Y. Zhang. #LogicProgramming #ASP #Teaching<\/li>\n<li><a href=\"https:\/\/journals.agh.edu.pl\/csci\/article\/view\/2863\">Using Erlang in research and education in a technical university<\/a>. ~ I. Petrov, A. Alexeyenko, G. Ivanova. #FunctionalProgramming #Erlang #Teaching<\/li>\n<li><a href=\"https:\/\/julesh.com\/2018\/08\/16\/lenses-for-philosophers\/\">Lenses for philosophers<\/a>. ~ Jules Hedges #CategoryTheory<\/li>\n<li><a href=\"https:\/\/www.johndcook.com\/blog\/2018\/04\/14\/categorical-data-analysis\/\">Categorical data analysis<\/a>. ~ John D. Cook #CategoryTheory<\/li>\n<li><a href=\"https:\/\/shiftordie.de\/blog\/2018\/08\/17\/how-to-transform-camels-purescript-haskell\/\">How to turn a Dromedary camel into a Bactrian camel<\/a>. ~ Alexander Klink #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/mchav\/CourseraMachineLearning\">Exercises and notes from the Coursera Machine Learning Course by Andrew Ng<\/a>. ~ Michael Chavinda #FunctionalProgramming #Haskell #MachineLearning<\/li>\n<li><a href=\"https:\/\/opensource.googleblog.com\/2018\/08\/zurihac-2018-haskell-hackathon-in.html\">ZuriHac 2018: Haskell hackathon in Rapperswil<\/a>. ~ Ivan Kri\u0161to. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/medium.com\/@maiavictor\/solving-the-mystery-behind-abstract-algorithms-magical-optimizations-144225164b07\">Solving the mystery behind Abstract Algorithm\u2019s magical optimizations<\/a>. ~ Victor Maia #Haskell<\/li>\n<li><a href=\"https:\/\/julesh.com\/2016\/09\/22\/abusing-the-continuation-monad\/\">Abusing the continuation monad<\/a>. ~ Jules Hedges #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/www.cis.upenn.edu\/~rrand\/popl_2016\/\">Programs and proofs in the Coq proof assistant<\/a>. ~ Arthur Azevedo de Amorim and Robert Rand. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/terrytao.wordpress.com\/2018\/08\/18\/qed-version-2-0-an-interactive-text-in-first-order-logic\">QED version 2.0: an interactive text in first-order logic<\/a>. ~ Terence Tao #Teaching #Logic<\/li>\n<li><a href=\"https:\/\/medium.com\/building-nubank\/demystifying-functional-programming-in-a-real-company-e954a2591504\">Demystifying functional programming (in a real company)<\/a>. ~ Caio Oliveira #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/@sderosiaux\/why-referential-transparency-matters-7c179424dab5\">Why referential transparency matters?<\/a> ~ St\u00e9phane Derosiaux #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1808.04289&amp;hl\">Eliminating unstable tests in floating-point programs<\/a>. ~ L. Titolo, C.A. Mu\u00f1oz, M.A. Feli\u00fa, and M.M. Moscato. #FormalVerification #PVS<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/DAOconCoq\/index.php\/Tema_6:_L%C3%B3gica_en_Coq\">DAOconCoq T6: L\u00f3gica en Coq<\/a>. #DAO #Coq #L\u00f3gica<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/DAOconCoq\/releases\/download\/v0.6\/DAOconCoq.pdf\">Demostraci\u00f3n Asistida por Ordenador con Coq (6 primeros cap\u00edtulos)<\/a>. #DAOconCoq #DAO #Coq #Programaci\u00f3nFuncional #L\u00f3gica<\/li>\n<li><a href=\"https:\/\/github.com\/LeventErkok\/sbvPlugin\">SBVPlugin: Formally prove properties of Haskell programs using SBV\/SMT<\/a>. ~ Levent Erk\u00f6k #Haskell<\/li>\n<li><a href=\"http:\/\/www.scs.stanford.edu\/11au-cs240h\/notes\/ghc-slides.htm\">A Haskell compiler<\/a>. ~ David Tereil #Haskell<\/li>\n<li><a href=\"https:\/\/bartoszmilewski.com\/2018\/08\/20\/recursion-schemes-for-higher-algebras\/\">Recursion schemes for higher algebras<\/a>. ~ Bartosz Milewski #FunctionalProgramming #Haskell #CategoryTheory<\/li>\n<li><a href=\"https:\/\/www.microsiervos.com\/archivo\/ia\/etica-asistentes-inteligentes-filosofia.html\">Sobre la \u00e9tica de los asistentes inteligentes<\/a>. ~ @Alvy #IA<\/li>\n<li><a href=\"https:\/\/philpapers.org\/archive\/DANTAE-2.pdf\">Towards an ethics of AI assistants: An initial framework<\/a>. ~ John Danaher #AI<\/li>\n<li><a href=\"https:\/\/francis.naukas.com\/2012\/11\/04\/excelencia-universitaria-y-elitismo\">Excelencia universitaria y elitismo<\/a>. ~ Francisco R. Villatoro (#Universidad<\/li>\n<li><a href=\"http:\/\/www.usma.edu\/eecs\/SiteAssets\/SitePages\/Faculty%20Publication%20Documents\/Okasaki\/icfp99square.pdf\">From fast exponentiation to square matrices: An adventure in types<\/a>. ~ Chris Okasaki #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/mathoverflow.net\/questions\/308797\/what-programming-language-should-a-professional-mathematician-know\">What programming language should a professional mathematician know?<\/a> #Math #Programming #CompSci<\/li>\n<li><a href=\"https:\/\/www.technologyreview.es\/s\/10458\/esta-red-neuronal-aplica-leyes-fisicas-aprendidas-de-forma-automatica\">Esta red neuronal aplica leyes f\u00edsicas aprendidas de forma autom\u00e1tica<\/a>. #IA #F\u00edsica<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1807.10300\">Discovering physical concepts with neural networks<\/a>. ~ R. Iten et als. #MachineLearning #Physics<\/li>\n<li><a href=\"https:\/\/functor.tokyo\/blog\/2018-08-21-machine-learning-for-haskellers\">How to get into Machine Learning for a Haskeller<\/a>. ~ Dennis Gosnell #Haskell #MachineLearning<\/li>\n<li><a href=\"https:\/\/functional.works-hub.com\/learn\/water-jug-rewrite-with-haskell-part-i-4347a?utm_source=reddit&amp;utm_campaign=Walkies&amp;utm_content=Hask\/Blog\">Water jug rewrite with Haskell (Part I)<\/a>. ~ Vignesh Sarma K #Haskell<\/li>\n<li><a href=\"http:\/\/ceur-ws.org\/Vol-2162\/paper-08.pdf\">A verified simple prover for first-order logic<\/a>. ~ J. Villadsen, A. Schlichtkrull, A.H. From. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1808.05342\">Formalisation of a frame stack semantics for a Java-like language<\/a>. ~ A Schubert, J. Chrz\u0105szcz. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/haskell.cs.yale.edu\/wp-content\/uploads\/2011\/01\/cs.pdf\">The conception, evolution, and application of functional programming languages<\/a>. ~ Paul Hudak #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/goto.ucsd.edu\/~nvazou\/real_world_liquid.pdf\">LiquidHaskell: Experience with refinement types in the real world<\/a>. ~ N. Vazou, E.L. Seidel, R. Jhala #Haskell #LiquidHaskell<\/li>\n<li><a href=\"https:\/\/leanpub.com\/fpmortals\/read\">Functional programming for mortals with Scalaz<\/a>. ~ Sam Halliday #FunctionalProgramming #Scala #Scalaz<\/li>\n<li><a href=\"https:\/\/github.com\/fommil\/fpmortals\">Source and examples to \u201cFunctional Programming for Mortals with Scalaz\u201d<\/a>. ~ Sam Halliday #FunctionalProgramming #Scala #Scalaz<\/li>\n<li><a href=\"http:\/\/andreipopescu.uk\/pdf\/cosmed.pdf\">CoSMed: A confidentiality-verified social media platform<\/a>. ~ T. Bauerei\u00df et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/profsjt.blogspot.com\/2018\/08\/review-of-cosmed-confidentiality.html\">Review of: &#8220;CoSMed: a confidentiality-verified social media platform&#8221;<\/a>. ~ Simon Thompson #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/www.egri-nagy.hu\/pdf\/Math_Liberal_Arts_Reader.pdf\">Mathematics and programming &#8211; the easy languages to learn<\/a>. ~ A. Egri-Nagy #Math #CompSci<\/li>\n<li><a href=\"http:\/\/downloads.hindawi.com\/journals\/mpe\/aip\/4982974.pdf\">A new algebraic approach to decision making in a railway interlocking system based on preprocess<\/a>. A. Hernando, R. Maestre, E. Roanes-Lozano. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/arboldetintalibros.wordpress.com\/2011\/11\/02\/matematicos-y-acusmaticos\/\">Matem\u00e1ticos y acusm\u00e1ticos<\/a>. ~ Lucio Fernando Ru\u00edz #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/w.pitula.me\/2016\/monad-proof\/\">The proof: Monad as a monoid in category of endofunctors<\/a>. ~ Wojtek Pitu\u0142a #FunctionalProgramming #Scala<\/li>\n<li><a href=\"https:\/\/medium.com\/@maiavictor\/the-abstract-calculus-fe8c46bcf39c\">The abstract calculus<\/a>. ~ Victor Maia #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/dev.to\/allanmacgregor\/you-should-learn-functional-programming-in-2018-4nff\">You should learn functional programming in 2018<\/a>. ~ Allan MacGregor #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/phaazon.net\/media\/uploads\/axelsson2013using.pdf\">Using circular programs for higher-order syntax (Functional pearl)<\/a>. ~ E. Axelsson, K. Claessen. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/purelyfunctional.org\/slides\/writing_fast_haskell.pdf\">Writing fast Haskell (Elegance is not an excuse for bad performance)<\/a>. ~ Moritz Kiefer #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/qnikst.github.io\/posts\/2018-08-23-ht-no-more.html\">Marrying Haskell and Hyper-Threading<\/a>. ~ Alexander Vershilov #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/towardsdatascience.com\/what-is-tail-recursion-elimination-or-why-functional-programming-can-be-awesome-43091d76915e\">How functional programming can be awesome: Tail recursion elimination<\/a>. ~ Luciano Strika #FunctionalProgramming #Python #Haskell<\/li>\n<li><a href=\"https:\/\/haskell-works.github.io\/posts\/2018-08-22-pdep-and-pext-bit-manipulation-functions.html\">Bit-manipulation operations for high-performance succinct data-structures and CSV parsing<\/a>. ~ John Ky #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/medium.com\/@zaid.naom\/exploring-folds-a-powerful-pattern-of-functional-programming-3036974205c8\">Exploring folds: A powerful pattern of functional programming<\/a>. ~ Zaid Ajaj #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/speakerdeck.com\/konn\/the-great-power-of-newtypes\">The great power of Newtypes.<\/a> ~ Hiromi Ishii #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/www.cs.tufts.edu\/~kfisher\/teaching.html\">Some lectures on programming languages<\/a>. ~ Kathleen Fisher #Programming<\/li>\n<li><a href=\"https:\/\/www.slideshare.net\/StevePoling1\/turing-goes-to-church\">Turing goes to Church (What can a computer do?).<\/a> ~ Steve Poling #CompSci #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/ajknapp.github.io\/2018\/08\/14\/notomatic-differentiation.html\">Not-o-matic differentiation<\/a>. ~ Andrew Knapp #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~patrikj\/papers\/Janssonetal_DSLsofMathCourseExamplesResults_preprint_2018-08-17.pdf\">Examples and results from a BSc-level course on domain specific languages of mathematics ~ P.<\/a> Jansson et als. #Haskell #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1808.07771\">FMS: Functional programming as a modelling language<\/a>. ~ I. Dasseville, G. Janssens. #ASP<\/li>\n<li><a href=\"http:\/\/es.r4ds.hadley.nz\/\">R para Ciencia de Datos<\/a>. ~ G. Grolemund, H. Wickham #Rstats #DataScience<\/li>\n<li><a href=\"http:\/\/jmc.stanford.edu\/articles\/lisp\/lisp.pdf\">History of Lisp<\/a>. ~ John McCarthy #Lisp<\/li>\n<li><a href=\"https:\/\/github.com\/utkarshkukreti\/purescript-hedwi\">Hedwig: a fast, type safe, declarative PureScript library for building web applications<\/a>. ~ Utkarsh Kukretig#examples #PureScript<\/li>\n<li><a href=\"https:\/\/youtu.be\/NcUNN_tSmyE\">Purely functional solutions to imperative problems (HaskellRank Ep.07)<\/a>. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/marcinszamotulski.me\/posts\/finite-state-machines.html\">Typed transitions, finite state machines and free categories<\/a>. ~ Marcin Szamotulski #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.cicm-conference.org\/2018\/infproc\/paper11.pdf\">Towards Mac Lane\u2019s comparison theorem for the (co)Kleisli construction in Coq<\/a>. ~ Burak Ekici. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.cicm-conference.org\/2018\/infproc\/paper2.pdf\">Logic as a path to enlightenment (Work in progress report)<\/a>. ~ Wolfgang Schreiner #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/www.cicm-conference.org\/2018\/infproc\/paper13.pdf\">Automatic proof-checking of ordinary mathematical texts<\/a>. ~ S. Frerix, P. Koepke. #ATP #ITP #Math<\/li>\n<li><a href=\"https:\/\/www.cicm-conference.org\/2018\/infproc\/paper14.pdf\">IsarMathLib: a formalized mathematics library for Isabelle\/ZF<\/a>. ~ S. Ko\u0142ody\u0144ski. #ITP #IsabelleZF #Math<\/li>\n<li><a href=\"http:\/\/adam.chlipala.net\/papers\/FiatCryptoSP19\">Simple high-level code for cryptographic arithmetic (with proofs, without compromises)<\/a>. ~ A. Erbsen, J. Philipoom, J. Gross, R. Sloan, A. Chlipala. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/homalg-project.github.io\/CAP_project\/\">CAP (Categories, Algorithms, and Programming) project<\/a>. ~ S. Gutsche, S. Posur, M. Barakat, \u00d8. Skarts\u00e6terhagen. #CAS #CategoryTheory<\/li>\n<li><a href=\"https:\/\/www.cicm-conference.org\/2018\/infproc\/paper21.pdf\">On the syntax and semantics of CAP (Categories, Algorithms, Programming) project<\/a>. ~ S. Gutsche, S. Posur, \u00d8. Skarts\u00e6terhagen. #CAS #CategoryTheory<\/li>\n<li><a href=\"http:\/\/unsworks.unsw.edu.au\/fapi\/datastream\/unsworks:51703\/SOURCE2\">Automation for proof engineering (Machine-checked proofs at scale)<\/a>. ~ D. Matichuk. #ITP #IsabelleHOL #PhD_Thesis<\/li>\n<li><a href=\"https:\/\/www.cicm-conference.org\/2018\/infproc\/paper15.pdf\">Progress in the formalization of Matiyasevich&#8217;s theorem in the Mizar system<\/a>. ~ K. P\u0105k #ITP #Mizar #Math<\/li>\n<li><a href=\"http:\/\/philsci-archive.pitt.edu\/14966\/1\/univalence-4.pdf\">Univalent foundations as a foundation for mathematical practice<\/a>. ~ H. Crane. #Logic #Math<\/li>\n<li><a href=\"https:\/\/locallycompact.gitlab.io\/ANLGTH\/\">A nonlinear guide to Haskell<\/a>. ~ Daniel Firth #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/stevelosh.com\/blog\/2018\/08\/a-road-to-common-lisp\/\">A road to Common Lisp<\/a>. ~ Steve Losh #FunctionalProgramming #CommonLisp<\/li>\n<li><a href=\"http:\/\/stevelosh.com\/blog\/2018\/05\/fun-with-macros-gathering\/\">Fun with macros: Gathering<\/a>. ~ Steve Losh #FunctionalProgramming #CommonLisp<\/li>\n<li><a href=\"http:\/\/stevelosh.com\/blog\/2018\/07\/fun-with-macros-if-let\/\">Fun with macros: If-let and when-let<\/a>. ~ Steve Losh #FunctionalProgramming #CommonLisp<\/li>\n<li><a href=\"http:\/\/hal.inria.fr\/inria-00076024\/document\">The calculus of constructions<\/a>. ~ T. Coquand, G. Huet #Logic #Math<\/li>\n<li>[[<a href=\"https:\/\/github.com\/jaalonso\/DAOconCoq\/releases\/download\/v0.6.1\/DAOconCoq.pdf\">https:\/\/github.com\/jaalonso\/DAOconCoq\/releases\/download\/v0.6.1\/DAOconCoq.pdf<\/a>][Demostraci\u00f3n Asistida por Ordenador con Coq (6 primeros cap\u00edtulos,<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Simplex.html\">An incremental simplex algorithm with unsatisfiable core generation in Isabelle\/HOL<\/a>. ~ Filip Mari\u0107 #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/mfaerber\/documents\/thesis.pdf\">Learning proof search in proof assistants<\/a>. ~ Michael F\u00e4rber #AutomatedTheoremProving #MachineLearning<\/li>\n<li><a href=\"https:\/\/github.com\/passingcuriosity\/talks\/blob\/master\/homology\">A computational sketch of homology<\/a>. ~ Thomas Sutton #FunctionalProgramming #Haskell #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1808.07832\">A simple methodology for computing families of algorithms<\/a>. ~ D.N. Parikh et als. #Programming #CompSci<\/li>\n<li><a href=\"https:\/\/dspace.library.uu.nl\/handle\/1874\/367810\">Formalisation of cryptographic proofs in Agda<\/a>. ~ A.M. Golov. #ITP #Agda<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/cek\/coqhammer\">CoqHammer: Automation for dependent type theory<\/a>. ~ \u0141. Czajka, C. Kaliszyk. #ITP #ATP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/lukaszcz\/coqhammer\">CoqHammer: An automated reasoning hammer tool for Coq<\/a>. ~ \u0141ukasz Czajka #ITP #ATP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1711.10455\">Backprop as functor: A compositional perspective on supervised learning<\/a>. ~ B. Fong, D.I. Spivak, R. Tuy\u00e9ras. #Haskell #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1808.08652\">Unique solutions of contractions, CCS, and their HOL formalisation<\/a>. ~ C. Tian, D. Sangiorgi. #ITP #HOL4<\/li>\n<li><a href=\"https:\/\/dspace.library.uu.nl\/handle\/1874\/367801\">Verified tail-recursive folds through dissection<\/a>. ~ C. Tom\u00e9 Corti\u00f1as. #FunctionalProgramming #ITP #Agda<\/li>\n<li><a href=\"http:\/\/qfpl.io\/share\/talks\/laws\/slides.pdf\">Laws!<\/a> ~ George Wilson #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/mikecroucher.github.io\/MLPM_talk\/\">Is your research software correct?<\/a> ~ Mike Croucher #Programming<\/li>\n<li><a href=\"https:\/\/softwarefoundations.cis.upenn.edu\/qc-current\/index.html\">Software foundations Volume 4: QuickChick: Property-based testing in Coq<\/a>. ~ L. Lampropoulos, B.C. Pierce. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1707.09616v3\">Owl: A general-purpose numerical library in OCaml<\/a>. ~ L. Wang. #FunctionalProgramming #OCaml<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1808.09701\">Comparison of two theorem provers: Isabelle\/HOL and Coq<\/a>. ~ A. Yushkovskiy, S. Tripakis. #ITP #IsabelleHOL #Coq<\/li>\n<li><a href=\"https:\/\/qfpl.io\/share\/talks\/appetite-for-dysfunction\">Appetite for dysfunction<\/a>. ~ Andrew McMiddlin #FunctionalProgramming #Haskell #WordPress<\/li>\n<li><a href=\"https:\/\/github.com\/caisah\/emacs.dz\">Awesome emacs config files<\/a>. #Emacs<\/li>\n<li><a href=\"https:\/\/blog.computationalcomplexity.org\/2018\/08\/what-is-data-science.html\">What is Data Science?<\/a> ~ Lance Fortnow #DataScience<\/li>\n<li><a href=\"https:\/\/simons.berkeley.edu\/workshops\/schedule\/6680\">Foundations of Data Science Boot Camp<\/a>. #DataScience<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9440-6.pdf\">The role of the Mizar Mathematical Library for interactive proof development in Mizar<\/a>. ~ G. Bancerek et als. #ITP #Mizar #Math<\/li>\n<li><a href=\"http:\/\/www.cs.nmsu.edu\/~epontell\/ALP\/uploads\/alp_Amelia_Harrison.pdf\">Proving program correctness using the AG semantics: An example with n-queens<\/a>. ~ A. Harrison-18. #LogicProgramming #ASP<\/li>\n<li><a href=\"https:\/\/works.bepress.com\/yuliya_lierler\/80\/download\/\">SMT-based constraint answer set solver EZSMT+ for non-tight programs<\/a>. ~ D. Shen, Y. Lierler #LogicProgramming #ConstraintProgramming #ASP #SMT<\/li>\n<li><a href=\"https:\/\/www.techrepublic.com\/article\/is-julia-the-next-big-programming-language-mit-thinks-so-as-version-1-0-lands\/\">Is Julia the next big programming language? MIT thinks so, as version 1.0 lands<\/a>. #Programming #Julia<\/li>\n<li><a href=\"https:\/\/github.com\/mandubian\/neurocat\">From neural networks to the Category of composable supervised learning algorithms in Scala<\/a>. ~ P. Voitot #NeuralNetworks #CategoryTheory #Scala<\/li>\n<\/ul>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante agosto 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,177],"tags":[178,292],"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\/6200"}],"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=6200"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6200\/revisions"}],"predecessor-version":[{"id":6202,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6200\/revisions\/6202"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6200"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6200"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6200"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}