{"id":6918,"date":"2019-12-01T07:09:24","date_gmt":"2019-12-01T06:09:24","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6918"},"modified":"2020-01-07T07:12:21","modified_gmt":"2020-01-07T06:12:21","slug":"resumen-de-lecturas-compartidas-durante-noviembre-de-2019","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-noviembre-de-2019\/","title":{"rendered":"Resumen de lecturas compartidas durante noviembre de 2019"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante noviembre 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>.<\/p>\n<p><!--more--><\/p>\n<ul class=\"org-ul\">\n<li><a href=\"http:\/\/www.philipzucker.com\/neural-networks-with-weighty-lenses-dioptics\/\">Neural Networks with Weighty Lenses (DiOptics?)<\/a> ~ Philip Zucker (@SandMouth). #Haskell #NeuralNetworks #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mitibmwatsonailab.mit.edu\/research\/publications\/paper\/download\/The-Future-of-Work-How-New-Technologies-Are-Transforming-Tasks.pdf\">The future of work: How new technologies are transforming tasks<\/a>. ~ M. Fleming et als. #AI #ML<\/li>\n<li><a href=\"https:\/\/jkeuhlen.com\/2019\/10\/19\/Compile-Your-Comments-In-Ghcid.html\">Compile your comments in ghcid<\/a>. ~ Jake Keuhlen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mbuffett.com\/scraping-goodreads-sitemaps-with-haskell\/\">Scraping Goodreads Sitemaps with Haskell<\/a>. ~ Marcus Buffett. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/maxhallinan.com\/posts\/2019\/10\/22\/how-does-the-continuation-monad-work\/\">How does the continuation monad work?<\/a> ~ Max Hallinan. #PureScript #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/copilot-language.github.io\/\">Copilot: A stream DSL for writing embedded C programs<\/a>. ~ Lee Pike (@pike7464). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.technologyreview.es\/s\/11589\/esta-ia-resuelve-un-antiguo-problema-matematico-mucho-mas-rapido\">Esta IA resuelve un antiguo problema matem\u00e1tico mucho m\u00e1s r\u00e1pido<\/a>. #IA<\/li>\n<li><a href=\"https:\/\/blog.ploeh.dk\/2019\/10\/28\/a-basic-haskell-solution-to-the-robot-journeys-coding-exercise\/\">A basic Haskell solution to the robot journeys coding exercise<\/a>. ~ Mark Seemann (@ploeh). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/wwwf.imperial.ac.uk\/~buzzard\/xena\/natural_number_game\/\">The natural number game (version 1.06)<\/a>. ~ K. Buzzard, M. Pedramfar. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/github.com\/philzook58\/learnxinyminutes-docs\/blob\/master\/coq.html.markdown\">Learn Coq in Y minutes tutorial<\/a>. ~ Philip Zucker (@SandMouth). #ITP #Coq<\/li>\n<li><a href=\"https:\/\/youtu.be\/bL6dL1fUTxY\">No Garden of Eden: Adventures in Teaching Haskell to Kids<\/a>. ~ Peter Berger (@peterb). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cs.cornell.edu\/courses\/cs4860\/2019fa\/lectures\/L2-A-Story-of-Logic.pdf\">The story of Logic<\/a>. ~ Robert L. Constable. #Logic #Math #ITP<\/li>\n<li><a href=\"http:\/\/www.cs.cornell.edu\/courses\/cs4860\/2019fa\/lectures\/L5-Comp-Foundations-of-Math.pdf\">Computational foundations of Mathematics<\/a>. ~ Robert L. Constable. #Logic Math #CompSci #ITP #Nuprl<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1906.06469\">Approximate normalization for gradual dependent types<\/a>. ~ J. Eremondi, \u00c9. Tanter, R. Garcia. #GDTL<\/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 #LeanProver<\/li>\n<li><a href=\"https:\/\/www.microsiervos.com\/archivo\/ia\/inteligencia-artificial-notas-sobresalientes-examenes-ciencias.html\">La inteligencia artificial capaz de puntuar con notas sobresalientes en los ex\u00e1menes de ciencias<\/a>. ~ @Alvy. #IA<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1909.01958\">From &#8216;F&#8217; to &#8216;A&#8217; on the N.Y. Regents Science Exams: An Overview of the Aristo Project<\/a>. ~ P. Clark et als. #AI<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1911.00399\">An implementation of Homotopy Type Theory in Isabelle\/Pure<\/a>. ~ J. Chen. #MSc_Thesis #ITP #IsabellePure #HoTT<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1911.00385\">A formal proof of PAC learnability for decision stumps<\/a>. ~ J. Tassarotti, J.B. Tristan, K. Vajjha. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2019-11-02-how-to-binary-random-access-list.html\">How to do binary random-access lists simply<\/a>. ~ Donnacha Ois\u00edn Kidney (@oisdk). #Agda #FunctionalProgramming #ITP<\/li>\n<li><a href=\"http:\/\/www.well-typed.com\/blog\/2019\/11\/unrolling-data-with-backpack\/\">Unrolling data with Backpack<\/a>. ~ Oleg Grenrus. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/archives\/fall2019\/entries\/category-theory\">Category Theory<\/a>. ~ Jean-Pierre Marquis. #CategoryTheory.<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1910.13975\">A brief tour of logic and optimization<\/a>. ~ J. Hooker. #Logic #Optimization<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/ZFC_in_HOL.html\">Zermelo Fraenkel Set Theory in Higher-Order Logic<\/a>. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1910.13554\">Differential Hoare logics and refinement calculi for hybrid systems with Isabelle\/HOL<\/a>. ~ S. Foster, G. Struth. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02333564\/document\">CoqTL: A Coq DSL for rule-based model transformation<\/a>. ~ Z. Cheng, M. Tisi, R. Douence. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/www.academia.edu\/download\/59970953\/IRJET-V6I553520190709-100880-1y6qr3f.pdf\">Recent trends in STM Haskell<\/a>. ~ P. Tiwari, S. Meenu. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1911.00580\">Introduction to univalent foundations of mathematics with Agda<\/a>. ~ Mart\u00edn H\u00f6tzel Escard\u00f3. #ITP #Agda HoTT<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/Publications\/documents\/ForsterStark_2019_CoqALaCarte.pdf\">Coq \u00e0 la carte (A practical approach to modular syntax with binders)<\/a>. ~ Y. Forster, K. Stark. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/bartoszmilewski.com\/2019\/11\/06\/fixed-points-and-diagonal-arguments\/\">Fixed points and diagonal arguments<\/a>. ~ Bartosz Milewski (@BartoszMilewski). #Haskell #Math<\/li>\n<li><a href=\"https:\/\/lisp-journey.gitlab.io\/pythonvslisp\/\">Python VS Common Lisp, workflow and ecosystem<\/a>. #Python #CommonLisp<\/li>\n<li><a href=\"https:\/\/yairchu.github.io\/posts\/sum-type-encodings.html\">The four simple ways to encode sum-types<\/a>. ~ Yair Chuchem (@yairchu). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/bor0.wordpress.com\/2019\/11\/06\/proving-groupoids-with-idris\/\">Proving groups with Idris<\/a>. ~ Boro Sitnikovski## (@BSitnikovski). #Idris #FunctionalProgramming #ITP<\/li>\n<li><a href=\"http:\/\/prologhub.pl\/predicates-vs-functions\/\">Predicates vs functions<\/a>. ~ Paul Brown. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/elpais.com\/elpais\/2019\/11\/06\/ciencia\/1573042148_224789.html\">Qu\u00e9 es la teor\u00eda de categor\u00edas y c\u00f3mo se ha convertido en tendencia<\/a>. ~ John Baez (@johncarlosbaez). #Teor\u00eda_de_categor\u00edas #L\u00f3gica #Matem\u00e1ticas #Computaci\u00f3n<\/li>\n<li><a href=\"http:\/\/bit.ly\/2pXFffg\">El problema de Collatz<\/a>. ~ Juan Arias de Reyna. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2019-11-08-monad-bayes-2.html\">Probabilistic programming with Monad\u2011Bayes, Part 2: Linear regression<\/a>. ~ S. Bhat, M. Meschede. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/Publications\/documents\/ForsterEtAl_2019_VerifiedTMs.pdf\">Verified programming of Turing machines in Coq<\/a>. ~ Y. Forster, F. Kunze, M. Wuttke. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/es.cs.uni-kl.de\/publications\/datarsg\/Pete19.pdf\">Intuitionistic logic: a view of its evolution<\/a>. ~ A.K. Peters. #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/ir.canterbury.ac.nz\/handle\/10092\/17558\">Minimal logic and automated proof verification<\/a>. ~ L. Warren. #PhD_Thesis #ITP #Agda #Logic<\/li>\n<li><a href=\"https:\/\/www.methodist.edu\/wp-content\/uploads\/2019\/01\/mr2018_shane.pdf\">Figurate numbers: a historical survey of an ancient mathematics<\/a>. ~ D. Shane. #Math #History<\/li>\n<li><a href=\"https:\/\/k-bx.github.io\/articles\/propositions-as-types-missing-links.html\">Propositions as types: some missing links<\/a>. ~ Kostiantyn Rybnikov (@ko_bx). #Agda #ITP #Math<\/li>\n<li><a href=\"https:\/\/bor0.wordpress.com\/2019\/11\/09\/formalizing-expresiveness-of-line-editors\/\">Formalizing expressiveness of line editors<\/a>. ~ Boro Sitnikovski. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/youtu.be\/UebPmYcI13M\">Commanding Emacs from Coq<\/a>. #ITP #Coq #Emacs<\/li>\n<li><a href=\"https:\/\/rjlipton.wordpress.com\/2019\/11\/11\/goldbach-a-curious-conjecture\/\">Goldbach: a curious conjecture<\/a>. ~ R.J. Lipton, K.W. Regan. #Math<\/li>\n<li><a href=\"https:\/\/github.com\/i-am-tom\/haskell-exercises\">GHC exercises (A little course to learn about some of the more obscure GHC extensions)<\/a>. ~ Tom Harding (@am_i_tom). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/linear-relation-algebra-of-circuits-with-hmatrix\/\">Linear relation algebra of circuits with HMatrix<\/a>. ~ Philip Zucker (@SandMouth). #Haskell #FunctionalProgramming<\/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 #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/marcosh.github.io\/post\/2019\/11\/11\/named-typeclasses-in-haskell.html\">Named typeclasses in Haskell<\/a>. ~ Marco Perone (@marcoshuttle). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3359759\">Source-free machine-checked validation of native code in Coq<\/a>. ~ K.W. Hamlen, D.Fisher, G.R. Lundquist. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1910.11724\">Embracing a mechanized formalization gap<\/a>. ~ A. Spector-Zabusky, J. Breitner, Y. Li, S. Weirich #ITP #Coq #Haskell via @scottfleischman<\/li>\n<li><a href=\"https:\/\/github.com\/jtassarotti\/coq-proba\">A probability theory library for the Coq theorem prover<\/a>. ~ J. Tassarotti. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/337005820_Formalizing_the_Dependency_Pair_Criterion_for_Innermost_Termination\">Formalizing the dependency pair criterion for innermost termination<\/a>. ~ A. Alves Almeida, M. Ayala-Rinc\u00f3n. #ITP #PVS<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1712.04375\">Computational logic: its origins and applications<\/a>. ~ L.C. Paulson. #Logic #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1804.07860\">Formalising mathematics in simple type theory<\/a>. ~ L.C. Paulson. #Logic #Math #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2019-11-15-small-proof-fin-inj.html\">A small proof that fin is injective<\/a>. ~ Donnacha Ois\u00edn Kidney (@oisdk). #ITP #Agda<\/li>\n<li><a href=\"https:\/\/www.declanoller.com\/2019\/11\/15\/variational-autoencoders-in-haskell-or-how-i-learned-to-stop-worrying-and-turn-my-friends-into-dogs\/\">Variational autoencoders in Haskell, or: how I learned to stop worrying and turn my friends into dogs<\/a>. ~ @heyitdeclan #Haskell #FunctionalProgramming via @SandMouth<\/li>\n<li><a href=\"https:\/\/logtalk.org\/2019\/11\/13\/many-worlds-design-pattern.html\">The &#8220;many worlds&#8221; design pattern<\/a>. ~ Paulo Moura. #LogicProgramming<\/li>\n<li><a href=\"https:\/\/prologhub.pl\/facts-and-fluents-vs-constants-and-variables\/\">Facts and fluents vs constants and variables<\/a>. ~ Paul Brown. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/logtalk.org\/2019\/11\/14\/abstracting-user-interaction.html\">Abstracting user interaction<\/a>. ~ Paulo Moura. #LogicProgramming<\/li>\n<li><a href=\"http:\/\/uu.diva-portal.org\/smash\/get\/diva2:1369286\/FULLTEXT01.pdf\">Monads in Haskell and category theory<\/a>. ~ Samuel Grahn. #Haskell #FunctionalProgramming #CategoryTheory<\/li>\n<li><a href=\"http:\/\/uu.diva-portal.org\/smash\/get\/diva2:1369180\/FULLTEXT01.pdf\">Cofree traversable functors<\/a>. ~ L. Waern. #Haskell #FunctionalProgramming #CategoryTheory<\/li>\n<li><a href=\"http:\/\/www3.risc.jku.at\/publications\/download\/risc_5936\/AXolotlPaper.pdf\">AXolotl: A self-study tool for first-order logic<\/a>. ~ David M. Cerna. #Logic<\/li>\n<li><a href=\"https:\/\/kwarc.info\/people\/frabe\/students\/muller_phd.pdf\">Mathematical knowledge management across formal libraries<\/a>. ~ D. M\u00fcller. #PhD_Thesis #MKM #ITP #PVS<\/li>\n<li><a href=\"https:\/\/taylor.fausak.me\/2019\/11\/16\/haskell-survey-results\">2019 state of Haskell survey results<\/a>. ~ Taylor Fausak (@taylorfausak). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1911.06643\">Forgetting to learn logic programs<\/a>. ~ Andrew Cropper. #ILP #LogicProgramming<\/li>\n<li><a href=\"https:\/\/geekingfrog.com\/blog\/post\/swappable-db\">Swap the DB based on a config file<\/a>. ~ Gr\u00e9goire Charvet. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/ozanerdem.github.io\/jekyll\/update\/2019\/11\/17\/representation-in-sat.html\">Encoding problems in boolean satisfiability<\/a>. ~ Ozan Erdem (@ozanerdem). #Logic #SAT_solving<\/li>\n<li><a href=\"https:\/\/github.com\/adjoint-io\/galois-fft\">Finite field polynomial arithmetic based on fast Fourier transforms<\/a>. ~ Stephen Diehl (@smdiehl). #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/ondahostil.wordpress.com\/2019\/10\/16\/mi-entorno-de-trabajo\/\">Mi entorno de trabajo en Emacs<\/a>. ~ Ondiz. #Emacs<\/li>\n<li><a href=\"https:\/\/sxysun.github.io\/files\/210\/main.pdf\">Category theory as a methodology for computational sciences<\/a>. ~ Xinyuan Sun. #CategoryTheory #Haskell<\/li>\n<li><a href=\"https:\/\/www.lri.fr\/~wolff\/papers\/conf\/2019-fide-isabelle_c.pdf\">Deeply integrating C11 code support into Isabelle\/PIDE<\/a>. ~ F. Tuong, B. Wolff. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/geekingfrog.com\/blog\/post\/deriving-magic-and-parsing-csv\">Deriving magic and parsing CSV<\/a>. ~ Gr\u00e9goire Charvet. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cs.umd.edu\/~rrand\/vqc\">Verified quantum computing<\/a>. ~ Robert Rand. #ITP #Coq #QuantumComputing<\/li>\n<li><a href=\"http:\/\/www.cs.umd.edu\/~rrand\/thesis.pdf\">Formally verified quantum programming<\/a>. ~ Robert Rand. #PhD_Thesis #ITP #Coq #QuantumComputing<\/li>\n<li><a href=\"https:\/\/github.com\/jldodds\/coq-lean-cheatsheet\">A quick reference for mapping Coq tactics to Lean tactics<\/a>. ~ Joey Dodds. #ITP #Coq #LeanProver<\/li>\n<li><a href=\"https:\/\/www.snoyman.com\/blog\/2019\/11\/boring-haskell-manifesto\">Boring Haskell manifesto (how to get Haskell into your organization, and how to make your organization more productive and profitable with better engineering)<\/a>. ~ M. Snoyman (@snoyberg). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/barbara-liskov-is-the-architect-of-modern-algorithms-20191120\/\">Barbara Liskov: The architect of modern algorithms<\/a>. ~ Susan D&#8217;Agostino (@susan_dagostino). #CompSci #Algorithms<\/li>\n<li><a href=\"https:\/\/github.com\/fpvandoorn\/lean-links\">Links to recourses for the Lean Theorem Prover<\/a>. ~ Floris van Doorn. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/github.com\/Gabriel439\/slides\/blob\/master\/simple-twitter\/slides.md\">A bare-bones Twitter clone implemented with Haskell + Nix<\/a>. ~ Gabriel Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/@cdsmithus\/codeworld-import-by-hash-2a9a5d18ece\">CodeWorld import by Hash<\/a>. ~ Chris Smith (@cdsmithus). #CodeWorld #Haskell<\/li>\n<li><a href=\"https:\/\/members.loria.fr\/DLarchey\/files\/papers\/MPC_2019.pdf%20ITP\">Certification of breadth-first algorithms by extraction<\/a>~ D. Larchey-Wendling, R. Matthes. #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.05818\">Verified self-explaining computation<\/a>. ~ J. Stolarek, J. Cheney. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/bobatkey\/CS316-19\">The 2019\/2020 edition of Strathclyde&#8217;s CS316 Functional Programming course<\/a>. ~ Bob Atkey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/scholarworks.umass.edu\/cgi\/viewcontent.cgi?article=2830&amp;context=dissertations_2\">Tools for tutoring theoretical computer science topics<\/a>. ~ Mark McCartin-Lim. #PhD_Thesis #CompSci #Logic #ATP<\/li>\n<li><a href=\"https:\/\/pp.ipd.kit.edu\/uploads\/publikationen\/huisinga19bachelorarbeit.pdf\">Formally verified insertion of reference counting instructions<\/a>. ~ Marc Huisinga. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/github.com\/jozefg\/learn-tt\">A collection of resources for learning type theory and type theory adjacent fields<\/a>. ~ Daniel Gratzer. #TypeTheory #CategoryTheory #ITP #Coq #LeanProver #HoTT<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1911.06899\">Constructing infinitary quotient-inductive types<\/a>. ~ M. Fiore, A.M. Pitts, S.C. Steenkamp. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.10674\">ConCert: A smart contract certification framework in Coq<\/a>. ~ D. Annenkov, J.B. Nielsen, B. Spitters. #ITP #Coq #Blockchain<\/li>\n<li><a href=\"https:\/\/github.com\/AU-COBRA\/ConCert\">ConCert: A framework for smart contract verification in Coq<\/a>. ~ J.B. Nielsen, D. Annenkov. #ITP #Coq #Blockchain<\/li>\n<li><a href=\"http:\/\/eprints.hsr.ch\/798\/1\/FS%202019-BA-EP-Marti-Kamm-The%20Sequent%20Calculus%20Calculator.pdf\">The sequent calculus calculator<\/a>. ~ Matteo Kamm, Mike Marti. #BsC_Thesis #Logic #ITP #Elm #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/seqcalc.io\">Sequent calculus calculator<\/a>. #Logic #ITP<\/li>\n<li><a href=\"https:\/\/csound.com\/icsc2019\/proceedings\/13.pdf\">Kairos: a Haskell library for live coding Csound performances<\/a>. ~ L. Foletto. #Haskell #FunctionalProgramming #Music<\/li>\n<li><a href=\"https:\/\/digitalcommons.lsu.edu\/gradschool_theses\/5037\">Supporting the Algebra I curriculum with an introduction to computational thinking course<\/a>. ~ M.M. Laskowski. #MsC_Thesis #CodeWorld #Haskell #Teaching<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell_Vol11\/raw\/master\/Libro\/Examenes_de_PF_con_Haskell_Vol11.pdf\">Libro de ex\u00e1menes de programaci\u00f3n funcional con Haskell (versi\u00f3n del 25 de noviembre de 2019)<\/a>. #Programaci\u00f3nFuncional #Haskell #I1M2019<\/li>\n<li><a href=\"https:\/\/github.com\/lemastero\/scala_typeclassopedia\">Abstractions and constructions from math, implementations in FP languages and formalizations in proof assistants<\/a>. ~ P. Paradzi\u0144ski. #CategoryTheory<\/li>\n<li><a href=\"https:\/\/steshaw.org\/plt\">PLT: A path to enlightenment in Programming Language Theory<\/a>. ~ Steven Shaw (@steshaw). #Programming #TypeTheory #FunctionalProgramming #CategoryTheory via @pparadzinski<\/li>\n<li><a href=\"https:\/\/www.mpi-sws.org\/~dreyer\/papers\/rustbelt\/paper.pdf\">RustBelt: Securing the foundations of the Rust programming language<\/a>. ~ Ralf Jung et als. #ITP #Coq #Rust<\/li>\n<li><a href=\"https:\/\/briansteffens.github.io\/2017\/02\/20\/from-math-to-machine.html\">From math to machine: translating a function to machine code<\/a>. ~ Brian Steffens (@brian_steffens). #Haskell #Math<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/11\/21\/digging-into-rusts-syntax\">Digging into Rust&#8217;s syntax<\/a>. ~ James Bowen (@james_OWA). #Programming #Rust #Haskell<\/li>\n<li><a href=\"https:\/\/www.47deg.com\/blog\/game-of-life-haskell\">Conway&#8217;s game of life using Haskell and Gloss<\/a>. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming #Gloss<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/categorical-lqr-control-with-linear-relations\">Categorical LQR control with linear relations<\/a>. ~ Philip Zucker (@SandMouth). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/speakerdeck.com\/ajnsit\/supercharged-imperative-programming-with-haskell-and-fp\">Supercharged imperative programming with Haskell and FP<\/a>. ~ Anupam Jain (@ajnsit). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/blog.kleinproject.org\/?p=4440\">The enormous theorem<\/a>. ~ Sarah Spoenemann. #Math<\/li>\n<li><a href=\"https:\/\/notxor.nueva-actitud.org\/blog\/2019\/11\/26\/introduccion-a-emacs\/\">Introducci\u00f3n a la &#8220;Introducci\u00f3n de Emacs&#8221;<\/a>. #Emacs<\/li>\n<li><a href=\"https:\/\/www.research.manchester.ac.uk\/portal\/files\/146395090\/FULL_TEXT.PDF\">Development of group theory in the language of internal set theory<\/a>. ~ Zoltan Kocsis #PhD_Thesis #ITP #Agda #Logic #Math<\/li>\n<li><a href=\"https:\/\/isabelle.in.tum.de\/Isar\/Isar-induct.pdf\">Structured induction proofs in Isabelle\/Isar<\/a>. ~ M. Wenzel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1911.12073\">Property invariant embedding for automated reasoning<\/a>. ~ M. Ol\u0161\u00e1k, C. Kaliszyk, J. Urban. #ATP #MachineLearnig<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/how-to-learn-haskell-in-10-minutes\">How to learn Haskell in 10 minutes a day<\/a>. ~ Yulia Gavrilova. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/astampoulis\/makam\">The Makam metalanguage: a tool for rapid language prototyping<\/a>. ~ Antonis Stampoulis. #Programming #Makam #OCaml<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2019-11-28-pcf-makam-spec\">How to make your papers run: Executable formal semantics for your language<\/a>. ~ Teodoro Freund. #Programming #Makam<\/li>\n<li><a href=\"https:\/\/blog.dropbox.com\/topics\/work-culture\/-the-mind-at-work--guido-van-rossum-on-how-python-makes-thinking\">The Mind at Work: Guido van Rossum on how Python makes thinking in code easier<\/a>. ~ Anthony Wing Kosner. #Programming #Python<\/li>\n<li><a href=\"https:\/\/codesync.global\/media\/revolution-in-computing-education-at-school-opportunity-and-challenge-cmldn19\">The revolution in computing education at school: opportunity and challenge<\/a>. ~ Simon Peyton Jones. #CompSci #Teaching<\/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 noviembre 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\/6918"}],"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=6918"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6918\/revisions"}],"predecessor-version":[{"id":6919,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6918\/revisions\/6919"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6918"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6918"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6918"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}