{"id":6724,"date":"2019-03-01T11:18:31","date_gmt":"2019-03-01T10:18:31","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6724"},"modified":"2019-09-01T11:20:27","modified_gmt":"2019-09-01T09:20:27","slug":"resumen-de-lecturas-compartidas-durante-febrero-de-2019","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-febrero-de-2019\/","title":{"rendered":"Resumen de lecturas compartidas durante febrero de 2019"},"content":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante febrero 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=\"http:\/\/code.intef.es\/inteligencia-artificial-en-el-aula-con-scratch-3-0\">Inteligencia artificial en el aula con Scratch 3.0<\/a>. #Ense\u00f1anza #InteligenciaArtificial #Scratch<\/li>\n<li><a href=\"https:\/\/github.com\/cohomolo-gy\/haskell-resources\">A list of foundational Haskell papers<\/a>. ~ Emily Pillmore. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.arcadianvisions.com\/blog\/2018\/org-nix-direnv.html\">Robust notes with embedded code<\/a>. #Emacs #OrgMode<\/li>\n<li><a href=\"http:\/\/vmls-book.stanford.edu\/vmls.pdf\">Introduction to applied linear algebra<\/a>. ~ S. Boyd, L. Vandenberghe. #Math<\/li>\n<li><a href=\"http:\/\/vmls-book.stanford.edu\/vmls-julia-companion.pdf\">Introduction to applied linear algebra (Julia language companion)<\/a>. ~ S. Boyd, L. Vandenberghe. #Math #Programming #JuliaLang<\/li>\n<li><a href=\"http:\/\/xion.io\/post\/programming\/rust-into-haskell.html\">Rust as a gateway drug to Haskell<\/a>. ~ Karol Kuczmarski. #Programming #Rust #Haskell<\/li>\n<li><a href=\"https:\/\/twitter.com\/kena42\">Rust for functional programmers<\/a>. ~ Raphael \u2018kena\u2019 Poss. #Rust #Haskell #OCaml #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/tries-with-recursion-schemes.html\">Visualizing prequel meme prefix tries with recursion schemes<\/a>. ~ Justin Le. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/coot.me\/posts\/categories-with-monadic-effects.html\">Categories with monadic effects and state machines<\/a>. ~ Marcin Szamotulski. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/kbsg.rwth-aachen.de\/~hofmann\/papers\/clips-exec-pddl.pdf\">CLIPS-based execution for PDDL planners<\/a>. ~ T. Niemueller, T. Hofmann, G. Lakemeyer. #CLIPS<\/li>\n<li><a href=\"https:\/\/books.google.es\/books?id=-UOCDwAAQBAJ&amp;printsec=frontcover\">Data Science with Julia<\/a>. ~ P.D. McNicholas, P. Tait. #eBook #DataScience #JuliaLang<\/li>\n<li><a href=\"https:\/\/tonyarcieri.com\/rust-in-2019-security-maturity-stability\">Rust in 2019: security, maturity, stability<\/a>. ~ Tony Arcieri. #RustLang<\/li>\n<li><a href=\"https:\/\/www.maxwell.vrac.puc-rio.br\/35851\/35851.PDF\">Formaliza\u00e7\u00e3o de algoritmos de criptografia em um assistente de provas interativo<\/a>. ~ Guilherme Gomes Felix da Silva. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1807.01456\">A purely functional computer algebra system embedded in Haskell<\/a>. ~ H. Ishii #Haskell #FunctionalProgramming #CAS #Math<\/li>\n<li><a href=\"https:\/\/konn.github.io\/computational-algebra\">Computational algebra system in Haskell<\/a>. ~ H. Ishii #Haskell #FunctionalProgramming #CAS #Math<\/li>\n<li><a href=\"http:\/\/beautiful.ai\/deck\/-LVp7S8CDQAZdaT8hNhW\/Intro-to-Julia\">Introduction to Julia (the language of the future for AI and ML)<\/a>. ~ Zhuo Jia Dai. #JuliaLang<\/li>\n<li><a href=\"https:\/\/blog.acolyer.org\/2019\/01\/25\/programming-paradigms-for-dummies-what-every-programmer-should-know\/\">Programming paradigms for dummies: what every programmer should know<\/a>. ~ Adrian Colyer. #Programming<\/li>\n<li><a href=\"https:\/\/xuanji.appspot.com\/isicp\">Structure and interpretation of computer programs<\/a>. (Interactive version). ~ Hal Abelson, Gerald Jay Sussman. ~ #CompSci<\/li>\n<li><a href=\"https:\/\/www.cs.uaf.edu\/users\/chappell\/public_html\/class\/2018_spr\/cs331\/docs\/types_primer.html\">A primer on type systems<\/a>. ~ Glenn G. Chappell. #Programming #Haskell #Cpp #Python #Lua<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1901.10220\">On the impact of programming languages on code quality (A reproduction study)<\/a>. ~ E.D. Berger et als. #Programming<\/li>\n<li><a href=\"https:\/\/mountainscholar.org\/bitstream\/handle\/10217\/193082\/Kessler_colostate_0053N_14914.pdf\">Functional programming applied to computational algebra<\/a>. ~ I.H. Kessler. #Msc_Thesis #Math #CategoryTheory #FunctionalProgramming #Scala<\/li>\n<li><a href=\"https:\/\/www.cs.utexas.edu\/~vl\/teaching\/378\/ASP.pdf\">Answer Set Programming (Draft)<\/a>. ~ V. Lifschitz. #DeclarativeProgramming #ASP<\/li>\n<li><a href=\"https:\/\/www21.in.tum.de\/~eberlm\/real_asymp.pdf\">Verified real asymptotics in Isabelle\/HOL<\/a>. ~ M. Eberl. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/reduction.io\/essays\/rosetta-haskell.html\">A Rosetta stone for Haskell abstractions<\/a>. ~ Chas Leichner. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/andre.tips\/wmh\/\">Wise man&#8217;s Haskell<\/a>. ~ Andre Popovitch. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/sras.me\/haskell\/miscellaneous-enlightenments.html\">Learning Haskell (Miscellaneous enlightenments)<\/a>. ~ Sandeep C.R. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/books.google.es\/books?id=dMJiDwAAQBAJ&amp;printsec=frontcover\">2062: The World that AI made<\/a>. ~ Toby Walsh. #eBook #AI<\/li>\n<li><a href=\"https:\/\/blog.goodaudience.com\/10-reasons-why-you-should-learn-julia-d786ac29c6ca\">10 reasons why you should learn Julia<\/a>. ~ Gabriel Gauci Maistre. #Programming #JuliaLang<\/li>\n<li><a href=\"http:\/\/bogumilkaminski.pl\/files\/julia_express.pdf\">The Julia express<\/a>. ~ Bogumi\u0142 Kami\u0144ski. #Programming #JuliaLang<\/li>\n<li><a href=\"https:\/\/goo.gl\/scholar\/CHqqCY\">esverify: Verifying dynamically-typed higher-order functional programs by SMT solving<\/a>. ~ C. Schuster, S. Banerjea, C. Flanagan. #SMT #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/goo.gl\/scholar\/qymEhF\">Formal analysis of language-based Android security using theorem proving approach<\/a>. ~ W. Khan et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/2\/4\/why-haskell-v-type-families\">Why Haskell V: Type families<\/a>. ~ James Bowen. #Haskell<\/li>\n<li><a href=\"http:\/\/www.pl-enthusiast.net\/2019\/02\/04\/what-is-pl-research-the-talk\">&#8220;What is programming languages research?&#8221; The talk<\/a>. ~ Michael Hicks. #PL<\/li>\n<li><a href=\"http:\/\/richardzach.org\/2018\/04\/10\/the-significance-of-philosophy-to-mathematics\">The significance of Philosophy to Mathematics<\/a>. ~ Richard Zach. #Philosophy #Mathematics<\/li>\n<li><a href=\"https:\/\/books.google.es\/books?id=wPhwJdjI-dIC&amp;printsec=frontcover\">Proof and other dilemmas: Mathematics and Philosophy<\/a>. ~ B. Gold, R.A. Simons. #Mathematics #Philosophy<\/li>\n<li><a href=\"https:\/\/yurichev.com\/writings\/SAT_SMT_by_example.pdf\">SAT\/SMT by example<\/a>. ~ Dennis Yurichev. #SAT #SMT<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1208.1368\">Getting started with Isabelle\/jEdit in 2018<\/a>. ~ C. Sternagel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/justinbarclay.me\/posts\/literate_programming_against_rest_apis\">Literate programming against REST APIs<\/a>. ~ Justin Barclay. #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/www.williamjbowman.com\/resources\/wjb-dissertation.pdf\">Compiling with dependent types<\/a>. ~ W.J. Bowman. #PhD_Thesis<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/UTP.html\">Isabelle\/UTP: Mechanised theory engineering for unifying theories of programming<\/a>. ~ S. Foster et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/kowainik.github.io\/posts\/2019-02-06-style-guide\">Haskell style guide<\/a>. ~ Kowainik. #Haskell<\/li>\n<li><a href=\"https:\/\/keyholesoftware.com\/2019\/01\/30\/running-your-life-with-emacs\/\">Running your life with Emacs<\/a>. ~ Garrett Hopper #Emacs<\/li>\n<li><a href=\"https:\/\/hgiasac.github.io\/posts\/2019-01-04-Typeable---A-long-journey-to-Type-Safe-Dynamic-Type-Representations.html\">Typeable: A long journey to type-safe dynamic type representation<\/a>. ~ Toan Nguyen. #Haskell<\/li>\n<li><a href=\"https:\/\/cvlad.info\/curry-howard\/\">Curry-Howard correspondence example<\/a>. ~ Vladimir Ciobanu. #Haskell #Logic #Math #CategoryTheory<\/li>\n<li><a href=\"https:\/\/irreal.org\/blog\/?p=7824\">Calc tutorial<\/a>. #Emacs<\/li>\n<li><a href=\"https:\/\/nullprogram.com\/blog\/2009\/06\/23\/\">The Emacs calculator<\/a>. ~ Chris Wellons. #Emacs<\/li>\n<li><a href=\"https:\/\/www.gnu.org\/software\/emacs\/manual\/calc.html\">Calc: an advanced calculator and mathematical tool<\/a>. #Emacs #Math<\/li>\n<li><a href=\"https:\/\/github.com\/ahyatt\/emacs-calc-tutorials\">A series of tutorials about emacs-calc<\/a>. ~ Andrew Hyatt #Emacs #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1902.00297\">Signatures and induction principles for higher inductive-inductive types<\/a>. ~ A. Kaposi, A. Kov\u00e1cs. #ITP #Agda #Haskell<\/li>\n<li><a href=\"https:\/\/jcheminf.biomedcentral.com\/track\/pdf\/10.1186\/s13321-019-0332-0\">Chemoinformatics and structural bioinformatics in OCaml<\/a>. ~ F- Berenger, K.Y.J. Zhang, Y. Yamanishi. #OCaml #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.iro.umontreal.ca\/~monnier\/hopl-4-emacs-lisp.pdf\">Evolution of Emacs Lisp<\/a>. ~ S. Monnier, M. Sperber. #Emacs #Lisp<\/li>\n<li><a href=\"https:\/\/andreaspk.github.io\/posts\/2019-02-01-nub-benchmarks.html\">Comparing nub implementations<\/a>. ~ A. Klebinger. #Haskell<\/li>\n<li><a href=\"https:\/\/www.lavanguardia.com\/tecnologia\/20190209\/46283380483\/inteligencia-artificial-ia-kairos-darpa-pentagono.html\">EE.UU crea un algoritmo que predice golpes de estado y crisis financieras<\/a>. ~ A. Barbieri #AI<\/li>\n<li><a href=\"http:\/\/andrewcropper.com\/pubs\/jelia19-typed.pdf\">Typed meta-interpretive learning of logic programs<\/a>. ~ R: Morel, A. Cropper, L. Ong. #Prolog #ML<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell_Vol4\/releases\/download\/v1.0\/Examenes_de_PF_con_Haskell_Vol4.pdf\">Ex\u00e1menes de programaci\u00f3n funcional con Haskell. Vol. 4 (Curso 2012-13)<\/a>. #Haskell #Programaci\u00f3nFuncional<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2019\/02\/11\/lean-in-latex\">Lean in LaTeX<\/a>. ~ Kevin Buzzard. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/medium.com\/@reinman\/monads-for-dummies-3c3c0bbf95b6\">AI automation of software (Demystifying functional programming and monads)<\/a>. ~ @datacountry_ai. #FunctionalProgramming #CategoryTheory<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1902.03218\">Model checking applied to quantum physics<\/a>. ~ J. Guan, Y. Feng, A. Turrini, M. Ying. #ModelChecking<\/li>\n<li><a href=\"https:\/\/www.juliabloggers.com\/bisecting-floating-point-numbers-3\/\">Bisecting floating point numbers in Julia<\/a>. #JuliaLang #Math<\/li>\n<li><a href=\"https:\/\/medium.com\/permutive\/having-your-cake-and-eating-it-9f462bf3f908\">Having your cake and eating it<\/a>. ~ Tim Spence. #Haskell<\/li>\n<li><a href=\"http:\/\/gallium.inria.fr\/blog\/incremental-cycle-detection\">Formal proof and analysis of an incremental cycle detection algorithm<\/a>. ~ Arma\u00ebl Gu\u00e9neau. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/vaibhavsagar.com\/blog\/2019\/02\/12\/refactoring-haskell\/\">Refactoring Haskell: A case study<\/a>. ~ Vaibhav Sagar. #Haskell<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Universal_Turing_Machine.html\">Universal Turing Machine in Isabelle\/HOL<\/a>. ~ Jian Xu et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/codurance.com\/2019\/02\/11\/bank-kata-in-haskell-state\/\">Bank kata in Haskell &#8211; dealing with state<\/a>. ~ Liam Griffin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/reasonablypolymorphic.com\/blog\/freer-monads\/\">Freer monads, more better programs<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2019-02-13-types-got-you.html\">The types got you<\/a>. ~ Mark Karpov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/functional.works-hub.com\/learn\/afsm-arrowized-functional-state-machines-f0640\">AFSM: Arrowized Functional State Machines<\/a>. ~ Hanzhong Xu. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.marktarver.com\/bipolar.html\">The bipolar Lisp programmer<\/a>. ~ Mark Tarver. #Lisp #Programming<\/li>\n<li><a href=\"https:\/\/catonmat.net\/proof-that-sed-is-turing-complete\">A proof that Unix utility sed is Turing complete<\/a>. ~ Peter Krumins. #Programming<\/li>\n<li><a href=\"https:\/\/www.msoos.org\/2019\/02\/sat-solvers-as-smart-search-engines\/\">SAT solvers as smart search engines<\/a>. ~ Mate Soos. #SAT #Logic<\/li>\n<li><a href=\"http:\/\/www.msoos.org\/wordpress\/wp-content\/uploads\/2018\/09\/EMF-camp-SAT-and-SMT-solvers-final.pdf\">Hacking using SAT and SMT solvers<\/a>. ~ Mate Soos. #SAT #SMT #Logic<\/li>\n<li><a href=\"http:\/\/www.msoos.org\/wordpress\/wp-content\/uploads\/2010\/11\/soos_microsoft_pres.pdf\">Using SAT solvers for cryptographic problems<\/a>. ~ Mate Soos. #SAT #SMT #Logic<\/li>\n<li><a href=\"https:\/\/www.comp.nus.edu.sg\/~meel\/Papers\/aaai19-sm.pdf%20\">BIRD: Engineering an efficient CNF-XOR SAT Solver and its applications to approximate model counting<\/a>. ~ Mate Soos, Kuldeep S. Meel. #SAT<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2019\/02\/13\/finding-roots-of-polynomials-in-haskell\/\">Finding roots of polynomials in Haskell?<\/a> ~ Brent Yorgey. #Haskell<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Probabilistic_Prime_Tests.html\">Probabilistic primality testing in Isabelle\/HOL<\/a>. ~ D. St\u00fcwe, M. Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/lexi-lambda.github.io\/blog\/2018\/02\/10\/an-opinionated-guide-to-haskell-in-2018\/\">An opinionated guide to Haskell in 2018<\/a>. ~ Alexis King. #Haskell<\/li>\n<li><a href=\"http:\/\/mpickering.github.io\/posts\/2019-02-14-stage-3.html\">A three-stage program you definitely want to write<\/a>. ~ Matthew Pickering. #Haskell<\/li>\n<li><a href=\"https:\/\/www.vandenoever.info\/blog\/2015\/07\/12\/translating-haskell-to-c++.html\">Translating Haskell to C++ metaprogramming<\/a>. ~ Jos van den Oever. #Haskell #Cpp<\/li>\n<li><a href=\"https:\/\/dspace.library.uu.nl\/bitstream\/handle\/1874\/364837\/3705269.pdf\">Compiling an Haskell EDSL to C<\/a>. ~ F. Dedden. #Haskell #Clang<\/li>\n<li><a href=\"https:\/\/alex-hhh.github.io\/2019\/02\/racket-data-structures.html\">An overview of common Racket data structures<\/a>. ~ Alex Hars\u00e1nyi. #Racket<\/li>\n<li><a href=\"http:\/\/www.ii.uni.wroc.pl\/~nivelle\/publications\/jlc2014.pdf\">Theorem proving for classical logic with partial functions by reduction to Kleene logic<\/a>. ~ H. de Nivelle. #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1407.4399\">A constructive version of Tarski&#8217;s geometry<\/a>. ~ M. Beeson. #Logic #Math<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell_Vol5\/raw\/master\/Libro\/Examenes_de_PF_con_Haskell_Vol5.pdf%20\">Ex\u00e1menes de programaci\u00f3n funcional con Haskell. Vol. 5 (Curso 2013-14)<\/a>. #Haskell #Programaci\u00f3nFuncional<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2019\/02\/16\/worstsort\/\">Worstsort<\/a>. ~ Brent Yorgey. #Haskell<\/li>\n<li><a href=\"https:\/\/www.theguardian.com\/commentisfree\/2019\/feb\/17\/machines-not-our-masters-but-sinister-side-ai-demands-smart-response\">Machines are not our masters \u2013 but the sinister side of AI demands a smart response<\/a>. ~ Will Hutton. #AI<\/li>\n<li><a href=\"https:\/\/hackage.haskell.org\/package\/heyting-algebras-0.0.2.0\">Heyting and boolean algebras in Haskell<\/a>. ~ Marcin Szamotulski. #Haskell #Math<\/li>\n<li><a href=\"http:\/\/winterland.me\/2019\/02\/17\/stdio-A-simple-and-high-performance-IO%20toolkit-for-Haskell\/\">stdio: A simple and high-performance IO toolkit for Haskell<\/a>. #Haskell<\/li>\n<li><a href=\"http:\/\/dld.bz\/hrGRD\">Implementing the Davis\u2013Putnam method<\/a>. ~ H. Zhang, M.E. Stickel. #Logic #ATP<\/li>\n<li><a href=\"http:\/\/newartisans.com\/2017\/05\/monads-are-monoids\/\">Monads are monoid objects<\/a>. #Haskell #CategoryTheory<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/set-theory-constructive\/\">Set theory: constructive and intuitionistic ZF<\/a>. ~ Laura Crosilla. #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Kruskal.html\">Kruskal&#8217;s algorithm for minimum spanning forest in Isabelle\/HOL<\/a>. ~ M.P.L. Haslbeck et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.repository.cam.ac.uk\/bitstream\/handle\/1810\/289389\/thesis.pdf\">Towards justifying computer algebra algorithms in Isabelle\/HOL<\/a>. ~ W. Li. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/reasonablypolymorphic.com\/blog\/too-fast-too-free\/\">Freer monads: too fast, too free<\/a>. #Haskell<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/a-touch-of-topological-computation-3-categorical-interlude\/\">A touch of topological quantum computation 3: Categorical interlude<\/a>. ~ Philip Zucker. #Haskell #CategoryTheory<\/li>\n<li><a href=\"https:\/\/whatthefunctional.wordpress.com\/2019\/02\/20\/a-brief-introduction-to-the-%CE%BB-calculus-part-1\">A brief introduction to the \u03bb-calculus (part 1)<\/a>. ~ Laurence Emms. #LambdaCalculus<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/news\/234896-the-ai-that-can-write-fake-news-stories-from-handful-of-words\/fulltext\">The AI that can write fake news stories from handful of words<\/a>. #AI<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/List_Inversions.html\">The inversions of a list in Isabelle\/HOL<\/a>. ~ M. Eberl. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/cvlad.info\/quantifiers\/\">Quantifiers in Agda<\/a>. ~ Vladimir Ciobanu. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/whatthefunctional.wordpress.com\/\">A brief introduction to the \u03bb-calculus (part 2)<\/a>. ~ Laurence Emms. #LambdaCalculus<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Prime_Distribution_Elementary.html\">Elementary facts about the distribution of primes in Isabelle\/HOL<\/a>. ~ M. Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/haskell-works.github.io\/posts\/2019-02-22-adding-bit-vectors-branchless-comparisons.html\">Adding bit vectors &#8211; Branchless Comparisons<\/a>. ~ John Ky. #Haskell<\/li>\n<li><a href=\"https:\/\/habr.com\/en\/post\/441350\/\">Is Haskell really the language of geniuses and academia?<\/a> #Haskell<\/li>\n<li><a href=\"https:\/\/coot.me\/posts\/monadic-io.html\">Why monadic IO?<\/a> ~ Marcin Szamotulski. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell_Vol6\/raw\/master\/LibroE\/xamenes_de_PF_con_Haskell_Vol6.pdf\">Ex\u00e1menes de programaci\u00f3n funcional con Haskell<\/a>. (Vol. 6: Curso 2014-15). #Haskell #Programaci\u00f3nFuncional<\/li>\n<li><a href=\"https:\/\/jfr.unibo.it\/article\/download\/8751\/8968\">Commutativity theorems in groups with power-like maps<\/a>. ~ R. Padmanabhan, Y. Zhang. #ATP #Prover9 #Math<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/Students\/baek_ms_thesis.pdf\">Reflected decision procedures in lean<\/a>. ~ S. Baek. #PhD_Thesis #ITP #LeanProver #Logic #Math<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2019\/02\/24\/whats-the-right-way-to-quickcheck-floating-point-routines\/\">What\u2019s the right way to QuickCheck floating-point routines?<\/a> ~ Brent Yorgey. #Haskell<\/li>\n<li><a href=\"http:\/\/r6.ca\/blog\/20190223T161625Z.html\">How can basic arithmetic make a self-referential sentence?<\/a> ~ Russell O\u2019Connor. #Haskell #Logic #Math<\/li>\n<li><a href=\"https:\/\/victorcmiraldo.github.io\/data\/tyde2018_draft.pdf\">Sums of products for mutually recursive datatypes (The appropriationist\u2019s view on generic programming)<\/a>. ~ V.C. Miraldo, A. Serrano. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.michael-noll.com\/blog\/2013\/12\/02\/twitter-algebird-monoid-monad-for-large-scala-data-analytics\/\">Of Algebirds, monoids, monads, and other bestiary for large-scale data analytics<\/a>. ~ Michael G. Noll. #Scala #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2019-02-25-agda-fingertrees.html\">Finger trees in Agda<\/a>. ~ Donnacha Ois\u00edn Kidney. #Agda<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/10237\/pdf\/dagrep_v008_i008_p130_18341.pdf\">Formalization of mathematics in type theory (Report from Dagstuhl Seminar 18341)<\/a>. #ITP #Math<\/li>\n<li><a href=\"https:\/\/people.smp.uq.edu.au\/YoniNazarathy\/julia-stats\/StatisticsWithJulia.pdf\">Statistics with Julia: Fundamentals for Data Science, Machine Learning and Artificial Intelligence<\/a>. ~ H. Klok, Y. Nazarathy. #eBook #JuliaLang #DataScience #MachineLearnig #AI<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1902.08048\">A complete axiomatisation of reversible Kleene lattices<\/a>. ~ P. Brunet. #ITP #Coq #Logic #Math<\/li>\n<li><a href=\"https:\/\/giordano.github.io\/blog\/2017-11-03-rock-paper-scissors\">Rock\u2013paper\u2013scissors game in less than 10 lines of code<\/a>. ~ Mos\u00e8 Giordano. #Programming #JuliaLang<\/li>\n<li><a href=\"https:\/\/towardsdatascience.com\/all-your-matplotlib-questions-answered-420dd95cb4ff\">Matplotlib guide for people in a hurry<\/a>. ~ Julia Kho. #Python<\/li>\n<li><a href=\"https:\/\/www.fpcomplete.com\/blog\/quickcheck-hedgehog-validity\">QuickCheck, Hedgehog, Validity<\/a>. ~ Syd Kerckhove. #Haskell<\/li>\n<li><a href=\"http:\/\/entropiesschool.sciencesconf.org\/data\/How_to_Write_Mathematics.pdf\">How to write mathematics<\/a>. ~ Paul R. Halmos. #Math<\/li>\n<li><a href=\"http:\/\/www3.risc.jku.at\/publications\/download\/risc_5895\/main.pdf\">Theorem and algorithm checking for courses on logic and formal methods<\/a>. ~ W. Schreiner. #ITP #Logic #Teaching<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2019-02-28-jupyter-with.html\">JupyterWith: Declarative, reproducible notebook environments<\/a>. ~ J. Sim\u00f5es, M. Meschede. #Programming #Jupyter<\/li>\n<\/ul>\n<\/div>\n<div id=\"postamble\" class=\"status\">\n<p class=\"date\">\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante febrero 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\/6724"}],"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=6724"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6724\/revisions"}],"predecessor-version":[{"id":6725,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6724\/revisions\/6725"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6724"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6724"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6724"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}