{"id":6736,"date":"2019-08-01T11:36:31","date_gmt":"2019-08-01T09:36:31","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6736"},"modified":"2019-09-01T11:37:54","modified_gmt":"2019-09-01T09:37:54","slug":"resumen-de-lecturas-compartidas-durante-julio-de-2019","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-julio-de-2019\/","title":{"rendered":"Resumen de lecturas compartidas durante julio de 2019"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante julio 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:\/\/bit.ly\/2ZZwFJp\">Bar-Hillel theorem mechanization in Coq<\/a>. ~ S. Bozhko, L. Khatbullina, S.Grigorev. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/mybinder.org\/v2\/gh\/jamesdbrock\/learn-you-a-haskell-notebook\/master?urlpath=lab\/tree\/learn_you_a_haskell\/00-preface.ipynb\">Jupyter adaptation of &#8220;Learn you a Haskell for great good!&#8221;<\/a> ~ James Brock. #Haskell #FunctionalProgramming #Jupyter<\/li>\n<li><a href=\"http:\/\/www.cs.nott.ac.uk\/~pszgmh\/fowler.pdf\">Property-based testing<\/a>. ~ J. Fowler. #PhD_Thesis #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/hcommons.org\/deposits\/download\/hc:24984\/CONTENT\/util.pdf\">An introduction to computer science research: selected papers with commentary<\/a>. ~ Camille Akmut. #CompSci<\/li>\n<li><a href=\"http:\/\/www.chargueraud.org\/research\/2019\/cycle_detect\/cycle_detect.pdf\">Formal proof and analysis of an incremental cycle detection algorithm<\/a>. ~ A. Gu\u00e9neau, J.H. Jourdan, A. Chargu\u00e9raud, F. Pottier. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.ssrg.ece.vt.edu\/papers\/safecomp19.pdf\">Formal verification of memory preservation of x86-64 binaries<\/a>. ~ J.A. Bockenek, F. Verbeek, P. Lammich, B. Ravindran. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/7\/1\/gloss-review\">Monday Morning Haskell: Gloss review!<\/a> ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.sigplan.org\/2019\/07\/01\/secure-compilation\">Secure compilation<\/a>. ~ C. Hritcu et als. #Programming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.00205\">The Ramanujan machine: Automatically generated conjectures on fundamental constants<\/a>. ~ G. Raayoni et als. #MachineLearning #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1904.02809\">Proving tree algorithms for succinct data structures<\/a>. ~ R. Affeldt, J. Garrigue, X. Qi, K. Tanaka. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.01449\">Formalizing the solution to the cap set problem<\/a>. ~ S.R. Dahmen, J. H\u00f6lzl, R.Y. Lewis. #ITP #LeanProver<\/li>\n<li><a href=\"http:\/\/www.cs.bham.ac.uk\/~mhe\/agda-new\/index.html\">Various new theorems in constructive univalent mathematics written in Agda<\/a>. ~ Martin Escardo. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1906.11718v1\">On solving word equations using SAT<\/a>. ~ Joel D. Day et als. #ATP #SAT<\/li>\n<li><a href=\"https:\/\/chshersh.github.io\/type-errors\">A story told by type errors<\/a>. ~ Dmitrii Kovanikov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/penkovsky.com\/categories\/10-days-of-grad\">10 days of neural networks in Haskell<\/a>. Bogdan Penkovsky. #Haskell #FunctionalProgramming #NeuralNetworks<\/li>\n<li><a href=\"https:\/\/youtu.be\/Nvw74z8uQVU\">A taste of type theory<\/a>. ~ Bartosz Milewski. #TypeTheory #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.01297\">Neural network verification for the masses (of AI graduates)<\/a>. ~ E. Komendantskaya et als. #AI #Verification #ITP #Coq #ATP #SMT #Z3 #NeuralNetworks<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/MFOTL_Monitor.html\">Formalization of a monitoring algorithm for metric first-order temporal logic<\/a>. ~ J. Schneider, D. Traytel. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/competition.isabelle.systems\/competitions\/contest\/11\/\">Proving for Fun: July 2019<\/a>. #ITP #IsabelleHOL #Coq<\/li>\n<li><a href=\"http:\/\/mat.unb.br\/~ayala\/RiceThFormalization.pdf\">Formalization of Rice&#8217;s theorem over a functional language model<\/a>. ~ T.M.F. Ramos, A.A- Almeida, M. Ayala-Rinc\u00f3n. #ITP #PVS<\/li>\n<li><a href=\"http:\/\/www.cs.nott.ac.uk\/~pszgmh\/improving.pdf\">Improving Haskell<\/a>. ~ M.A.T. Handley, G. Hutton. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2019\/07\/05\/lightweight-invertible-enumerations-in-haskell\/\">Lightweight invertible enumerations in Haskell<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cs.ox.ac.uk\/publications\/publication12590-abstract.html\">Coding with asymmetric numeral systems<\/a>. ~ J. Gibbons. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/kseo.github.io\/posts\/2016-06-01-learn-haskell-to-be-a-better-programmer.html\">Learn Haskell to be a better programmer<\/a>. ~ Kwang Yul Seo. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/engineering.linecorp.com\/en\/blog\/cutting-through-the-smog-making-an-air-quality-bot-with-haskell\/\">Cutting through the smog: making an air quality bot with Haskell<\/a>. ~ A. Moreno. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cs-syd.eu\/posts\/2019-06-28-microsmos\">Microsmos: Writing a simple tree-editor with brick<\/a>. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?TFPIE2018.6\">Examples and results from a BSc-level course on domain specific languages of mathematics<\/a>. ~ P. Jansson, S.H. Einarsd\u00f3ttir, C. Ionescu. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/dspace.library.uu.nl\/bitstream\/handle\/1874\/380853\/thesis.pdf\">Generic diffing and merging of mutually recursive datatypes in Haskell<\/a>. ~ A. van Putten. #Msc_Thesis #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.sigplan.org\/2019\/07\/03\/s-stands-for-shock-the-european-funders-proposal-for-open-access\">S Stands for Shock: The European funders\u2019 proposal for Open Access<\/a>. ~ Jeremy Gibbons.<\/li>\n<li><a href=\"https:\/\/www.cs.princeton.edu\/~appel\/papers\/funspec_sub.pdf\">Abstraction and subsumption in modular verification of C programs<\/a>. ~ A.W. Appel, L. Beringer. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/dataspace.princeton.edu\/jspui\/bitstream\/88435\/dsp010r9676504\/1\/Cao_princeton_0181D_12718.pdf\">Separation-logic-based program verification in Coq<\/a>. ~ Qinxiang Cao. #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2019\/07\/06\/a-computer-generated-proof-that-nobody-understands\/\">A computer-generated proof that nobody understands<\/a>. ~ Kevin Buzzard. #ATP #Math<\/li>\n<li><a href=\"http:\/\/dev.stephendiehl.com\/fun\/\">Write you a Haskell (Building a modern functional compiler from first principles)<\/a>. ~ Stephen Diehl. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/JKTKops\/Write-You-a-Haskell-2\">A continuation of Stephen Diehl&#8217;s &#8220;Write you a Haskell&#8221;<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/334190273_Lemma_Discovery_for_Induction_A_Survey\">Lemma discovery for induction: A survey<\/a>. ~ Moa Johansson. #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.02836\">From LCF to Isabelle\/HOL<\/a>. ~ L.C. Paulson, T. Nipkow, M. Wenzel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.02594\">Domain-specific language to encode induction heuristics<\/a>. ~ Yutaka Nagashima. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/7\/8\/preparing-for-simulation-player-ai\">Preparing for simulation: Player AI<\/a>. ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/odone.io\/posts\/2019-07-08-scripting-in-haskell-and-purescript.html\">Scripting in Haskell and PureScript<\/a>. ~ Riccardo Odone. #Haskell #PureScript<\/li>\n<li><a href=\"https:\/\/essay.utwente.nl\/78694\/\">A formal proof of the termination of Zielonka&#8217;s algorithm for solving parity games<\/a>. ~ R. Abraham. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1711.06542\">Mechanizing Principia Logico-Metaphysica in functional type theory<\/a>. ~ D. Kirchner, C. Benzm\u00fcller, E.N. Zalta. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/colinzwanziger.com\/wp-content\/uploads\/2019\/06\/Mathematics_of_Language_2019.pdf\">Dependently-typed Montague semantics in the proof assistant Agda-flat<\/a>. ~ C. Zwanziger. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/332786587_IO_Logic_in_HOL\">I\/O logic in HOL<\/a>. ~ C. Benzm\u00fcller, A. Farjami, P. Meder, X. Parent. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.04408\">SAT solvers and computer algebra systems: A powerful combination for mathematics<\/a>. ~ C. Bright, I. Kotsireas, V. Ganesh. #SAT #CAS #Math<\/li>\n<li><a href=\"https:\/\/functor.tokyo\/blog\/2019-07-11-announcing-world-peace\">Open Sum Types in Haskell with world-peace<\/a>. ~ Dennis Gosnell (Dennis Gosnell). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dkalemis.wordpress.com\/2014\/03\/22\/trees-as-monads\/\">Trees as monads<\/a>. ~ Dimitrios Kalemis. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/crypto.stanford.edu\/~blynn\/lambda\/\">Lambda calculus<\/a>. ~ Ben Lynn. #LambdaCalculus #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.jair.org\/index.php\/jair\/article\/view\/11524\">REBA: A refinement-based architecture for knowledge representation and reasoning in robotics<\/a>. ~ M. Sridharan, M. Gelfond, S. Zhang, J. Wyatt. #AI #KRR #ASP<\/li>\n<li><a href=\"https:\/\/www.jair.org\/index.php\/jair\/article\/view\/11529\">Dependency learning for QBF<\/a>. ~ T. Peitl, F. Slivovsky, S. Szeider. #AI<\/li>\n<li><a href=\"https:\/\/blog.sigplan.org\/2019\/07\/09\/my-first-fifteen-compilers\/\">My first fifteen compilers<\/a>. ~ Lindsey Kuper. #Programming #Compilers #Nanopass<\/li>\n<li><a href=\"https:\/\/lars.hupel.info\/pub\/isabelle-cakeml.pdf\">A verified compiler from Isabelle\/HOL to CakeML<\/a>. ~ L. Hupel, T. Nipkow. #ITP #Isabelle\/HOL<\/li>\n<li><a href=\"https:\/\/mpickering.github.io\/papers\/multi-stage-programs-in-context.pdf\">Multi stage programming in context<\/a>. ~ M. Pickering, N. Wu, C. Kiss. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mpickering.github.io\/papers\/working-with-source-plugins.pdf\">Working with source plugins<\/a>. ~ M. Pickering, N. Wu, B. N\u00e9meth. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.04065\">Trustworthy graph algorithms<\/a>. ~ M. Abdulaziz, K. Mehlhorn, T. Nipkow. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/minikanren.org\/workshop\/2019\/minikanren19-final5.pdf\">Certified semantics for miniKanren<\/a>. ~ D. Rozplokhas, A. Vyatkin, D. Boulytchev. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-02176456\/document\">(Co) inductive proof systems for compositional proofs in reachability logic<\/a>. ~ V. Rusu, D. Nowak. #ITP #IsabelleHOL #Coq<\/li>\n<li><a href=\"https:\/\/blog.sigplan.org\/2019\/07\/12\/gradual-typing-theory-practice\/\">Gradual typing from theory to practice<\/a>. ~ Sam Tobin-Hochstadt. #Programming<\/li>\n<li><a href=\"http:\/\/essay.utwente.nl\/78785\/1\/VriesDe_BA_EEMCS.pdf\">Walker: Automated assessment of Haskell code using syntax tree analysis<\/a>. ~ R.H. de Vries. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/peerj.com\/articles\/7223\/\">BioShake: a Haskell EDSL for bioinformatics workflows<\/a>. ~ J. Bed\u0151. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/omelkonian.github.io\/data\/publications\/music-grammars.pdf\">Music as language (Putting probabilistic temporal graph grammars to good use)<\/a>. ~ O. Melkonian #Haskell #FunctionalProgramming #Music<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.04134\">A bridge anchored on both sides: Formal deduction in introductory CS, and code proofs in discrete math<\/a>. ~ D.G. Wonnacott, P.M. Osera. #Logic #Math #ITP #Coq #Haskell<\/li>\n<li><a href=\"https:\/\/www.cister.isep.ipp.pt\/docs\/experimental_evaluation_of_formal_software_development_using_dependently_typed_languages\/1534\/view.pdf\">Experimental evaluation of formal software development using dependently typed languages<\/a>. ~ F. Tamasi. #ITP #Coq #Agda<\/li>\n<li><a href=\"https:\/\/treszkai.github.io\/2019\/07\/13\/haskell-eval\">Evaluation of function calls in Haskell<\/a>. ~ Laszlo Treszkai. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/pdfs\/bsc-thesis.pdf\">Automatically and efficiently illustrating polynomial equalities in Agda<\/a>. ~ Donnacha Ois\u00edn Kidney. #Bachelor_Thesis #ITP #Agda<\/li>\n<li><a href=\"https:\/\/medium.com\/@cdsmithus\/building-and-debugging-frp-with-codeworld-and-reflex-a912083e66c1\">Building and debugging FRP with CodeWorld and Reflex<\/a>. ~ Chris Smith. #Haskell #CodeWorld<\/li>\n<li><a href=\"https:\/\/gist.github.com\/javierdaza\/4258b74e2eb7cfd4f55286061b592f37\">El zen de Python: Explicado y con ejemplos<\/a>. ~ Javier Daza. #Programaci\u00f3n #Python<\/li>\n<li><a href=\"https:\/\/medium.com\/@Pythonidaer\/a-brief-analysis-of-the-zen-of-python-2bfd3b76edbf\">A brief analysis of \u201cThe zen of Python\u201d<\/a>. ~ Jonathan Hammond #Programming #Python<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3322004\">Genetic algorithms as shrinkers in property-based testing<\/a>. ~ F.Y. Lo, C.H. Chen, Y. Chen. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/10816\/pdf\/LIPIcs-ECOOP-2019-24.pdf\">Julia&#8217;s efficient algorithm for subtyping unions and covariant tuples<\/a>. ~ B Chung, F. Zappa Nardelli, J. Vitek. #ITP #Coq #JuliaLang<\/li>\n<li><a href=\"https:\/\/www.cs.princeton.edu\/~appel\/papers\/safe-closure.pdf\">Closure conversion is safe for space<\/a>. ~ Z. Paraskevopoulou, A.W. Appel. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/7\/15\/advanced-search-with-drilling\">Advanced search with drilling!<\/a> ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/write.as\/dani\/writing-a-phd-thesis-with-org-mode\">Writing a PhD thesis with Org Mode<\/a>. ~ Daniel Gomez. #Emacs #Org_mode<\/li>\n<li><a href=\"https:\/\/github.com\/dangom\/org-thesis\">Writing a Ph.D. thesis with Org Mode (emplate repository)<\/a>. ~ Daniel Gomez. #Emacs #Org_mode<\/li>\n<li><a href=\"http:\/\/joostkremers.github.io\/ebib\">ebib: A BibTeX database manager for Emacs<\/a>. #Emacs #LaTeX<\/li>\n<li><a href=\"https:\/\/rjlipton.wordpress.com\/2019\/07\/16\/summer-reading-in-theory\/\">Summer reading in theory<\/a>. R.J. Lipton, K.W. Regan. #CompSci<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2019-07-17-codestatistics.html\">Revelations from repetition: Source code headers in Haskell and Python<\/a>. ~ S. Carstens, M. Meschede. #Haskell #Python<\/li>\n<li><a href=\"https:\/\/www.gaussianos.com\/una-interesante-introduccion-a-la-logica-difusa\">Una interesante introducci\u00f3n a la l\u00f3gica difusa<\/a>. ~ Carlos Bejines. #L\u00f3gica #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/FOL_Seq_Calc1.html\">A sequent calculus for first-order logic in Isabelle\/HOL<\/a>. ~ Andreas Halkj\u00e6r From. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.07885\">Formal verification of trading in financial markets<\/a>. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/ro-che.info\/articles\/2019-07-19-decompose-contt\">Decompose ContT<\/a>. ~ Roman Cheplyaka. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/dimensions-haskell-singletons\">Dimensions and Haskell: Singletons in action<\/a>. ~ R. Stryungis, D. Rogozin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/towardsdatascience.com\/elements-of-functional-programming-in-python-1b295ea5bbe0\">Elements of functional programming in Python<\/a>. ~ Parul Pandey. #Python #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/eprints.whiterose.ac.uk\/148557\/1\/UTP2019.pdf\">Hybrid relations in Isabelle\/UTP<\/a>. ~ S.D. Foster. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/lcs.ios.ac.cn\/~znj\/papers\/CAV2019b.pdf\">Formal verification of quantum algorithms using quantum Hoare logic<\/a>. ~ J. Liu et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.05523\">Towards a verified model of the Algorand consensus protocol in Coq<\/a>. ~ M.A. Alturki, J. Chen, V. Luchangco, B. Moore. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/www.mat.unb.br\/ayala\/C_NominalUnif_PVS.pdf\">A certified functional nominal C-unification<\/a>. ~ M. Ayala-Rinc\u00f3n et als. #ITP #PVS<\/li>\n<li><a href=\"http:\/\/www.staff.science.uu.nl\/~swier004\/publications\/2019-icfp-tim.pdf\">A predicate transformer semantics for effects (Functional pearl)<\/a>. ~ W. Swierstra, T. Baanen. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/richarde.dev\/papers\/2019\/kind-inference\/kind-inference.pdf\">Kind inference for datatypes<\/a>. ~ N. Xie, R.A. Eisenberg, B.C.D.S. Oliveira. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.staff.science.uu.nl\/~swier004\/publications\/2019-tyde-cas.pdf\">Generic enumerators<\/a>. ~ C. van der Rest, W. Swierstra, M. Chakravarty. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.vex.net\/~trebla\/haskell\/IO.xhtml\">Haskell I\/O tutorial<\/a>. ~ Albert Y. C. Lai. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/stackabuse.com\/mathematical-proof-of-algorithm-correctness-and-efficiency\/\">Mathematical proof of algorithm correctness and efficiency<\/a>. ~ Vladimir Bato\u0107anin. #CompSci #Algorithms<\/li>\n<li><a href=\"https:\/\/ro-che.info\/articles\/2019-07-22-associativity-of-fmap\">A curious associativity of the &lt;$&gt; operator<\/a>. ~ Roman Cheplyaka. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/7\/22\/analyzing-our-parameters\">Analyzing our parameters<\/a>. ~ James Bowen #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/kowainik.github.io\/posts\/membrain\">Insane in the Membrain<\/a>. ~ Veronika Romashkina. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/homepage.divms.uiowa.edu\/~astump\/cedille\/lola19.pdf\">Rediscovering constructive type theory with Cedille<\/a>. ~ Aaron Stump. #Haskell #Cedille<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/careers\/238281-making-it-easier-to-program-and-protect-the-web\/fulltext\">Making it easier to program and protect the Web<\/a>. #CompSci<\/li>\n<li><a href=\"http:\/\/lisp-univ-etc.blogspot.com\/2019\/07\/programming-algorithms-book.html\">&#8220;Programming Algorithms&#8221; Book<\/a>. ~ Vsevolod Dyomkin. #Programming #Lisp #Algorithms<\/li>\n<li><a href=\"https:\/\/www.marsja.se\/how-to-use-binder-python-for-reproducible-research\/\">How to use Binder and Python for reproducible research<\/a>. ~ Erik Marsja. #Binder #Docker #Jupyter #Python<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.07794\">Generating correctness proofs with neural networks<\/a>. ~ A. Sanchez-Stern et als. #ITP #NeuralNetworks<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.10674\">Towards a smart contract verification framework in Coq<\/a>. ~ D. Annenkov, B. Spitters. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/dev.to\/riccardoodone\/building-a-blog-in-haskell-with-yesod-using-a-database-41ip\">Building a blog in Haskell with Yesod\u2013using a database<\/a>. ~ R. Odone. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dev.to\/erwald\/euclidean-rhythms-and-haskell-5ecj\">Euclidean rhythms and Haskell<\/a>. ~ Erich Grunewald. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/bollu\/blaze\/blob\/75c4ab5c17bda3b751f0d328b19064a2ce1eccfe\/notebooks\/tutorial.ipynb\">A weekend replication of STOKE, a stochastic superoptimiser<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/hadolint\/hadolint\">Haskell Dockerfile linter: A smarter Dockerfile linter that helps you build best practice Docker images<\/a>. #Docker #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/queuea9.wordpress.com\/2019\/07\/25\/in-praise-of-strong-fp\/\">In praise of strong FP<\/a>. ~ Aaron Stump. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/Bodigrim\/poly\">Fast polynomial arithmetic in Haskell<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.theatlantic.com\/magazine\/archive\/2019\/08\/henry-kissinger-the-metamorphosis-ai\/592771\/\">The AI metamorphosis<\/a>. ~ Henry A. Kissinger, Eric Schmidt, Daniel Huttenlocher. #AI<\/li>\n<li><a href=\"https:\/\/www.lemonde.fr\/blog\/binaire\/2019\/07\/26\/demonstrations-mathematiques-et-programmes-informatiques\/\">Langages des maths, langages de l\u2019informatique<\/a>. #Math #CompSi<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/mathematician-solves-computer-science-conjecture-in-two-pages-20190725\/\">Decades-old computer science conjecture solved in two pages<\/a>. ~ Erica Klarreich. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/www.irif.fr\/~sozeau\/research\/publications\/drafts\/Coq_Coq_Codet.pdf\">Coq Coq Codet! (Towards a Verified Toolchain for Coq in MetaCoq)<\/a>. ~ M. Sozeau et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.degruyter.com\/downloadpdf\/j\/forma.2019.27.issue-2\/forma-2019-0020\/forma-2019-0020.xml\">Formalization of the MRDP theorem in the Mizar system<\/a>. ~ K. P\u0105k. #ITP #Mizar #Math<\/li>\n<li><a href=\"https:\/\/www.degruyter.com\/view\/j\/forma.2019.27.issue-2\/forma-2019-0017\/forma-2019-0017.xml\">Partial correctness of a factorial algorithm<\/a>. ~ A. Jaszczak, A. Korni\u0142owicz. #ITP #Mizar<\/li>\n<li><a href=\"https:\/\/www.degruyter.com\/downloadpdf\/j\/forma.2019.27.issue-2\/forma-2019-0015\/forma-2019-0015.xml\">Natural addition of ordinals<\/a>. ~ S. Koch. #ITP #Mizar #Math<\/li>\n<li><a href=\"https:\/\/cris.vub.be\/files\/46086326\/paper.pdf\">Modular effects in Haskell through effect polymorphism and explicit dictionary applications<\/a>. ~ D. Devriese. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cs.ox.ac.uk\/ACT2019\/preproceedings\/Genovese%20Gryzlov%20Herold%20Knispel%20Perone%20Post%20and%20Videla.pdf\">idris-ct: A library to do category theory in Idris<\/a>. ~ F. Genovese et als.. #Idris #CategoryTheory<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Szpilrajn.html\">Szpilrajn extension theorem in Isabelle\/HOL<\/a>. ~ P. Zeller. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/observablehq.com\/@bryangingechen\/fibonacci-formalized-1-some-sums\">Fibonacci formalized 1: some sums<\/a>. ~ Bryan Gin-ge Chen. #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/www.timphilipwilliams.com\/posts\/2019-07-25-minecraft.html\">Generating castles for Minecraft using Haskell<\/a>. ~ Tim Philip Williams. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cs-syd.eu\/posts\/2019-07-28-cursors-forest\">Cursors, part 6: The forest cursor<\/a>. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/summer.haskell.org\/news\/2019-07-26-testing-bipartiteness.html\">Testing bipartiteness with monad transformers<\/a>. ~ Vasily Alferov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/@cdsmithus\/solving-a-puzzle-in-haskell-8216a683555\">Solving a puzzle in Haskell<\/a>. ~ Chris Smith. #Haskell #FunctionalProgramming #CodeWorld<\/li>\n<li><a href=\"https:\/\/kodimensional.dev\/recordwildcards\">The power of RecordWildCards<\/a>. ~ Dmitrii Kovanikov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/lisp-univ-etc.blogspot.com\/2019\/07\/crash-course-in-lisp.html\">Programming algorithms: A crash course in Lisp<\/a>. ~ Vsevolod Dyomkin. #CommonLisp<\/li>\n<li><a href=\"https:\/\/dspace.library.uu.nl\/bitstream\/handle\/1874\/382131\/thesis.pdf\">Formalizing extended UTxO and BitML calculus in Agda<\/a>. ~ O Melkonian. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1907.11501\">Extensional higher-order paramodulation in Leo-III<\/a>. ~ A. Steen, C. Benzm\u00fcller. #ITP #Leo_III<\/li>\n<li><a href=\"https:\/\/www.manning.com\/books\/functional-programming-in-scala\">Functional programming in Scala<\/a>. ~ P. Chiusano, R. Bjarnason. #eBook #FunctionalProgramming #Scala<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1803.06494\">Attack trees in Isabelle<\/a>. ~ F. Kamm\u00fcller. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/typeclasses.com\/news\/2019-07-phrasebook\">Introducing the Haskell Phrasebook<\/a>. ~ Chris Martin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/typeclasses.com\/phrasebook\">The Haskell Phrasebook<\/a>. ~ Chris Martin, Julie Moronuki. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/bor0.wordpress.com\/2019\/07\/30\/arithmetic-on-algebraic-data-types\/\">Arithmetic on algebraic data types<\/a>. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/www.nature.com\/articles\/d41586-019-02310-3\">Julia: come for the syntax, stay for the speed<\/a>. ~ J.M. Perkel. #Programming #JuliaLang<\/li>\n<li><a href=\"http:\/\/revue.sesamath.net\/spip.php?article1248\">Les algorithmes du nouveau lyc\u00e9e technologique, en Python<\/a>. ~ Alain Busser. #Programming #Python<\/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 julio 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\/6736"}],"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=6736"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6736\/revisions"}],"predecessor-version":[{"id":6738,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6736\/revisions\/6738"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6736"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6736"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6736"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}