{"id":6101,"date":"2018-07-01T10:45:43","date_gmt":"2018-07-01T08:45:43","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6101"},"modified":"2018-07-10T10:00:23","modified_gmt":"2018-07-10T08:00:23","slug":"resumen-de-lecturas-compartidas-durante-junio-de-2018","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-junio-de-2018\/","title":{"rendered":"Resumen de lecturas compartidas durante junio de 2018"},"content":{"rendered":"<div id=\"content\">Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante junio 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\/caminos-reducidos\">Exercitium: &#8220;Caminos reducidos&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Optimal_BST.html\">Optimal binary search trees in Isabelle\/HOL<\/a>. ~ T. Nipkow and D. Somogyi #ITP #IsabelleHOL #Algorithms<\/li>\n<li><a href=\"http:\/\/www.diva-portal.org\/smash\/get\/diva2:1209426\/FULLTEXT01.pdf\">Functional programming and legacy software (Using PureScript to extend a legacy JavaScript system)<\/a>. ~ C. Fischer #PureScript<\/li>\n<li><a href=\"https:\/\/people.cs.kuleuven.be\/~tom.schrijvers\/Research\/papers\/lics2018.pdf\">Syntax and semantics for operations with scopes<\/a>. ~ M. Pir\u00f3g, T. Schrijvers, N. Wu, M. Jaskelioff #Haskell<\/li>\n<li><a href=\"https:\/\/mat-web.upc.edu\/people\/sebastia.xambo\/QC\/qc.pdf\">Mathematical essentials of quantum computing<\/a>. ~ J. Ru\u00e9, S. Xamb\u00f3 #Math #CompSci<\/li>\n<li><a href=\"https:\/\/dslsofmath.github.io\/BScProj2018\/index.html\">Learn You a Physics for Great Good!<\/a> ~ B. Werner, E. Sj\u00f6str\u00f6m, J. Johansson, O. Lundstr\u00f6m #eBook #Haskell #Physics<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1805.10090\">Certified ordered completion in Isabelle\/HOL<\/a>. ~ C. Sternagel, S. Winkler #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-01799712\/document\">Modular verification of programs with effects and effect handlers in Coq<\/a>. ~ T. Letan, Y. R\u00e9gis-Gianas, P. Chifflier, G. Hiet #ITP #Coq<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-01799629\/document\">A more precise, more correct stack and register model for CompCert<\/a>. ~ G. Barany #ITP #Coq<\/li>\n<li><a href=\"http:\/\/staff.mmcs.sfedu.ru\/~ulysses\/Papers\/2018-TFP-dgp-recursion.pdf\">Handling recursion in generic programming using closed type families<\/a>. ~ A. Bolotina, A. Pelenitsyn #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/books.goalkicker.com\/AlgorithmsBook\">Algorithms notes for professionals<\/a>. #eBook #Algorithms<\/li>\n<li><a href=\"https:\/\/github.com\/owickstrom\/gi-gtk-declarative\">Purely functional and declarative GTK+ programming in Haskell<\/a>. ~ Oskar Wickstr\u00f6m (@owickstrom) #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/DSLsofMath\/DSLsofMath\/raw\/master\/L\/snapshots\/DSLsofMathNotes_2018-02-28.pdf\">Domain specific languages of mathematics: lecture notes<\/a>. ~ Patrik Jansson (@patrikja), Cezar Ionescu. #Haskell #Math<\/li>\n<li><a href=\"http:\/\/www.well-typed.com\/blog\/2018\/05\/semi-formal-development\/\">Semi-formal development: The Cardano wallet<\/a>. ~ Edsko de Vries #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/numeros-de-church\">Exercitium: &#8220;N\u00fameros de Church&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"http:\/\/www.posteriorscience.net\/?p=206\">Programming by poking: why MIT stopped teaching SICP (The Structure and Interpretation of Computer Programs)<\/a>. ~ Yarden Katz #Programming<\/li>\n<li><a href=\"http:\/\/www.cs.cmu.edu\/~15150\">Course CMU 15-150: Functional programming, summer 2018<\/a>. #FunctionalProgramming #SML<\/li>\n<li><a href=\"http:\/\/reports-archive.adm.cs.cmu.edu\/anon\/2010\/CMU-CS-10-140.pdf\">Introductory Computer Science Education at Carnegie Mellon University: A Deans\u2019 Perspective<\/a>. ~ R.E. Bryant, K. Sutner, M.J. Stehlik #Teaching #CompSci<\/li>\n<li><a href=\"https:\/\/existentialtype.wordpress.com\/2011\/04\/17\/some-advice-on-teaching-fp\">Some thoughts on teaching functional programming<\/a>. ~ R. Harper #Teaching #FuncionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/cascala\/galileo\">Galileo is the genesis of a symbolic and numerical math tool written in Scala; a Computer Algebra System (CAS)<\/a>. #Scala #Math #CAS<\/li>\n<li><a href=\"https:\/\/whatthefunctional.wordpress.com\/2018\/06\/02\/making-an-ecosystem-simulation-in-haskell-part-3\">Making an ecosystem simulation in Haskell (Part 3)<\/a>. ~ Laurence Emms (@wtfunctional) #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1806.00069\">Explaining explanations: an approach to evaluating interpretability of machine learning<\/a>. ~ L.H. Gilpin et als. #XAI #AI #MachineLearning<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/numeros-taxicab\">Exercitium: &#8220;N\u00fameros taxicab&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/github.com\/coinmetrics-io\/haskell-tools\">Haskell-based CoinMetrics.io tools<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2018\/6\/4\/bxit5i954uafn0n4gah3yrzcxnc3q6\">Codeworld: Haskell as a first programming language<\/a>. ~ James Bowen (@james_OWA) #Haskell #Codeworld #Teaching<\/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 (@allanmacgregor) #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/books.goalkicker.com\/LinuxBook\/\">Linux notes for professionals<\/a>. #eBook #Linux<\/li>\n<li><a href=\"https:\/\/github.com\/pedritomelenas\/Software-Matematicas-GAP\">Bloque de GAP de la asignatura Software Matem\u00e1ticas<\/a>. ~ Pedro A. Garc\u00eda-S\u00e1nchez #CAS #SageMath<\/li>\n<li><a href=\"https:\/\/www.gap-system.org\/\">GAP (groups, algorithms, programming) a system for computational discrete algebra<\/a>. #CAS<\/li>\n<li><a href=\"https:\/\/github.com\/TheWizardTower\/monadTransformers\/raw\/master\/Slides.pdf\">Monad transformers for the easily confused<\/a>. ~ @TheWizardTower #Haskell<\/li>\n<li><a href=\"https:\/\/techspree.net\/github-alternatives\/\">GitHub alternative top 7 sites to host your open source project<\/a>. #GitHub<\/li>\n<li><a href=\"https:\/\/itsfoss.com\/github-alternatives\">Top GitHub alternatives to host your open source project<\/a>. ~ Abhishek Prakash #GitHub<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/la-regla-de-los-signos-de-descartes\">Exercitium: &#8220;La regla de los signos de Descartes&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1806.00608\">GamePad: a learning environment for theorem proving<\/a>. ~ D. Huang, P. Dhariwal, D. Song, I. Sutskever #ITP #Coq #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1806.00810\">A new style of mathematical proof<\/a>. ~ W.M. Farmer #Logic #Math<\/li>\n<li><a href=\"https:\/\/jfr.unibo.it\/article\/download\/8212\/7877\">A decision procedure for univariate polynomial systems based on root counting and interval subdivision<\/a>. ~ C. Munoz, A. Narkawicz, A. Dutle #ITP #PVS #Math<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/subexpresiones-aritmeticas\">Exercitium: &#8220;Subexpresiones aritm\u00e9ticas&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1806.02101\">Calculational verification of reactive programs with reactive relations and Kleene algebra<\/a>. ~ S. Foster, K. Ye, A. Cavalcanti, J. Woodcock #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/paytonturnage.com\/writing\/2018-06-05-generating-art-with-haskell\">Generating art with Haskell<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2018-06-03-breadth-first-traversals-in-too-much-detail.html\">Breadth-first traversals in far too much detail<\/a>. ~ Donnacha Ois\u00edn Kidney (@oisdk) #Haskell<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/ancestro-comun-mas-bajo\">Exercitium: &#8220;Ancestro com\u00fan m\u00e1s bajo&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"http:\/\/www.riptutorial.com\/haskell\">Haskell RIP tutorial<\/a>. ~ @RipTutorial #Haskell<\/li>\n<li><a href=\"https:\/\/www.kosmikus.org\/DerivingVia\/deriving-via-paper.pdf\">Deriving via (or, how to turn hand-written instances into an anti-pattern)<\/a>. ~ B. Bl\u00f6ndal, A. L\u00f6h, R. Scott #Haskell<\/li>\n<li><a href=\"https:\/\/www.technologyreview.com\/s\/611272\/this-algorithm-can-tell-which-number-sequences-a-human-will-find-interesting\">This algorithm can tell which number sequences a human will find interesting<\/a>. #AI #MachineLearning #Math<\/li>\n<li><a href=\"https:\/\/shemesh.larc.nasa.gov\/people\/cam\/publications\/WoLLIC2018-draft.pdf\">Formalization of the undecidability of the halting problem for a functional language<\/a>. ~ T. M. Ferreira Ramos et al. #ITP #PVS<\/li>\n<li><a href=\"https:\/\/sketis.net\/wp-content\/uploads\/2018\/05\/isabelle-jedit-fide2018.pdf\">Isabelle\/jEdit as IDE for domain-specific formal languages and informal text documents<\/a>. ~ M. Wenzel #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.sodavision.com\/essential-cheat-sheets-for-machine-learning-and-deep-learning-engineers\/\">Essential cheat sheets for machine learning and deep learning engineers<\/a>. ~ Vivian Chong #MachineLearning #DeepLearning<\/li>\n<li><a href=\"https:\/\/mpg.is\/papers\/gissurarson2018suggesting.pdf\">Suggesting valid hole fits for typed-holes<\/a>. ~ Matth\u00edas P\u00e1ll Gissurarson #Haskell<\/li>\n<li><a href=\"http:\/\/sitr.us\/2014\/05\/05\/category-theory-proofs-in-idris.html\">Category theory proofs in Idris<\/a>. ~ Jesse Hallett (@hallettj) #Idris #CategoryTheory<\/li>\n<li><a href=\"https:\/\/www.quora.com\/How-does-Idris-compare-to-other-dependently-typed-programming-languages\">How does Idris compare to other dependently-typed programming languages?<\/a> ~ Edwin Brady #Idris<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/valores-de-polinomios-y-de-expresiones\">Exercitium: &#8220;Valores de polinomios y de expresiones&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"http:\/\/bit.ly\/2JIFD9w\">Las matem\u00e1ticas del f\u00fatbol y el nuevo ministro de cultura<\/a>. ~ Juan Arias de Reyna #Matem\u00e1ticas #Computaci\u00f3n<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1806.03049\">Formalization of Lerch&#8217;s theorem using HOL Light<\/a>. ~ A. Rashid, O. Hasan #ITP #HOL_Light #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1806.03205\">Formal small-step verification of a call-by-value lambda calculus machine<\/a>. ~ F. Kunze, G. Smolka, Y. Forster #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/exercitium\/el-problema-de-las-n-torres\">Exercitium: &#8220;El problema de las N torres&#8221;<\/a>. #Haskell #I1M2017<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/lenses-products-prisms-sums.html\">Lenses embody Products, Prisms embody Sums<\/a>. ~ Justin Le (@mstk) #Haskell<\/li>\n<li><a href=\"https:\/\/gupea.ub.gu.se\/bitstream\/2077\/56128\/1\/gupea_2077_56128_1.pdf\">Formalizing constructive quantifier elimination in Agda<\/a>. ~ J. Pope #ITP #Agda #Logic<\/li>\n<li><a href=\"http:\/\/page.mi.fu-berlin.de\/cbenzmueller\/papers\/C71.pdf\">A dyadic deontic logic in HOL<\/a>. ~ C. Benzm\u00fcller, A. Farjami, X. Parent #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"http:\/\/group-mmm.org\/~ayamada\/DJTY18.pdf\">A formalization of the LLL basis reduction algorithm<\/a>. ~ J. Divas\u00f3n, S. Joosten, R. Thiemann, A. Yamada #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.technologyreview.com\/s\/611397\/machine-learning-predicts-world-cup-winner\">Machine learning predicts World Cup winner<\/a>. #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1806.03208\">Prediction of the FIFA World Cup 2018: A random forest approach with an emphasis on estimated team ability parameters<\/a>. ~ A. Groll et als. #MachineLearning<\/li>\n<li><a href=\"https:\/\/sigma.software\/about\/media\/lisp-back-future-tribute-60th-anniversary\">LISP: back to the future (a tribute to 60th anniversary)<\/a>. ~ Nikolay Mozgovoy #Programming #Lisp<\/li>\n<li><a href=\"http:\/\/www.cccblog.org\/2018\/06\/13\/the-surprising-security-benefits-of-end-to-end-formal-proofs\">The surprising security benefits of end-to-end formal proofs<\/a>. ~ Adam Chlipala<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1806.04774\">Goal-oriented conjecturing for Isabelle\/HOL<\/a>. ~ Y. Nagashima, J. Parsert #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.newton.ac.uk\/seminar\/20170713100011001\">Mining the Archive of Formal Proofs<\/a>. ~ J. Blanchette, M. Haslbeck, D. Matichuk, T. Nipkow #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/binaire.blog.lemonde.fr\/2018\/06\/12\/mettre-lethique-dans-lalgorithme\/\">Mettre l\u2019\u00e9thique dans l\u2019algorithme?<\/a> ~ Catherine Tessier, Vincent Bonnemains, Claire Saurel<\/li>\n<li><a href=\"http:\/\/revue.sesamath.net\/spip.php?article1110\">S\u00e9quences d\u2019algorithmique en math\u00e9matique en Python 3, de la seconde \u00e0 la terminale<\/a>. ~ Hubert Raymondaud #Python<\/li>\n<li><a href=\"http:\/\/irreal.org\/blog\/?p=7270\">A complete computing environment<\/a>. #Emacs<\/li>\n<li><a href=\"http:\/\/doc.rix.si\/cce\/cce.html\">Emacs as a complete computing environment<\/a>. ~ Ryan Rix #Emacs<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/paradox-skolem\/\">Skolem&#8217;s paradox<\/a>. ~ Timothy Bays #Logic<\/li>\n<li><a href=\"https:\/\/people.kth.se\/~kurlberg\/colloquium\/2005\/MartinLooef.pdf\">100 years of Zermelo\u2019s axiom of choice: what was the problem with it?<\/a> ~ Per Martin-L\u00f6f #Logic #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1806.03541\">Functional Pearl: Theorem Proving for all (Equational reasoning in Liquid Haskell)<\/a>. ~ N. Vazou, J. Breitner, W. Kunkel, D. van Horn, G. Hutton #Hakell #LiquidHaskell<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/~kirst\/hok\/thesis.pdf\">Foundations of Mathematics: a discussion of sets and types<\/a>. ~ Dominik Kirst #Logic #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1806.03205\">Formal small-step verification of a call-by-value lambda calculus machine<\/a>. ~ F. Kunze, G. Smolka, Y. Forster #ITP #Coq<\/li>\n<li><a href=\"https:\/\/files.sketis.net\/Isabelle_Workshop_2018\/Isabelle_2018_paper_3.pdf\">Substitutionless first-order logic: a formal soundness proof<\/a>. ~ A.H. From, J.B Larsen, A. Schlichtkrull, J. Villadsen #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-01811922\/document\">Ghosts for lists: from axiomatic to executable specifications<\/a>. ~ F. Loulergue, A. Blanchard, N. Kosmatov #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1806.03527\">Engaging millennials into learning formal methods<\/a>. ~ N. Cata\u00f1o #Teaching #FormalMethods<\/li>\n<li><a href=\"https:\/\/files.sketis.net\/Isabelle_Workshop_2018\/Isabelle_2018_paper_8.pdf\">PaMpeR: a proof method recommendation system for Isabelle\/HOL<\/a>. ~ Y. Nagashima, Y. He #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Projective_Geometry.html\">Projective geometry in Isabelle\/HOL<\/a>. ~ Anthony Bordg #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/markkarpov.com\/post\/smart-constructors-that-cannot-fail.html\">Smart constructors that cannot fail<\/a>. ~ Mark Karpov (@mrkkrp) #Haskell<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Localization_Ring.html\">The localization of a commutative ring in Isabelle\/HOL<\/a>. ~ Anthony Bordg #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/lists.cam.ac.uk\/pipermail\/cl-isabelle-users\/2018-June\/msg00072.html\">International Olympiad in Isabelle?<\/a> #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/128.84.21.199\/pdf\/1806.06114\">Formalizing category theory and presheaf models of type theory in Nuprl<\/a>. ~ Mark Bickford #ITP #Nuprl #CategoryTheory<\/li>\n<li><a href=\"http:\/\/mpickering.github.io\/posts\/2018-06-11-source-plugins.html\">Source Plugins: Four ways to build a typechecked Haskell expression<\/a>. ~ Matthew Pickering #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1803.07130.pdf\">A promise checked is a promise kept: inspection testing<\/a>. ~ Joachim Breitner (@nomeata) #Haskell<\/li>\n<li><a href=\"https:\/\/books.goalkicker.com\/PythonBook\">Python notes for professionals<\/a>. #Python<\/li>\n<li><a href=\"https:\/\/qz.com\/1307091\/the-inside-story-of-how-ai-got-good-enough-to-dominate-silicon-valley\">The inside story of how AI got good enough to dominate Silicon Valley<\/a>. #AI<\/li>\n<li><a href=\"https:\/\/www.cs.us.es\/~fsancho\/?e=204\">Di\u00e1logos entre Arquitectura, Ciudad y Computaci\u00f3n<\/a>. ~ F. Sancho (@sanchocaparrini) #NetLogo<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell\/blob\/master\/Curso_2017-18\/Grupo_1\/examen_6_12_jun.hs\">#I1M2017: Soluciones del 6\u00ba examen de programaci\u00f3n funcional con Haskell de los grupos 1, 2 y 3<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell\/blob\/master\/Curso_2017-18\/Grupo_4\/examen_6_12_jun.hs\">#I1M2017: Soluciones del 6\u00ba examen de programaci\u00f3n funcional con Haskell de los grupos 4 y 5<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell\/blob\/master\/Curso_2017-18\/Grupo_1\/examen_5_03_may.hs\">#I1M2017: Soluciones del 5\u00ba examen de programaci\u00f3n funcional con Haskell del grupo 1<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell\/blob\/master\/Curso_2017-18\/Grupo_2\/examen_5_30_abr.hs\">#I1M2017: Soluciones del 5\u00ba examen de programaci\u00f3n funcional con Haskell del grupo 2<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell\/blob\/master\/Curso_2017-18\/Grupo_3\/examen_5_26_abr.hs\">#I1M2017: Soluciones del 5\u00ba examen de programaci\u00f3n funcional con Haskell del grupo 3<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell\/blob\/master\/Curso_2017-18\/Grupo_5\/examen_5_07_may.hs\">#I1M2017: Soluciones del 5\u00ba examen de programaci\u00f3n funcional con Haskell del grupo 5<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/www.jaist.ac.jp\/is\/labs\/ishihara-lab\/mla2018\/doc\/slides\/Norbert_Preining.pdf\">Hyper natural deduction for G\u00f6del Logic: a natural deduction system for parallel reasoning<\/a>. ~ A. Beckmann, N. Preinin #Logic<\/li>\n<li><a href=\"https:\/\/www.johndcook.com\/blog\/r_language_for_programmers\/\">R language for programmers<\/a>. ~ John D. Cook #Rstats<\/li>\n<li><a href=\"http:\/\/github.com\/Web-Prolog\/swi-web-prolog\/raw\/master\/book\/web-prolog.pdf\">Web Prolog and the programmable Prolog Web (An attempt to revive and rebrand Prolog)<\/a>. ~ Torbj\u00f6rn Lager #Prolog<\/li>\n<li><a href=\"https:\/\/www.andrew.cmu.edu\/user\/avigad\/Papers\/formal_epistemology.pdf\">Proof theory<\/a>. ~ Jeremy Avigad #Logic<\/li>\n<li><a href=\"http:\/\/www.cs.nott.ac.uk\/~pszgmh\/autobench.pdf\">AutoBench: Comparing the time performance of Haskell programs<\/a>. ~ M.A.T. Handley, G. Hutton #Haskell<\/li>\n<li><a href=\"http:\/\/www.microsiervos.com\/archivo\/ia\/ibm-debater-inteligencia-artificial-debate-humano.html\">IBM Debater: la primera inteligencia artificial que gana un debate a un ser humano<\/a>. ~ @Alvy #IA<\/li>\n<li><a href=\"http:\/\/www.microsiervos.com\/archivo\/ia\/introduccion-aprendizaje-automatico-sesgos.html\">Una introducci\u00f3n visual al aprendizaje autom\u00e1tico y otra a los sesgos que pueden sufrir sus algoritmos<\/a>. ~ @Alvy #IA #AprendzajeAutom\u00e1tico<\/li>\n<li><a href=\"http:\/\/www.r2d3.us\/visual-intro-to-machine-learning-part-1\">A visual introduction to machine learning<\/a>. ~ Stephanie Yee (@stephaniejyee), Tony Chu (@tonyhschu) #AI #MachineLearning<\/li>\n<li><a href=\"http:\/\/www.r2d3.us\/visual-intro-to-machine-learning-part-2\">Model tuning and the bias-variance tradeoff<\/a>. ~ Stephanie Yee (@stephaniejyee), Tony Chu (@tonyhschu) #AI #MachineLearning<\/li>\n<li><a href=\"https:\/\/anthonybonato.com\/2018\/06\/20\/the-p-vs-np-problem-2\/\">The P vs NP problem<\/a>. ~ Anthony Bonato #CompSci<\/li>\n<li><a href=\"https:\/\/www.johndcook.com\/blog\/2013\/06\/06\/seven-dogmas-of-category-theory\/\">Seven dogmas of category theory<\/a>. ~ John D. Cook #CategoryTheory<\/li>\n<li><a href=\"https:\/\/medium.com\/@kurtcagle\/why-you-dont-need-data-scientists-a9654cc9f0e4\">Why you don\u2019t need data scientists<\/a>. ~ Kurt Cagle #DataScience<\/li>\n<li><a href=\"http:\/\/www.microsiervos.com\/archivo\/puzzles-y-rubik\/algoritmo-inteligente-cubo-rubik.html\">Un algoritmo que ha aprendido a resolver el Cubo de Rubik \u00absin asistencia humana\u00bb<\/a>. ~ @Alvy #IA #AprendizajeAutom\u00e1tico<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1805.07470\">Solving the Rubik&#8217;s cube without human knowledge<\/a>. ~ S. McAleer et als. #AI #MachineLearning<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/Ricardo_Pena5\/publication\/277290326_La_programacion_funcional_en_Haskell\/links\/5a9545bca6fdccecff07c72e\/La-programacion-funcional-en-Haskell.pdf\">La programaci\u00f3n funcional en Haskell<\/a>. ~ R. Pe\u00f1a #Programaci\u00f3nFuncional #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1806.07523\">Schematic polymorphism in the Abella proof assistant<\/a>. ~ G. Nadathur, Y. Wang #ITP #Abella<\/li>\n<li><a href=\"http:\/\/simonmar.github.io\/posts\/2018-06-20-Finding-fixing-space-leaks.html\">Fixing 17 space leaks in GHCi, and keeping them fixed<\/a>. ~ Simon Marlow (@simonmar) #Haskell<\/li>\n<li><a href=\"http:\/\/konn.github.io\/computational-algebra\">Computational algebra system in Haskell (Dependently-typed computational algebra system written in Haskell)<\/a>. ~ Hiromi Ishii #Haskell #CAS<\/li>\n<li><a href=\"https:\/\/cs.uwaterloo.ca\/~plragde\/flaneries\/FDS\/index.html\">Functional data structures<\/a>. ~ Prabhakar Ragde #FunctionalProgramming #Algorithms #OCaml<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell\/files\/2128201\/Examenes_de_PF_con_Haskell.pdf\">Libro de ex\u00e1menes de programaci\u00f3n funcional con Haskell (versi\u00f3n del 22 de junio de 2018)<\/a>. #Haskell #I1M2017<\/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<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/blog.goodaudience.com\/introduction-to-deep-learning-a46e92cb0022\">Introduction to deep learning (What is deep learning and how can I study it?)<\/a>. ~ Tyler Bettilyon (@TebbaVonMaths) #AI #DeepLearning<\/li>\n<li><a href=\"https:\/\/medium.com\/@TebbaVonMathenstien\/deep-neural-networks-as-computational-graphs-867fcaa56c9\">Deep neural networks as computational graphs (DNNs don\u2019t need to be a black box)<\/a>. ~ Tyler Bettilyon (@TebbaVonMaths) #AI #DeepLearning<\/li>\n<li><a href=\"https:\/\/diessi.ca\/blog\/computer-and-human-languages\">Computer and human languages<\/a>. ~ Di\u00e9ssica Gurskas (@diessicode) #Programming<\/li>\n<li><a href=\"https:\/\/people.eng.unimelb.edu.au\/tobym\/papers\/secdev2018.pdf\">BP: Formal proofs, the fine print and side effects<\/a>. ~ T- Murray, P.C. van Oorschot #FormalVerification<\/li>\n<li><a href=\"http:\/\/simonmar.github.io\/posts\/2018-06-22-New-SRTs.html\">Rethinking static reference tables in GHC<\/a>. ~ Simon Marlow (@simonmar) #Haskell<\/li>\n<li><a href=\"http:\/\/ozark.hendrix.edu\/~yorgey\/pub\/GCBP-author-version.pdf\">What\u2019s the difference? (A functional pearl on subtracting bijections)<\/a>. ~ B.A. Yorgey, K. Foner #Haskell<\/li>\n<li><a href=\"https:\/\/eng.uber.com\/queryparser\">Queryparser, an open source tool for parsing and analyzing SQL<\/a>. ~ Matt Halverson #Haskell<\/li>\n<li><a href=\"http:\/\/webdelprofesor.ula.ve\/ingenieria\/jacinto\/libros\/logica-practica-aprendizaje-computacional.pdf\">L\u00f3gica pr\u00e1ctica y aprendizaje computacional<\/a>. ~ Jacinto D\u00e1vila (@jacintodavila) #L\u00f3gica #IA #AprendizajeAutom\u00e1tico<\/li>\n<li><a href=\"http:\/\/www.doc.ic.ac.uk\/~rak\/papers\/newbook.pdf\">Computational logic and human thinking: How to be artificially intelligent<\/a>. ~ Robert Kowalski #eBook #IA #Logic<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Pell.html\">Pell&#8217;s equation in Isabelle\/HOL<\/a>. ~ Manuel Eberl #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/hal.univ-lille3.fr\/hal-01814822\/document\">Making the history of computing. The history of computing in the history of technology and the history of mathematics<\/a>. ~ L. de Mol, M. Bullynck #History #CompSci #Math<\/li>\n<li><a href=\"http:\/\/cs.yale.edu\/homes\/aspnes\/classes\/202\/notes.pdf\">Notes on discrete mathematics<\/a>. ~ James Aspnes #eBook #Math<\/li>\n<li><a href=\"https:\/\/abhinavsarkar.net\/posts\/fast-sudoku-solver-in-haskell-1\">Fast Sudoku solver in Haskell #1: a simple solution<\/a>. ~ Abhinav Sarkar (@abhin4v) #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/norvig\/paip-lisp\">Paradigms of Artificial Intelligence programming: case studies in Common Lisp<\/a>. ~ Peter Norvig #AI #CommonLisp<\/li>\n<li><a href=\"https:\/\/github.com\/hasktorch\/hasktorch\">Hasktorch: a library for tensors and neural networks in Haskell<\/a>. #Haskell #AI #MachineLearning<\/li>\n<li><a href=\"http:\/\/www.cs.rice.edu\/~vardi\/papers\/nsf16.pdf\">The automated-reasoning revolution: from theory to practice and back<\/a>. ~ Moshe Y. Vardi (@vardi) #ATP<\/li>\n<li><a href=\"http:\/\/cachestocaches.com\/2018\/6\/org-literate-programming\/\">Literate programming with Org-mode<\/a>. ~ Gregory J Stein (@CachesToCaches) #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/leanprover.github.io\/logic_and_proof\/logic_and_proof.pdf\">Logic and proof (Release 0<\/a>.1). ~ Jeremy Avigad, Robert Y. Lewis, and Floris van Doorn #Logic #LeanTheoremProver<\/li>\n<li><a href=\"http:\/\/reasonablypolymorphic.com\/blog\/roles\/\">Coercions and roles for dummies<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/benlynn.blogspot.com\/2018\/06\/why-laziness-matters.html\">Why laziness matters<\/a>. ~ Ben Lynn #Haskell<\/li>\n<li><a href=\"https:\/\/www.cs.us.es\/~jalonso\/apuntes\/inst-Lean.html\">Instalaci\u00f3n de &#8220;Lean theorem prover&#8221;<\/a>. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/github.com\/avigad\/formal_methods_in_education\/blob\/gh-pages\/index.md\">A web page with resources for teaching with formal methods and tools<\/a>. ~ Jeremy Avigad #ITP #Logic #Math<\/li>\n<li><a href=\"https:\/\/leanprover.github.io\/talks\/stanford2017.pdf\">Formal methods in mathematics and the Lean theorem prover<\/a>. ~ Jeremy Avigad #ITP #Logic #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1806.10920\">Machine learning for mathematical software<\/a>. ~ M. England #MachineLearning #MathematicalSoftware<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1611.04838v4\">Fast verifying proofs of propositional unsatisfiability via window shifting<\/a>. ~ Jingchao Chen #SAT<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell\/blob\/master\/Curso_2017-18\/Grupo_4\/examen_7_27_jun.hs\">#I1M2017: Soluciones del 7\u00ba examen de programaci\u00f3n funcional con Haskell<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell\/releases\/download\/v9.7\/Examenes_de_PF_con_Haskell.pdf\">Libro de ex\u00e1menes de programaci\u00f3n funcional con Haskell<\/a> (versi\u00f3n 9.7 del 30 de junio de 2018). #Haskell #I1M2017<\/li>\n<li><a href=\"http:\/\/irreal.org\/blog\/?p=7308\">The Emacs Commune<\/a>. #Emacs #History<\/li>\n<li><a href=\"http:\/\/forallx.openlogicproject.org\/\">forall x: Calgary Remix (An introduction to formal logic)<\/a>. ~ P.D. Magnus, T. Button, J. Robert Loftis, Aaron Thomas-Bolduc, R. Zach #eBook #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/sinahab\/shamir-secret-sharing\">The Shamir secret sharing algorithm in Haskell<\/a>. ~ Sina Habibian (@sinahab) #Haskell<\/li>\n<li><a href=\"http:\/\/very.science\/pdf\/StrictCheck_arxiv.pdf\">Keep your laziness in check<\/a>. ~ K. Foner et als. #Haskell<\/li>\n<\/ul>\n<div id=\"postamble\"><\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante junio 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\/6101"}],"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=6101"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6101\/revisions"}],"predecessor-version":[{"id":6146,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6101\/revisions\/6146"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6101"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6101"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6101"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}