{"id":6306,"date":"2018-11-01T08:10:21","date_gmt":"2018-11-01T07:10:21","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6306"},"modified":"2018-11-01T08:10:21","modified_gmt":"2018-11-01T07:10:21","slug":"resumen-de-lecturas-compartidas-durante-octubre-de-2018","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-octubre-de-2018\/","title":{"rendered":"Resumen de lecturas compartidas durante octubre de 2018"},"content":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante octubre 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:\/\/dl.acm.org\/citation.cfm?id=3241787\">From algebra to abstract machine: a verified generic construction<\/a>. ~ C. Tom\u00e9 Corti\u00f1as, W. Swierstra. #FunctionalProgramming #ITP #Agda<\/li>\n<li><a href=\"http:\/\/ctp.di.fct.unl.pt\/~btoninho\/depk_draft.pdf\">Refinement kinds (A theory of type-safe meta-programming)<\/a>. ~ L. Caires, B. Toninho. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3242766\">Typing the wild in Erlang<\/a>. ~ N. Valliappan, J. Hughes. #FunctionalProgramming #Erlang<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1809.10756\">An introduction to probabilistic programming<\/a>. ~ J.W. van de Meent, B. Paige, H. Yang, F. Wood. #FunctionalProgramming #Lisp #Clojure #FOPPL<\/li>\n<li><a href=\"https:\/\/gitlab.com\/jgkamat\/rmsbolt\">RMSbolt: A supercharged implementation of the godbolt compiler-explorer for Emacs<\/a>. ~ Jay Kamat. #Programming #Emacs<\/li>\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-septiembre-de-2018\/\">Resumen de lecturas compartidas durante septiembre de 2018<\/a>.<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Pi_Transcendental.html\">The transcendence of \u03c0 in Isabelle\/HOL<\/a>. ~ M. Eberl. #ITP #isabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/orbit.dtu.dk\/files\/154035749\/paper7.pdf\">Proving in the Isabelle proof assistant that the set of real numbers is not countable<\/a>. ~ J. Villadsen. #ITP #isabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/orbit.dtu.dk\/files\/154035393\/paper6.pdf\">Students&#8217; Proof Assistant (SPA)<\/a>. ~ A. Schlichtkrull, J. Villadsen, A.H. From. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/introduction-to-singletons-3.html\">Introduction to Singletons (Part 3)<\/a>. ~ Justin Le. #Haskell<\/li>\n<li><a href=\"https:\/\/alasconnect.github.io\/blog\/posts\/2018-10-02-introducing-haskell-to-a-company.html\">Introducing Haskell to a company<\/a>. ~ Brian Jones. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/matryoshka.gforge.inria.fr\/pubs\/schlichtkrull_phd_thesis.pdf\">Formalization of logic in the Isabelle proof assistant<\/a>. ~ A. Schlichtkrull. #PhD_Thesis #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/annals-csis.org\/proceedings\/2018\/drp\/pdf\/88.pdf\">Representation matters: An unexpected property of polynomial rings and its consequences for formalizing abstract field theory<\/a>. ~ C. Schwarzweller. #ITP #Mizar #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1810.01109\">AI benchmark: Running deep neural networks on Android smartphones<\/a>. ~ A. Ignatov et als. #AI #DeepLearning<\/li>\n<li><a href=\"http:\/\/prl.korea.ac.kr\/~pronto\/home\/papers\/oopsla18-fixml.pdf\">Automatic diagnosis and correction of logical errors for functional programming assignments<\/a>. ~ J. Lee et als. #FunctionalProgramming #OCaml via @scottfleischman<\/li>\n<li><a href=\"https:\/\/repository.upenn.edu\/edissertations\/2879\/\">Random testing for language design<\/a>. ~ L. Lampropoulos. #PhD_Thesis #ITP #Coq #QuickChick<\/li>\n<li><a href=\"https:\/\/alasconnect.github.io\/blog\/posts\/2018-10-04-productive-haskell-in-enterprise.html\">Productive Haskell in enterprise<\/a>. ~ Brian Jones. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/blog.nyarlathotep.one\/2018\/09\/rewrite-rules-and-a-specific-fold\/\">Rewrite rules and a specific fold: use optimization techniques from GHC.Base<\/a>. ~ Alexandre Moine. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/soupi\/haskell-study-plan\">Haskell study plan (an opinionated list of resources for learning Haskell)<\/a>. ~ Gil Mizrahi. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1810.00445\">An application of ASP theories of intentions to understanding restaurant scenarios: insights and narrative corpus<\/a>. ~ Q. Zhang, C. Benton, D. Inclezan. #LogicProgramming #ASP<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1810.00453\">anthem: Transforming gringo programs into first-order theories (preliminary report)<\/a>. ~ V. Lifschitz, P. L\u00fchne, T. Schaub. #LogicProgramming #ASP #ATP<\/li>\n<li><a href=\"https:\/\/jiggerwit.wordpress.com\/2018\/09\/18\/a-review-of-the-lean-theorem-prover\/\">A review of the Lean theorem prover<\/a>. ~ Thomas Hales. #ITP #LeanTheoremProver<\/li>\n<li><a href=\"https:\/\/madiot.fr\/coq100\/\">Formalizing 100 theorems in Coq<\/a>. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2018-10-04-capability.html\">capability: the ReaderT pattern without boilerplate<\/a>. ~ A. Herrmann, A. Spiwack. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/erkmos\/haskell-companies\">A gently curated list of companies using Haskell in industry<\/a>. ~ Erik Mossberg #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.fpcomplete.com\/blog\/2012\/09\/ten-things-you-should-know-about-haskell-syntax\">Ten things you should know about Haskell syntax<\/a>. ~ Bartosz Milewski #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.makeuseof.com\/tag\/python-programming-language-downsides\/\">4 reasons why Python isn\u2019t the programming language for you<\/a>. ~ Ian Buckley #Programming #Python<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2018\/10\/07\/what-is-the-xena-project\/\">What is the Xena Project?<\/a> ~ Kevin Buzzard #ITP #LeanTheoremProver #Math<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2018\/10\/06\/counting-inversions-with-monoidal-sparks\/\">Counting inversions with monoidal sparks<\/a>. ~ Brent Yorgey #FunctionalProgramming #Haskell #Math<\/li>\n<li><a href=\"http:\/\/www.parsonsmatt.org\/2018\/10\/02\/small_types.html\">Keep your types small \u2026 and your bugs smaller<\/a>. ~ Matt Parsons . #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/daniberg.com\/2018\/10\/02\/monads-for-fp-in-scala.html\">Monads for functional programming in Scala<\/a>. ~ Daniel Berg #FunctionalProgramming #Scala<\/li>\n<li><a href=\"http:\/\/downloads.hindawi.com\/journals\/mpe\/2018\/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:\/\/mml-book.com\/\">Companion webpage to the book &#8220;Mathematics for Machine Learning&#8221;<\/a>. ~ Marc Peter Deisenroth, A Aldo Faisal, and Cheng Soon Ong. #eBook #MachineLearning #Math<\/li>\n<li><a href=\"http:\/\/www.haskellforall.com\/2018\/10\/detailed-walkthrough-for-beginner.html\">Detailed walkthrough for a beginner Haskell program<\/a>. ~ G. Gonzalez . #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/lptk.github.io\/programming\/2018\/10\/04\/comprehending-monoids-with-class.html\">Comprehending Monoids with Class<\/a>. ~ Lionel Parreaux #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2018\/10\/8\/deeper-stack-knowledge\">Deeper Stack knowledge<\/a>. ~ James Bowen . #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/www.newthinktank.com\/2015\/08\/learn-haskell-one-video\/\">Learn Haskell in one video<\/a>. ~ Derek Banas. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/division-of-polynomials-in-haskell\">Division of polynomials in Haskell<\/a>. ~ Philip Zucker. #FunctionalProgramming #Haskell #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1810.02688\">Wikistat 2.0: Educational resources for Artificial Intelligence<\/a>. ~ P. Besse, B. Guillouet, B. Laurent #AI<\/li>\n<li><a href=\"https:\/\/github.com\/wikistat\/\">Wikistat 2.0: Tutoriels (calepins jupyter) d&#8217;auto-apprentissage en Science des Donn\u00e9es &amp; Intelligence artificielle<\/a>. #DataScience #AI<\/li>\n<li><a href=\"http:\/\/scholar.rose-hulman.edu\/cgi\/viewcontent.cgi?article=1217&amp;context=rhumj\">Fractals and the Weierstrass-Mandelbrot function<\/a>. ~ A. Zaleski #Math<\/li>\n<li><a href=\"http:\/\/www.ijpe-online.com\/attachments\/article\/1515\/02-IJPE-09-02.pdf\">Formal verification of helicopter automatic landing control algorithm in theorem prover Coq<\/a>. ~ X. Chen, G. Chen. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.mpg.is\/papers\/gissurarson2018suggesting-msc.pdf\">Suggesting valid hole fits for typed-holes in Haskell<\/a>. ~ Matth\u00edas P\u00e1ll Gissurarson. #Msc_Thesis #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1810.02142\">Propositional logic with short-circuit evaluation: a non-commutative and a commutative variant<\/a>. ~ J.A. Bergstra, A. Ponse, D.J.C. Staudt. #Logic #ATP #Prover9<\/li>\n<li><a href=\"https:\/\/whatthefunctional.wordpress.com\/2018\/10\/10\/making-a-haskell-interface-for-the-rosie-pattern-language\/\">Making a Haskell interface for the Rosie Pattern Language<\/a>. ~ Laurence Emms. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1810.04314\">The fundamental theorem of algebra in ACL2<\/a>. ~ R. Gamboa, J. Cowles. #ITP #ACL2 #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1810.04312\">Using ACL2 in the design of efficient, verifiable data structures for high-assurance systems<\/a>. ~ D. Hardin, K. Slind. #ITP #ACL2<\/li>\n<li><a href=\"https:\/\/samcgardner.github.io\/2018\/10\/06\/linear-regression-in-haskell.html\">An introduction to linear regression using Haskell<\/a>. ~ Sam Gardner. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/andrewgelman.com\/2018\/10\/11\/functional-programming-languages-popular-programming-languages-community\/\">Why are functional programming languages so popular in the programming languages community?<\/a> #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mitpress.mit.edu\/books\/art-prolog-second-edition\">The art of Prolog, second edition (Advanced programming techniques)<\/a>. ~ L.S. Sterling, E.Y. Shapiro. #Open #eBook #LogicProgramming #Prolog<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1810.04315\">Real vector spaces and the Cauchy-Schwarz inequality in ACL2(r)<\/a>. ~ C. Kwan, M.R. Greenstreet. #ITP #ACL2 #Math<\/li>\n<li><a href=\"https:\/\/www.ideals.illinois.edu\/bitstream\/handle\/2142\/100116\/K-semantics-tech-report.pdf\">IsaK: a complete semantics of K<\/a>. ~ L. Li, E.L. Gunter. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/haskanything.com\/\">Hask Anything!: a website aimed at collecting and organizing the collective knowledge of the Haskell community<\/a>. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/wiki.haskell.org\/Functional_programming\">Functional programming<\/a>. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.technologyreview.com\/s\/612263\/the-us-military-wants-to-teach-ai-some-basic-common-sense\">The US military wants to teach AI some basic common sense<\/a>. ~ Will Knight. #AI<\/li>\n<li><a href=\"https:\/\/joshchen.io\/pdfs\/implementation-hott-isabelle.pdf\">An implementation of Homotopy Type Theory in Isabelle\/Pure<\/a>. ~ J. Chen . #Msc_Thesis #ITP #Isabelle #HoTT<\/li>\n<li><a href=\"https:\/\/github.com\/jaycech3n\/Isabelle-HoTT\">Isabelle\/HoTT: An experimental implementation of HoTT in the interactive proof assistant Isabelle<\/a>. J. Chen. #ITP #Isabelle #HoTT<\/li>\n<li><a href=\"https:\/\/eprint.iacr.org\/2018\/941.pdf\">A tutorial introduction to CryptHOL<\/a>. ~ A. Lochbihler, S.R. Sefidgar. #ITP #IsabelleHOL #CryptHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1810.04309\">Formalising filesystems in the ACL2 theorem prover: an Application to FAT32<\/a>. ~ Mihir Parang Mehta. #ITP #ACL2<\/li>\n<li><a href=\"https:\/\/www.ahri.net\/practical-haskell-programs-from-scratch\/\">Practical Haskell programs from scratch (a quick and easy guide)<\/a>. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/drive.google.com\/file\/d\/1qexG1WABkK56G9XJsw9McRCdPVbGBJBj\/view\">Headfirst into Haskell<\/a>. ~ Abby Sassel. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/ranjitjhala.github.io\/static\/ctfp-ccs18.pdf\">Towards verified, constant-time floating point operations<\/a>. ~ M. Andrysco et als. #FunctionalProgramming #Haskell #SMT<\/li>\n<li><a href=\"https:\/\/jaspervdj.be\/posts\/2018-09-04-binomial-heaps-101.html\">Dependent types in Haskell: Binomial heaps 101 (Who put binary numbers in my type system?)<\/a>. ~ Jasper Van der Jeugt. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1810.04311\">Incremental SAT library integration in ACL2 using abstract stobjs<\/a>. ~ Sol Swords. #ITP #ACL2 #SAT<\/li>\n<li><a href=\"http:\/\/blog.ezyang.com\/2018\/09\/hiw18-lets-go-mainstream-with-eta\/\">#HIW18: Let\u2019s go mainstream with Eta!<\/a>. ~ Rahul Muttineni . #FunctionalProgramming #Haskell #Eta<\/li>\n<li><a href=\"https:\/\/icfp18.sigplan.org\/event\/hiw-2018-papers-corespec-verifying-ghc-with-hs-to-coq\">CoreSpec: Verifying GHC with hs-to-coq<\/a>. ~ Antal Spector-Zabusky et als. #FunctionalProgramming #Haskell #ITP #Coq<\/li>\n<li><a href=\"https:\/\/icfp18.sigplan.org\/event\/hiw-2018-papers-coercion-quantification\">Coercion quantification<\/a>. ~ N. Xie, R.A. Eisenberg. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/guide.aelve.com\/haskell\">Aelve Guide: Wiki for the Haskell ecosystem<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/ajlopez\/AprendiendoDeepLearning\">Enlaces y recursos sobre redes neuronales y deep learning<\/a>. ~ @ajlopez #AI #NeuralNetworks #DeepLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1810.04316\">Convex functions in ACL2(r)<\/a>. ~ C. Kwan, M.R. Greenstreet. #ITP #ACL2 #Math<\/li>\n<li><a href=\"https:\/\/github.com\/RKlompUU\/SCRIPTWriter\">ESCRIPT: a human readable language for programming Bitcoin scripts<\/a>. ~ Rick Klomp. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/RKlompUU\/SCRIPTAnalyser\">SCRIPT Analyser: Symbolic verification of Bitcoin&#8217;s output scripts<\/a>. ~ Rick Klomp. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/medium.com\/@cdsmithus\/fixpoints-in-haskell-294096a9fc10\">Fixpoints in Haskell<\/a>. ~ Chris Smith. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/typeclasses.com\/javascript\/monoidal-folds\">A JavaScript WAT and monoidal folds<\/a>. ~ Julie Moronuki and Chris Martin. #JavaScript #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/volhovM\/orgstat\">Orgstat: a statistics visualizer tool for org-mode<\/a>. ~ Mikhail Volkhov. #Haskell #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/github.com\/orome\/crypto-enigma-hs\">A Haskell Enigma machine simulator with rich display and machine state details<\/a>. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/wiki.haskell.org\/index.php?title=Haskell_in_industry\">Haskell in industry<\/a>. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/openlibra.com\/es\/book\/learn-programming\">Learn programming<\/a>. ~ A. Salonen. #eBook #Programming #OpenLibra<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1810.05315\">Learning to reason (Theorem proving at first order via reinforcement learning)<\/a>. ~ Brian Groenke. #Logic #ATP #MachineLearning<\/li>\n<li><a href=\"https:\/\/twobithistory.org\/2018\/10\/14\/lisp.html\">How Lisp became God&#8217;s own programming language<\/a>. ~ Sinclair Target . #Programming #Lisp<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1810.05666\">DefunT: A tool for automating termination proofs by using the community books<\/a>. ~ Matt Kaufmann. #ITP #ACL2<\/li>\n<li><a href=\"https:\/\/github.com\/MaiaVictor\/cedille-core\">Cedille-Core: A minimal (600 LOC) programming language capable of proving theorems about its own terms<\/a>. #ITP #Logic #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/maiavictor\/formality\">Formality: An efficient programming language and proof assistant<\/a>. #ITP #Cedille<\/li>\n<li><a href=\"https:\/\/github.com\/nkarag\/haskell-DBFunctor\">DBFunctor: Functional data management (type safe ETL\/ELT in Haskell)<\/a>. ~ Nikos Karagiannidis. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/anthonybonato.com\/2018\/10\/17\/problem-solving-vs-proving\/\">Problem solving vs proving<\/a>. ~ Anthony Bonato #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Factored_Transition_System_Bounding.html\">Upper bounding diameters of state spaces of factored transition systems in Isabelle\/HOL<\/a>. F. Kurz and M. Abdulaziz. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/github.com\/granule-project\/granule\">Granule: a statically typed functional language with graded modal types for fine-grained program reasoning via types<\/a>. ~ Dominic Orchard #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/sbmf\/sbmf.pdf\">Programming language foundations in Agda<\/a>. ~ P. Wadler. #ITP #Agda #Coq<\/li>\n<li><a href=\"https:\/\/plfa.github.io\/\">Programming language foundations in Agda<\/a>. ~ P. Wadler, W. Kokke. #eBook #ITP #Agda #Coq<\/li>\n<li><a href=\"http:\/\/ilyasergey.net\/papers\/temporal-isola18.pdf\">Temporal properties of smart contracts<\/a>. ~ I. Sergey, A. Kumar, A. Hobor. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/perso.telecom-paristech.fr\/bloch\/OptionIA\/Logics-SymbolicAI.html\">Logics and symbolic Artificial Intelligence<\/a>. ~ Isabelle Bloch, Natalia D\u00edaz Rodr\u00edguez. #AI #Logic<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Randomised_BSTs.html\">Randomised binary search trees in Isabelle\/HOL<\/a>. ~ M. Eberl #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/diogocastro.com\/blog\/2018\/10\/17\/haskells-kind-system-a-primer\/\">Haskell&#8217;s kind system (a primer)<\/a>. ~ D. Castro. #Haskell<\/li>\n<li><a href=\"http:\/\/blog.ploeh.dk\/2018\/10\/15\/an-applicative-password-list\">An applicative password list<\/a>. ~ M. Seemann. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/chame.co\/writeups\/sum_and_product\/post.html\">Sigma, Pi, Sum, Product<\/a>. ~ Samuel Breese. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/diginomica.com\/2018\/06\/04\/ai-curve-fitting-not-intelligence\">AI today and tomorrow is mostly about curve fitting, not intelligence<\/a>. ~ Kurt Marko. #AI #DeepLearning<\/li>\n<li><a href=\"https:\/\/elpais.com\/tecnologia\/2018\/03\/16\/actualidad\/1521204836_317670.html\">M\u00e1quinas listas, pero sin sentido com\u00fan<\/a>. ~ Ramon L\u00f3pez de M\u00e1ntaras. #IA<\/li>\n<li><a href=\"http:\/\/www.mit.edu\/~tomeru\/papers\/machines_that_think.pdf\">Building machines that learn and thinlike people<\/a>. ~ B.M. Lake, T.D. Ullman, J.B. Tenenbaum, S.J. Gershman. #AI<\/li>\n<li><a href=\"http:\/\/binaire.blog.lemonde.fr\/2018\/10\/20\/algorithmes-a-la-recherche-de-luniversalite-perdue\/\">Algorithmes: \u00e0 la recherche de l\u2019universalit\u00e9 perdue<\/a>. ~ Rachid Guerraoui #CompSci<\/li>\n<li><a href=\"http:\/\/verse.systems\/blog\/post\/2018-10-02-Proofs-And-Side-Effects\/\">Proofs and side effects (Understanding the promise and the fine print of formal methods for security)<\/a>. ~ Toby Murray. #ITP<\/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 Oorscho. #ITP<\/li>\n<li><a href=\"http:\/\/blog.sigfpe.com\/2018\/10\/running-from-past.html\">Running from the past<\/a>. ~ Dan Piponi. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/blog.plover.com\/prog\/haskell\/traversable.html\">Mark Dominus: I struggle to understand Traversable<\/a>. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/wiki.haskell.org\/Cookbook\">The Haskell Cookbook<\/a>. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/babbagefiles.xyz\/next_browser-common_lisp\/\">Browsing the Web with Common Lisp<\/a>. #Lisp #CommonLisp #Web #NextBrowser<\/li>\n<li><a href=\"http:\/\/next.atlas.engineer\/\">Next: a keyboard-oriented, extensible web-browser inspired by Emacs and designed for power users<\/a>. #Lisp #CommonLisp #Web #NextBrowser<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1810.08380\">Formalizing computability theory via partial recursive functions<\/a>. ~ M. Carneiro. #ITP #Lean<\/li>\n<li><a href=\"https:\/\/gmalecha.github.io\/reflections\/2018\/denotational-imp\">A denotational semantics for an imperative language<\/a>. ~ G. Malecha . #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Lambda_Free_EPO.html\">Formalization of the embedding path order for lambda-free higher-order terms<\/a>. ~ A. Bentkamp. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/vadosware.io\/post\/rest-ish-services-in-haskell-part-1\/\">REST-ish services in Haskell (Part 1)<\/a>. ~ @vadosware #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/javpelle\/ComputerAlgebra\">Some computer algebra algorithms in Haskell<\/a>. ~ J. Pellejero. #FunctionalProgramming #Haskell #Math<\/li>\n<li><a href=\"https:\/\/chalkdustmagazine.com\/features\/an-invitation-to-category-theory\/\">An invitation to category theory<\/a>. ~ Tai-Danae Bradley. #CategoryTheory<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-02508-3_10.pdf\">Layer systems for confluence \u2014 formalized<\/a>. ~ B. Felgenhauer, F. Rapp #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Prime_Number_Theorem.html\">The prime number theorem in Isabelle\/HOL<\/a>. ~ M. Eberl, L. Paulson. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2018\/11\/12\/elm-more-functional-frontend\">Elm: Functional frontend!<\/a> ~ James Bowen. #FunctionalProgramming #Elm<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/introduction-to-singletons-4.html\">Introduction to Singletons (Part 4)<\/a>. ~ Justin Le. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/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:\/\/www.csc.kth.se\/~jsannemo\/slask\/main.pdf\">Principles of algorithmic problem solving<\/a>. ~ J. Sannemo. #eBook #Algorithms #Programming #CompSci<\/li>\n<li><a href=\"http:\/\/knowledge.wharton.upenn.edu\/article\/student-loan-debt-crisis\/\">The student debt crisis: Could it slow the U.S. economy?<\/a><\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-01897468\/document\">Deriving proved equality tests in Coq-elpi (Stronger induction principles for containers in Coq)<\/a>. ~ E. Tassi. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/in-computers-we-trust-20130222\/\">In computers we trust? (As math grows ever more complex, will computers reign?)<\/a> #Math #CompSci #ITP<\/li>\n<li><a href=\"http:\/\/web.eecs.umich.edu\/~cpeikert\/pubs\/alchemy.pdf\">Alchemy: A Language and Compiler for Homomorphic Encryption Made easY<\/a>. ~ E. Crockett, C. Peikert, C. Sharp. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dimjasevic.net\/marko\/2018\/10\/23\/typed-functional-programming-and-software-correctness\">Typed functional programming and software correctness<\/a>. ~ Marko Dimja\u0161evi\u0107. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.softwaremill.com\/algebraic-data-types-in-four-languages-858788043d4e\">Algebraic Data Types in four languages (A comparison)<\/a>. ~ #Haskell #Scala #Rust #TypeScript<\/li>\n<li><a href=\"https:\/\/medium.com\/@scott_jones\/third-wave-ai-the-coming-revolution-in-artificial-intelligence-1ffd4784b79e\">Third wave AI: The coming revolution in Artificial Intelligence<\/a>. ~ Scott Jones. #AI<\/li>\n<li><a href=\"https:\/\/www.darpa.mil\/about-us\/darpa-perspective-on-ai\">A DARPA perspective on Artificial Intelligence<\/a>. ~ John Launchbury. #AI<\/li>\n<li><a href=\"https:\/\/www.bbc.com\/news\/business-44466213\">Can we trust AI if we don&#8217;t know how it works?<\/a> ~ Marianne Lehnis. #AI<\/li>\n<li><a href=\"https:\/\/www.youtube.com\/watch?v=T6ohwZNL0RQ\">Assuring AI<\/a>. ~ John Launchbury. #AI<\/li>\n<li><a href=\"https:\/\/code.world\/doc.html?shelf=help\/codeworld.shelf&amp;path=help\/GuideUnit1.md#13\">CodeWorld guide<\/a>. ~ Chris Smith. #Haskell #CodeWorld #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/P8fgFCSAqYs\">Solving russian calendar problems in Haskell (HaskellRank Ep.08)<\/a>. ~ Alexey Kutepov. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/2Pm3Sxc\">Los cuadrados y la factorizaci\u00f3n<\/a>. ~ Juan Arias de Reyna. #Matematicas #Computacion<\/li>\n<li><a href=\"https:\/\/www.ams.org\/journals\/notices\/199612\/pomerance.pdf\">A tale of two sieves<\/a>. ~ C. Pomerance. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/magazines\/2018\/11\/232193-ai-explain-yourself\/fulltext\">AI, explain yourself<\/a>. ~ Don Monroe. #AI #XAI<\/li>\n<li><a href=\"https:\/\/www.teslarati.com\/darpa-us-defense-ai-common-sense-machine-learning\/\">US Department of Defense commits $2B to training AI to have \u201ccommon sense\u201d<\/a>. #AI<\/li>\n<li><a href=\"https:\/\/www.ciodive.com\/news\/ai-talent-pipeline-clogged-by-education-programs-slow-or-unable-to-change\/540497\/\">AI talent pipeline clogged by education programs slow or unable to change<\/a>. #AI<\/li>\n<li><a href=\"https:\/\/francis.naukas.com\/2011\/07\/13\/para-que-sirven-las-matematicas\/\">Para qu\u00e9 sirven las matem\u00e1ticas<\/a>. ~ Francisco R. Villatoro #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/www3.math.tu-berlin.de\/combi\/wp_henk\/wp-content\/uploads\/2011\/08\/475166a-The+unplanned+impact+of+mathematics.pdf\">The unplanned impact of mathematics<\/a>. ~ P. Rowlett. #Math<\/li>\n<li><a href=\"https:\/\/es.slideshare.net\/AlejandroMena6\/build-your-own-monads\">Build your own monads<\/a>. ~ A. Serrano. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/anchpop.github.io\/wise_mans_haskell\">Wise man\u2019s Haskell (Free book for learning Haskell)<\/a>. ~ Andre Popovitch. #eBook #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/drive.google.com\/file\/d\/1ikKuK6T2xccLynvdAVjGGZ029zjQlGAX\/view\">Headfirst into Haskell<\/a>. ~ Abby Sassel. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.slideshare.net\/LukaJacobowitz\/testing-in-the-world-of-functional-programming\">Testing in the World of Functional Programming<\/a>. ~ Luka Jacobowitz . #FunctionalProgramming #Scala<\/li>\n<li><a href=\"https:\/\/theconversation.com\/statistics-and-data-science-degrees-overhyped-or-the-real-deal-102958\">Statistics and data science degrees: Overhyped or the real deal?<\/a> ~ P. Richard Hahn #DataScience<\/li>\n<li><a href=\"http:\/\/cleilaclo2018.mackenzie.br\/docs\/SIESC\/182774.pdf\">A functional paradigm using the C language for teaching Programming for Engineers<\/a>. ~ V. Theoktisto. #Teaching #Programming #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/George_Baryannis\/publication\/328282705_Legal_Representation_and_Reasoning_in_Practice_A_Critical_Comparison\/links\/5bc9cb06a6fdcc03c7941e70\/Legal-Representation-and-Reasoning-in-Practice-A-Critical-Comparison.pdf\">Legal representation and reasoning in practice: a critical comparison<\/a>. ~ S. Batsakis et als. #KRR #ASP #Logic #AI<\/li>\n<li><a href=\"https:\/\/stratos.seas.harvard.edu\/files\/stratos\/files\/periodictabledatastructures.pdf\">The periodic table of data structures<\/a>. ~ S. Idreos et als. #Algorithmic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1808.02066.pdf\">The internals of the data calculator<\/a>. ~ S. Idreos et als. #Algorithmic<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Epistemic_Logic.html\">Epistemic logic in Isabelle\/HOL<\/a>. ~ Andreas Halkj\u00e6r From . #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/ptival.github.io\/card-game-04\">Creating a card game in Haskell (part 4)<\/a>. ~ Valentin Robert #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/2RnL3qv\">Fourier, Cantor, las series trigonom\u00e9tricas y la teor\u00eda de conjuntos<\/a>. ~ Pedro J. Pa\u00fal #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/dimjasevic.net\/marko\/2018\/10\/23\/typed-functional-programming-and-software-correctness\/\">Typed functional programming and software correctness<\/a>. ~ Marko Dimja\u0161evi\u0107. #FunctionalProgramming #Haskell #Agda<\/li>\n<li><a href=\"http:\/\/qfpl.io\/posts\/intro-to-state-machine-testing-1\">Introduction to state machine testing: part 1<\/a>. ~ Andrew McMiddlin #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/nickseagull.github.io\/lw-eta-2018\">Pragmatic development in Eta<\/a>. ~ Nick Tchayka. #FunctionalProgramming #Haskell #Eta<\/li>\n<li><a href=\"http:\/\/www.cis.syr.edu\/~sueo\/cis252\">Course CIS 252: Introduction to Computer Science<\/a>. ~ Susan Older #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3276946\">A trustworthy mechanized formalization of R<\/a>. ~ M. Bodin, T. Diaz, \u00c9. Tanter. #ITP #Coq #RStat<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1803.06494\">Attack trees in Isabelle<\/a>. ~ F. Kamm\u00fcller. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-01903752\/document\">A generic Coq proof of typical worst-case analysis<\/a>. ~ P. Fradet, M. Lesourd, J.F. Monin, S. Quinton. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/ivanperez-keera\/simple-affine-space\">A simple implementation of affine spaces and vector spaces in Haskell<\/a>. #FunctionalProgramming #Haskell #Math<\/li>\n<li><a href=\"https:\/\/www.hindawi.com\/journals\/tswj\/2014\/834237\">The laws of natural deduction in inference by DNA computer<\/a>. ~ \u0141. Rogowski, P. Sos\u00edk. #Logic #DNAcomputing<\/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 octubre 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":[177],"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\/6306"}],"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=6306"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6306\/revisions"}],"predecessor-version":[{"id":6307,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6306\/revisions\/6307"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6306"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6306"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6306"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}