{"id":6734,"date":"2019-07-01T11:33:58","date_gmt":"2019-07-01T09:33:58","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6734"},"modified":"2019-09-01T11:34:56","modified_gmt":"2019-09-01T09:34:56","slug":"resumen-de-lecturas-compartidas-durante-junio-de-2019","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-junio-de-2019\/","title":{"rendered":"Resumen de lecturas compartidas durante junio de 2019"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante junio 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=\"https:\/\/www.gaussianos.com\/sheldon-tenia-razon-el-mejor-numero-es-el-73\">Sheldon ten\u00eda raz\u00f3n: el mejor n\u00famero es el 73<\/a>. ~ M.A. Morales. #Matem\u00e1ticas<\/li>\n<li><a href=\"http:\/\/group-mmm.org\/~ayamada\/DJTY2019.pdf\">A verified implementation of the Berlekamp\u2013Zassenhaus factorization algorithm<\/a>. ~ J. Divas\u00f3n et als. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/uilis.unsyiah.ac.id\/oer\/files\/original\/aa4c33bd9eeba8b979b3033a615b60c8.pdf\">First semester in numerical analysis with Julia<\/a>. ~ G. \u00d6kten. #eBook #JuliaLang #Math<\/li>\n<li><a href=\"https:\/\/www.reddit.com\/r\/haskell\/comments\/bwah9q\/why_haskell_why_github_use_haskell_for_their\/\">Why Haskell &#8211; why GitHub use Haskell for their newly released Semantic package<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/KD_Tree.html\">Multidimensional binary search trees in Isabelle\/HOL<\/a>. ~ Martin Rau. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.cs.kent.ac.uk\/people\/staff\/rnsr\/docs\/herbrand-jlc.pdf\">Towards automated reasoning in Herbrand structures<\/a>. ~ L. Cohen, R. Rowe, Y. Zohar. #Logic #ATP<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~mista\/assets\/pdf\/ast19.pdf\">Generating random structurally rich algebraic data type values<\/a>. ~ A. Mista, A. Russo. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/6\/3\/fighting-back\">Monday Morning Haskell: Fighting Back!<\/a> ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/alhassy\/OCamlCheatSheet\">Reference of basic commands to get comfortable with OCaml<\/a>. ~ Musa Al-hassy. #OCaml<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3309508\">Translation from problem to code in seven steps<\/a>. ~ A.D. Hilton, G.M. Lipp, S.H. Rodger. #Teaching #Programming<\/li>\n<li><a href=\"https:\/\/www21.in.tum.de\/~haslbema\/documents\/Haslbeck_Lammich-Refinement_with_Time.pdf\">Refinement with time (Refining the run-time of algorithms in Isabelle\/HOL)<\/a>. ~ M.P.L. Haslbeck, P. Lammich. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-01897468v2\/document\">Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq<\/a>. ~ Enrico Tassi. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/alioth.uwb.edu.pl\/~pakkarol\/articles\/CBCKKP-ITP2019.pdf\">Higher-order Tarski Grothendieck as a foundation for formal proof<\/a>. ~ C. Brown, C. Kaliszyk, K. P\u0105k. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1904.11818\">A certifying extraction with time bounds from Coq to call-by-value \u03bb-calculus<\/a>. ~ Y. Forster, F. Kunze. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/members.loria.fr\/SMerz\/papers\/itp2019.pdf\">Formal proof of Tarjan\u2019s strongly connected components algorithm in Why3, Coq, and Isabelle<\/a>. ~ R. Chen et als. #ITP #Why3 #Coq #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1810.08380\">Formalizing computability theory via partial recursive functions<\/a>. ~ M. Carneiro. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/wickstrom.tech\/programming\/2019\/06\/02\/property-based-testing-in-a-screencast-editor-case-study-3.html\">Property-based testing in a screencast editor, case study 3: Integration testing<\/a>. ~ Oskar Wickstr\u00f6m. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.ploeh.dk\/2019\/06\/03\/either-catamorphism\/\">Either catamorphism<\/a>. Mark Seemann. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/tibbe\/haskell-style-guide\/blob\/master\/haskell-style.md\">Haskell style guide<\/a>. ~ Johan Tibell. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2019-06-04-solving-puzzles-without-your-brain.html\">Solving programming puzzles without using your brain<\/a>. ~ Donnacha Ois\u00edn Kidney. #Python #Math<\/li>\n<li><a href=\"https:\/\/lean-forward.github.io\/e-g\/e-g.pdf\">Formalizing the solution to the cap set problem<\/a>. ~ S. Dahmen, J. H\u00f6lzl, R.Y. Lewis. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-02088293\/document\">Quantitative continuity and computable analysis in Coq<\/a>. ~ F. Steinberg, L. Thery, H. Thies. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/easychair.org\/publications\/preprint_download\/GhvC\">Hilbert meets Isabelle. (Formalisation of the DPRM theorem in Isabelle\/HOL)<\/a>. ~ D. Aryal et als. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/perso.ens-lyon.fr\/florent.brehard\/chebapprox\/TOFILL\">A certificate-based approach to formally verified approximations<\/a>. ~ F. Br\u00e9hard, A. Mahboubi, D. Pous. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.xuanruiqi.com\/assets\/succinct.pdf\">Proving tree algorithms for succinct data structures<\/a>. ~ R. Affeldt, J. Garrigue, X. Qi, K. Tanaka. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/gupea.ub.gu.se\/bitstream\/2077\/60174\/1\/gupea_2077_60174_1.pdf\">Automatic refactoring for Agda<\/a>. ~ K. Wibergh. #Msc_Thesis #ITP #Agda<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3309512\">LP based integration of computing and science education in middle schools<\/a>. ~ Y. Zhang et als. #Teaching #LogicProgramming<\/li>\n<li><a href=\"https:\/\/wiki.ifs.hsr.ch\/SemProgAnTr\/files\/FS19_Waelter_FP-Web-Mobile.pdf\">Functional programming for Web and mobile (A review of the current state of the art)<\/a>. ~ J. W\u00e4lter. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.13706\">A role for dependent types in Haskell (Extended version)<\/a>. ~ S. Weirich et als. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1906.03930\">Formalization of the axiom of choice and its equivalent theorems<\/a>. ~ T. Sun, W. Yu. #ITP #Coq #Logic #Math<\/li>\n<li><a href=\"https:\/\/github.com\/styzystyzy\/Axiomatic_Set_Theory.%20~%20T.%20Sun.\">Formalization of axiomatic set theory in Coq<\/a>. #ITP #Coq #Logic #Math<\/li>\n<li><a href=\"https:\/\/github.com\/styzystyzy\/Axiom_of_Choice\">Formalization of the axiom of choice and its equivalent theorems in Coq<\/a>. ~ T. Sun. #ITP #Coq #Logic #Math<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3329959\">TeIL: a type-safe imperative tensor intermediate language<\/a>. ~ N.A. Rink, J. Castrillon. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02150167\/document\">Rapid prototyping formal systems in MMT: 5 case studies<\/a>. ~ D. M\u00fcller, F. Rabe. #ITP #MMT #Logic<\/li>\n<li><a href=\"https:\/\/digitalcommons.library.umaine.edu\/cgi\/viewcontent.cgi?article=1536&amp;context=honors\">Exploring semantic hierarchies to improve resolution theorem proving on ontologies<\/a>. ~ S. Small. #ATP #Prover9<\/li>\n<li><a href=\"https:\/\/www.cloudseal.io\/blog\/2019-06-07-pure-programs\">Pure programs: Pure functions aren&#8217;t enough<\/a>. ~ Ryan Newton. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/6\/10\/spring-cleaning-parameters-and-savign\">Spring cleaning: Parameters and saving!<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1906.03523\">Inductive logic programming via differentiable deep neural logic networks<\/a>. ~ A. Payani, F. Fekri. #ILP #NeuralNetworks #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1904.08368\">Relay: A high-level IR for Deep Learning<\/a>. ~ J. Roesch et als. #FunctionalProgramming #MachineLearning<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2019\/06\/11\/the-inverse-of-a-bijection\/\">The inverse of a bijection<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/captjakk.com\/posts\/2019-05-12-practical-intro-eff.html\">A practical introduction to freer monads (Eff)<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cs.cornell.edu\/courses\/cs3110\/2019sp\/textbook\">Functional programming in OCaml<\/a>. ~ Michael R. Clarkson. #eBook #FunctionalProgramming #OCaml<\/li>\n<li><a href=\"http:\/\/home.in.tum.de\/~immler\/documents\/immler2018thesis.pdf\">A verified ODE solver and Smale&#8217;s 14th problem<\/a>. ~ F. Immler. #PhD_Thesis #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/home.in.tum.de\/~mansour\/cv-and-website\/papers\/Greens_journal.pdf\">An Isabelle\/HOL formalisation of Green\u2019s theorem<\/a>. ~ M. Abdulaziz, L.C. Paulson. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/home.in.tum.de\/~mansour\/cv-and-website\/papers\/diamBoundingFormalisationJAR.pdf\">Formally verified algorithms for upper-bounding state space diameters<\/a>. ~ M. Abdulaziz, M. Norrish, C. Gretton. #ITP #HOL4<\/li>\n<li><a href=\"http:\/\/home.in.tum.de\/~mansour\/cv-and-website\/papers\/verifiedValidator.pdf\">A formally verified validator for classical planning problems and solutions<\/a>. ~ M. Abdulaziz, P. Lammich. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/isabelle.in.tum.de\/website-Isabelle2011\/dist\/Isabelle2011\/doc\/isar-overview.pdf\">A tutorial introduction to structured Isar proofs<\/a>. ~ T. Nipkow. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/github.com\/stylewarning\/cl-permutation\">Permutations and permutation groups in Common Lisp<\/a>. ~ Robert Smith. #CommonLisp #Math<\/li>\n<li><a href=\"http:\/\/tomasp.net\/academic\/drafts\/cultures\/cultures.pdf\">Cultures of programming (Understanding the history of programming through controversies and technical artifacts)<\/a>. ~ T. Petricek, #Programming<\/li>\n<li><a href=\"http:\/\/philomatica.org\/wp-content\/uploads\/2019\/06\/rodin_kovalyov.pdf\">Truth and justification in knowledge representation<\/a>. ~ A. Rodin, S. Kovalyov. #KR #HoTT<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/IMP2_Binary_Heap.html\">Binary heaps for IMP2 in Isabelle\/HOL<\/a>. ~ S. Griebel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/jamesrwilcox.com\/InductionExercises.html\">Exercises on generalizing the induction hypothesis<\/a>. ~ James Wilcox. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/typeclasses.com\/monoid\">Monoid<\/a>. ~ Chris Martin, Julie Moronuki. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/semantic.org\/post\/empty-and-unit-types\">Empty and unit types<\/a>. ~ Ashley Yakeley. #Haskell #FunctionalProgramming #TypeTheory<\/li>\n<li><a href=\"https:\/\/blog.poisson.chat\/posts\/2019-06-09-free-monads-free-monads.html\">Free monads of free monads<\/a>. ~ Li-yao Xia. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/bawolk\/hsp\">hsp: Haskell command line text stream processor<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2019\/06\/15\/proofs-are-not-programs\/\">Proofs are not programs<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.msoos.org\/2019\/06\/crystalball-sat-solving-data-gathering-and-machine-learning\/\">CrystalBall: SAT solving, data gathering, and machine learning<\/a>. ~ Mate Soos. #SAT #MachineLearning<\/li>\n<li><a href=\"https:\/\/www.cs.mcgill.ca\/~bpientka\/papers\/learn-ocaml-icfp19.pdf\">Teaching the art of functional programming using automated grading (Experience report)<\/a>. ~ A. Hameer, B. Pientka. #Teaching #FunctionalProgramming #OCaml<\/li>\n<li><a href=\"https:\/\/github.com\/teaching-the-art-of-fp\/learn-ocaml\/tree\/teaching-fp\">Learn-OCaml: A Web application for learning OCaml<\/a>. #Teaching #FunctionalProgramming #OCaml<\/li>\n<li><a href=\"https:\/\/www.staff.ncl.ac.uk\/andrey.mokhov\/selective-functors-slides.pdf\">Selective applicative functors<\/a>. ~ Andrey Mokhov. [Slides] #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.hrpub.org\/download\/20190530\/SA3-19613106.pdf\">Composing monads for a musical performance<\/a>. ~ N. Rossiter, M. Heather. #Music #CategoryTheory #Haskell<\/li>\n<li><a href=\"http:\/\/microsoft.com\/en-us\/research\/uploads\/prod\/2019\/03\/ho-haskell-5c8bb4918a4de.pdf\">Higher-order type-level programming in Haskell<\/a>. ~ C. Kiss et als. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.codefornerds.com\/developing-an-intuition-for-reduce-in-javascript-through-haskell-monoids\/\">Developing an intuition for reduce in JavaScript through Haskell: Monoids<\/a>. ~ @codefornerds #JavaScript #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/parsing-typed-edsl\">Parsing typed eDSL<\/a>. ~ George Agapov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/bit.ly\/2IimNnX\">Haskell quick syntax reference<\/a>. ~ S.L. Nita, M. Mihailescu. #eBook #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1906.06251\">Effective problem solving using SAT solvers<\/a>. ~ C. Bright et als. #ATP #SAT<\/li>\n<li><a href=\"http:\/\/talisker.inf.kcl.ac.uk\/cgi-bin\/repos.cgi\/isabelle-cookbook\/raw-file\/tip\/progtutorial.pdf\">The Isabelle cookbook (A gentle tutorial for programming Isabelle\/ML)<\/a>. ~ C. Urban et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/www3.risc.jku.at\/publications\/download\/risc_5929\/Paper.pdf\">Gr\u00f6bner bases and Macaulay matrices in Isabelle\/HOL<\/a>. ~ A. Maletzky. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/www3.risc.jku.at\/publications\/download\/risc_5919\/Paper.pdf\">Formalization of Dub\u00e9&#8217;s degree bounds for Gr\u00f6bner bases in Isabelle\/HOL<\/a>. ~ A. Maletzky. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Groebner_Macaulay.html\">Gr\u00f6bner bases, Macaulay matrices and Dub\u00e9&#8217;s degree bounds in Isabelle\/HOL<\/a>. ~ A. Maletzky. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Nullstellensatz.html\">Hilbert&#8217;s Nullstellensatz in Isabelle\/HOL<\/a>. ~ A. Maletzky. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/digitalcommons.wpi.edu\/mqp-all\/7119\">Formal verification of boolean unification algorithms with Coq<\/a>. ~ D. Richardson et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/EgbertRijke\/HoTT-Intro\">Introduction to homotopy type theory<\/a>. ~ E. Rijke. #HoTT #Logic #math #ITP #Agda<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1611.05990\">Monte Carlo tableau proof search<\/a>. ~ M. F\u00e4rber, C. Kaliszyk, J. Urban. #ATP #Logic #MachineLearning<\/li>\n<li><a href=\"https:\/\/github.com\/adjoint-io\/auth-adt\">Authenticated data structures, generically<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/6\/17\/loading-games-and-changing-colors\">Loading games and changing colors!<\/a> ~ James Bowen #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.javiercasas.com\/articles\/functional-programming-patterns-functional-core-imperative-shell\">Patterns of functional programming: functional core &#8211; imperative shell<\/a>. ~ J. Casas. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/@baseerhk\/a-taste-of-functional-programming-in-kotlin-3b163b5c8101\">A taste of functional programming in Kotlin<\/a>. ~ Baseer Al-Obaidy. #FunctionalProgramming #Kotlin<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/functor-combinatorpedia.html\">The Functor Combinatorpedia<\/a>. ~ Justin Le. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.slideshare.net\/ScottWlaschin\/the-functional-programming-toolkit-ndc-oslo-2019-150648710\">The functional programming toolkit<\/a>. ~ Scott Wlaschin. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.slideshare.net\/ScottWlaschin\/the-power-of-composition\">The power of composition (for beginners in FP)<\/a>. ~ Scott Wlaschin. #FunctionalProgramming #Fsharp<\/li>\n<li><a href=\"https:\/\/www.slideshare.net\/ScottWlaschin\/functional-design-patterns-devternity2018\">Functional design patterns<\/a>. ~ Scott Wlaschin. #FunctionalProgramming #Fsharp<\/li>\n<li><a href=\"https:\/\/levelup.gitconnected.com\/implementing-recursion-with-the-y-combinator-in-any-language-9e83fa369ca\">Implementing recursion with the Y combinator in any language<\/a>. ~ Michele Riva. #LambdaCalculus #JavaScript #Haskell #Java #Racket #Python #C<\/li>\n<li><a href=\"https:\/\/github.com\/CypherpunkArmory\/UserLAnd\">UserLAnd: The easiest way to run a Linux distribution or application on Android<\/a>. #Linux #Android<\/li>\n<li><a href=\"https:\/\/alhassy.github.io\/InteractiveWayToC\/\">An interactive way to C<\/a>. ~ Musa Al-hassy. #Programming #C #Emacs #Org_mode<\/li>\n<li><a href=\"http:\/\/www.howardism.org\/Technical\/Emacs\/eshell-present.html\">Presenting the Eshell<\/a>. ~ Howard Abrams. #Emacs<\/li>\n<li><a href=\"https:\/\/williamyaoh.com\/posts\/2019-05-27-string-interpolation-and-overlapping-instances.html\">String interpolation and overlapping instances<\/a>. ~ William Yao. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/vadosware.io\/post\/countmin-sketch-in-haskell\/\">Count-Min sketch in Haskell<\/a>. ~ Victor Adossi. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/theindigamer\/not-a-blog\/blob\/5ee43179fe4b148bd8c61680112b4e9e048481fc\/opinionated-haskell-guide-2019.md\">An opinionated beginner\u2019s guide to Haskell in mid 2019<\/a>. ~ Varun Gandhi. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/neilmitchell.blogspot.com\/2019\/04\/foldr-under-hood.html\">foldr under the hood<\/a>. ~ Neil Mitchell. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/typeclasses.com\/python\/itertools-zipping\">Transition to Haskell from Python: Zipping<\/a>. ~ Chris Martin, Julie Moronuki. #Python #Haskell<\/li>\n<li><a href=\"http:\/\/www3.risc.jku.at\/publications\/download\/risc_5930\/Paper.pdf\">Theorema-HOL: Classical Higher-Order Logic in Theorema<\/a>. ~ A. Maletzky. #ITP #TheoremaHOL<\/li>\n<li><a href=\"https:\/\/copilot-language.github.io\/copilot_tutorial.pdf\">An introduction to Copilot<\/a>. ~ F. Dedden et als. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1906.06805\">Neural theorem provers do not learn rules without exploration<\/a>. ~ M. de Jong, F. Sha. #ATP #MachineLearning<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Linear_Inequalities.html\">Linear inequalities in Isabelle\/HOL<\/a>. ~ R. Bottesch, A. Reynaud, R. Thiemann. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/medium.com\/@daltonjlundy\/verifying-fold-using-monoids-in-coq-766e9eaa3893\">Verifying fold using Monoids in Coq<\/a>. ~ Dalton Lundy. #ITP #Coq #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/gvolpe.github.io\/blog\/lessons-learned-while-writing-a-haskell-app\/\">Lessons learned while writing a Haskell application<\/a>. ~ G. Volpe. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/adjoint-io\/galois-field#readme\">An efficient implementation of Galois fields<\/a>. ~ Stephen Diehl. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/argumatronic.com\/posts\/2019-06-21-algebra-cheatsheet.html\">A brief guide to a few algebraic structures<\/a>. ~ Julie Moronuki. #Math #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/why-i-as-of-june-22-2019-think-haskell-is-the-best-general-purpose-language-as-of-june-22-2019\/\">Why I (as of June 22 2019) think Haskell is the best general purpose language (as of June 22 2019)<\/a>. ~ Philip Zucker. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/hiphish.github.io\/blog\/2019\/06\/22\/what-is-a-programmable-programming-language\/\">What is a programmable programming language? ~ A<\/a>. Sanchez. #Programming #Lisp<\/li>\n<li><a href=\"https:\/\/mauriciotejada.com\/introduccion-a-la-programacion-en-julia\/\">Introducci\u00f3n a la programaci\u00f3n en Julia<\/a>. ~ Mauricio M. Tejada. #JuliaLang<\/li>\n<li><a href=\"https:\/\/phys.org\/news\/2019-06-mathematical-proof-isnt-intellectual.html\">A mathematical proof isn&#8217;t just an intellectual exercise<\/a>. ~ D. Holland. #Math<\/li>\n<li><a href=\"http:\/\/theconversation.com\/en-busca-de-una-nueva-definicion-para-la-inteligencia-de-las-maquinas-118742\">En busca de una nueva definici\u00f3n para la inteligencia de las m\u00e1quinas<\/a>. ~ Luis Ignacio Hojas Hojas. #IA<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Differential_Game_Logic.html\">Differential game logic in Isabelle\/HOL<\/a>. ~ Andr\u00e9 Platzer. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/6\/24\/taking-a-shortcut\">Taking a shortcut!<\/a> ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/jonathanabennett.github.io\/blog\/2019\/06\/20\/python-and-emacs-pt.-1\/\">Python and Emacs Pt<\/a>. 1. ~ Jonathan Bennett. #Emacs #Python<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1906.08084\">LiFtEr: Language to encode induction heuristics for Isabelle\/HOL<\/a>. ~ Y. Nagashima. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/adam.chlipala.net\/theses\/cshao.pdf\">A framework for specifying and formally verifying application security policies<\/a>. ~ C. Shao. #Msc_Thesis #ITP #Coq<\/li>\n<li><a href=\"http:\/\/mizar.org\/fm\/fm27-2\/field_1.pdf\">On roots of polynomials over F(X)\/&lt;p&gt;<\/a>. ~ C. Schwarzweller. #ITP #Mizar #Math<\/li>\n<li><a href=\"https:\/\/blog.sigplan.org\/2019\/06\/24\/ai-safety-as-a-pl-problem\/\">AI safety as a PL problem<\/a>. ~ Swarat Chaudhuri. #AI #FormalVerification #MachineLearning<\/li>\n<li><a href=\"https:\/\/typeclasses.com\/python\/data-classes\">Transition to Haskell from Python: Data classes<\/a>. ~ Chris Martin , Julie Moronuki. #Python #Haskell<\/li>\n<li><a href=\"https:\/\/reasonablypolymorphic.com\/blog\/typeholes\/index.html\">Implement with types, not your brain!<\/a> #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/dc.sigedep.exactas.uba.ar\/media\/academic\/grade\/thesis\/tesis-gonzalez-final.pdf\">Evaluaci\u00f3n de implementaciones alternativas de colas concurrentes en Haskell<\/a>. ~ T.A: Gonz\u00e1lez. #Haskell<\/li>\n<li><a href=\"http:\/\/www.cs.nott.ac.uk\/~pszgmh\/clairvoyant.pdf\">Call-by-need is clairvoyant call-by-value<\/a>. ~ J. Hackett, G. Hutton. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/alhassy.github.io\/ElispCheatSheet\">Elisp reference sheet (Quick reference to the core language of Emacs)<\/a>. ~ Musa Al-hassy. #Programminf #Lisp #Elisp #Emacs<\/li>\n<li><a href=\"https:\/\/proofcraft.org\/blog\/isabelle-style.html\">Gerwin&#8217;s style guide for Isabelle\/HOL. Part 1: Good proofs<\/a>. ~ Gerwin Klein. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/proofcraft.org\/blog\/isabelle-style-part2.html\">Gerwin&#8217;s style guide for Isabelle\/HOL. Part 2: Good style<\/a>. ~ Gerwin Klein. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/www.cse.unsw.edu.au\/~cs4161\/18s2\/lect.html\">Course: Advanced topics in software verification<\/a>. ~ Gerwin Klein, June Andronick, Christine Rizkallah, Miki Tanaka. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2019-06-27-cpp-considered-harmful.html\">CPP considered harmful<\/a>. ~ Mathieu Boespflug. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/@erights\/the-tragedy-of-the-common-lisp-why-large-languages-explode-4e83096239b9\">The tragedy of the Common Lisp: Why large languages explode<\/a>. ~ Mark Miller. #Programming<\/li>\n<li><a href=\"http:\/\/news.mit.edu\/2019\/toward-artificial-intelligence-that-learns-to-write-code-0614\">Toward artificial intelligence that learns to write code<\/a>. ~ K. Martineau. #Programming #AI #DeepLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1902.06349.pdf\">Learning to infer program sketches<\/a>. ~ M. Nye et als. #Programming #AI #DeepLearning<\/li>\n<li><a href=\"https:\/\/www.tfp2019.org\/resources\/tfp2019-how-to-specify-it.pdf\">How to specify it! (A guide to writing properties of pure functions)<\/a>. ~ John Hughes. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3314221.3314642\">Gen: A general-purpose probabilistic programming system with programmable inference<\/a>. ~ M.F. Cusumano-Towner et als. #AI #JuliaLang<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Priority_Search_Trees.html\">Priority search trees im Isabelle\/HOL<\/a>. ~ P. Lammich, T. Nipkow. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Prim_Dijkstra_Simple.html\">Purely functional, simple, and efficient implementation of Prim and Dijkstra in Isabelle\/HOL<\/a>. ~ P. Lammich, T. Nipkow. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Complete_Non_Orders.html\">Complete non-orders and fixed points in Isabelle\/HOL<\/a>. ~ A. Yamada, and J. Dubut. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/Papers\/method.pdf\">Mathematical method and proof<\/a>. ~ Jeremy Avigad. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/typeclasses.com\/art\/juliaset\">A Julia set generator<\/a>. ~ Chris Martin, Julie Moronuki. #Haskell #FunctionalProgramming<\/li>\n<\/ul>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante junio 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\/6734"}],"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=6734"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6734\/revisions"}],"predecessor-version":[{"id":6735,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6734\/revisions\/6735"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6734"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6734"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6734"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}