{"id":6729,"date":"2019-05-01T11:25:23","date_gmt":"2019-05-01T09:25:23","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6729"},"modified":"2019-09-01T11:26:39","modified_gmt":"2019-09-01T09:26:39","slug":"resumen-de-lecturas-compartidas-durante-abril-de-2019","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-abril-de-2019\/","title":{"rendered":"Resumen de lecturas compartidas durante abril de 2019"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante abril 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:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?thedu18.1.pdf\">Students\u2019 Proof Assistant (SPA)<\/a>. ~ Anders Schlichtkrull, J\u00f8rgen Villadsen, Andreas Halkj\u00e6r From. #Logic #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?thedu18.3.pdf\">Towards ranking geometric automated theorem provers<\/a>. ~ N. Baeta, P. Quaresma. #ATP #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1803.01466v1\">Learning how to prove: From the Coq proof assistant to textbook style<\/a>. ~ S. B\u00f6hne, C. Kreitz. #Teaching #Logic #ITP #Coq<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/4\/1\/building-a-bigger-world\">Building a bigger World<\/a>. James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/macsphere.mcmaster.ca\/bitstream\/11375\/12315\/1\/fulltext.pdf\">A history of the theory of types<\/a>. ~ J. Collins. #Logic #History<\/li>\n<li><a href=\"https:\/\/sigma.software\/about\/media\/pillars-functional-programming-part-1\">The pillars of functional programming (part 1)<\/a>. N. Mozgovoy. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/chrisdone\/dynamic\">Dynamic typing in Haskell<\/a>. ~ Chris Done. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/EugeneLoy\/coq_jupyter\">Jupyter kernel for Coq<\/a>. ~ Eugene Loy. #ITP #Coq #Jupyter<\/li>\n<li><a href=\"https:\/\/www.logicmatters.net\/2019\/04\/02\/ifl2-chapters-on-propositional-natural-deduction-again\/\">IFL2: Chapters on propositional natural deduction, again<\/a>. ~ Peter Smith. #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1904.00620\">Theorem and algorithm checking for courses on logic and formal methods<\/a>. ~ W. Schreiner. #Logic #RISCAL<\/li>\n<li><a href=\"https:\/\/www.karlin.mff.cuni.cz\/~krajicek\/prf2.pdf\">Proof complexity<\/a>. ~ Jan Krajicek. #Book #Logic<\/li>\n<li><a href=\"https:\/\/lars.hupel.info\/pub\/phd-thesis_hupel.pdf\">Verified code generation from Isabelle\/HOL<\/a>. ~ L. Hupel. #PhD_Thesis #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1711.00113v4\">Proving soundness of extensional normal-form bisimilarities<\/a>. ~ P. Polesiuk, S Lenglet, D. Biernacki. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1904.01677\">Hammering Mizar by learning clause guidance<\/a>. ~ J. Jakub\u016fv, J. Urban. #ITP #Mizar #MachineLearnig<\/li>\n<li><a href=\"http:\/\/garden.irmacs.sfu.ca\/\">The Open Problem Garden: a collection of unsolved problems in mathematics<\/a>. #Math<\/li>\n<li><a href=\"https:\/\/duplode.github.io\/posts\/idempotent-applicatives-parametricity-and-a-puzzle.html\">Idempotent applicatives, parametricity, and a puzzle<\/a>. ~ D. Mlot. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/proving-addition-is-commutative-in-haskell-using-singletons\/\">Proving addition is commutative in Haskell using singletons<\/a>. ~ Philip Zucker. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/idontgetoutmuch.org\/singleday.htm\">Data Science in Haskell: An example using temperature data from Thailand and Myanmar<\/a>. ~ Dominic Steinitz. #Haskell #FunctionalProgramming #DataScience<\/li>\n<li><a href=\"https:\/\/jozefg.bitbucket.io\/posts\/2015-03-24-pcf.html\">A tiny compiler for a typed higher order language<\/a>. ~ Danny Gratzer. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/vaibhavsagar.com\/blog\/2017\/05\/29\/imperative-haskell\/\">Imperative Haskell<\/a>. ~ Vaibhav Sagar. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/leanpub.com\/fpmortals-es\/read\">Programaci\u00f3n funcional para mortales con Scalaz<\/a>. ~ S. Halliday, O. Vargas. #Scalaz #Programaci\u00f3nFuncional<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1904.01557\">Analysing mathematical reasoning abilities of neural models<\/a>. ~ D. Saxton, E. Grefenstette, F. Hill, P. Kohli. #MachineLearnig<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Exercitium2018\/raw\/master\/texto\/Exercitium2018.pdf\">Libro de soluciones de problemas de programaci\u00f3n funcional con Haskell propuestos en Exercitum (versi\u00f3n del 6-abr-19)<\/a>. #Haskell #Exercitium<\/li>\n<li><a href=\"https:\/\/dimjasevic.net\/marko\/2019\/02\/09\/isomorphism-and-embedding\/\">Isomorphism and embedding<\/a>. ~ Marko Dimja\u0161evi\u0107. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/www.dataschool.io\/cloud-services-for-jupyter-notebook\">Six easy ways to run your Jupyter Notebook in the cloud<\/a>. #Jupyter<\/li>\n<li><a href=\"https:\/\/blog.statebox.org\/fun-with-functors-95e4e8d60d87\">Fun with functors<\/a>. ~ Marco Perone. #FunctionalProgramming #CategoryTheory<\/li>\n<li><a href=\"https:\/\/www.cl.cam.ac.uk\/~lp15\/papers\/Notes\/Founds-FP.pdf\">Foundations of functional programming<\/a>. ~ L.C Paulson. #FunctionalProgramming #LambdaCalculus<\/li>\n<li><a href=\"https:\/\/www.cl.cam.ac.uk\/teaching\/1213\/DiscMathII\/DiscMathII.pdf\">Set theory for Computer Science<\/a>. ~ G. Winskel. #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.cl.cam.ac.uk\/teaching\/1819\/DataSci\/notes0.pdf\">Foundations of Data Science<\/a>. ~ D. Wischik. #DataScience<\/li>\n<li><a href=\"https:\/\/www.cl.cam.ac.uk\/teaching\/1819\/Types\/handout.pdf\">Type systems<\/a>. ~ N. Krishnaswami. #TypeTheory<\/li>\n<li><a href=\"https:\/\/chrisdone.com\/posts\/web-engines\">Web engines in Haskell<\/a>. ~ Chris Done. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/chrisdone\/vado\">Vado: A demo web browser engine written in Haskell<\/a>. ~ Chris Done. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/cantors-paradise\/the-nature-of-infinity-and-beyond-a05c146df02c\">The nature of infinity\u200aand beyond (An introduction to Georg Cantor and his transfinite paradise)<\/a>. ~ J\u00f8rgen Veisdal. #Logic #Math<\/li>\n<li><a href=\"https:\/\/medium.com\/cantors-paradise\/the-riemann-hypothesis-explained-fa01c1f75d3f\">The Riemann Hypothesis, explained<\/a>. ~ J\u00f8rgen Veisdal. #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1802.08437\">Abstract completion, formalized<\/a>. ~ N. Hirokawa, A. Middeldorp, C. Sternagel, S. Winkler. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/publications.lib.chalmers.se\/records\/fulltext\/255039\/255039.pdf\">On initial categories with families (Formalization of unityped and simply typed CwFs in Agda)<\/a>. ~ K. Brilakis. #Msc_Thesis #ITP #Agda<\/li>\n<li><a href=\"https:\/\/jashug.github.io\/papers\/ConstructingII.pdf\">Constructing inductive-inductive types in cubical type theory<\/a>. ~ J. Hugunin. #ITP #Agda #Coq<\/li>\n<li><a href=\"https:\/\/medium.com\/@samuel.fare\/what-making-a-cup-of-tea-taught-me-about-functional-programming-a09909679924\">What making a cup of tea taught me about functional programming<\/a>. Sam Fare. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.jstage.jst.go.jp\/article\/kantogakueneconomics\/45\/0\/45_40\/_pdf\">Programming prospect theory in Prolog<\/a>. ~ I. Kenryo. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/4\/8\/generating-more-difficult-mazes\">Generating more difficult mazes!<\/a> ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.techiediaries.com\/julia-data-science-tutorial-dataframe-csv\/\">Julia Data Science Tutorial: Working with DataFrames and CSV<\/a>. #JuliaLang #DataScience<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Binding_Syntax_Theory.html\">A general theory of syntax with bindings in Isabelle\/HOL<\/a>. ~ L. Gheri. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1904.03241\">HOList: An environment for machine learning of higher-order theorem proving (extended version)<\/a>. ~ K. Bansal et als. #ITP #HOL_Light #MachineLearnig<\/li>\n<li><a href=\"https:\/\/blog.monic.co\/a-gentle-introduction-to-symbolic-execution\/\">A gentle introduction to symbolic execution<\/a>. ~ B. Schroeder, J. Burget. #Haskell #SMT<\/li>\n<li><a href=\"https:\/\/blog.stephenwolfram.com\/2018\/11\/logic-explainability-and-the-future-of-understanding\/\">Logic, explainability and the future of understanding<\/a>. ~ S. Wolfram. #Logic<\/li>\n<li><a href=\"https:\/\/blog.jle.im\/entry\/free-alternative-regexp.html\">Applicative regular expressions using the free alternative<\/a>. ~ Justin Le. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cosmius.bitbucket.io\/tkhe\">To kata haskellen evangelion (Learn Haskell the easy way)<\/a>. ~ Cosmia Fu. #eBook #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02086931\/document\">Short proof of Menger&#8217;s Theorem in Coq (Proof Pearl)<\/a>. ~ C. Doczkal. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1904.01677\">Hammering Mizar by learning clause guidance<\/a>. ~ J. Jakub\u016fv, J. Urban. #ATP #Mizar #MachineLearnig<\/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:\/\/jaredcorduan.github.io\/posts\/2019-04-10--rubik-group.html\">The Rubik&#8217;s cube group<\/a>. ~ Jared Corduan. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/dimjasevic.net\/marko\/2019\/04\/08\/become-a-better-haskeller-by-learning-about-inductive-types\/\">Become a better haskeller by learning about inductive types<\/a>. ~ Marko Dimja\u0161evi\u0107. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/hplgit.github.io\/primer.html\/doc\/pub\/half\/book.pdf\">A primer on scientific programming with Python<\/a>. ~ Hans Petter Langtangen. #eBook #Python #Programming<\/li>\n<li><a href=\"https:\/\/www.southampton.ac.uk\/~fangohr\/training\/python\/pdfs\/Python-for-Computational-Science-and-Engineering.pdf\">Introduction to Python for computational science and engineering (A beginner\u2019s guide)<\/a>. ~ Hans Fangohr. #eBook #Python #Programming<\/li>\n<li><a href=\"https:\/\/www.reddit.com\/r\/lisp\/comments\/bc83zt\/lisp_used_to_generate_rhythms_for_a_contemporary\">Lisp used to generate rhythms for a contemporary string trio<\/a>. #Lisp #Programming #Music<\/li>\n<li><a href=\"https:\/\/www.ashwinnarayan.com\/post\/learning-haskell-google-code-jam\/\">Learning Haskell through Google Code Jam<\/a>. ~ Ashwin Narayan. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/@cdsmithus\/new-in-codeworld-share-a-folder-as-a-gallery-bd1b17d36f19\">New in CodeWorld: Share a folder as a gallery<\/a>. ~ Chris Smith. #CodeWorld #Haskell<\/li>\n<li><a href=\"https:\/\/williamyaoh.com\/posts\/2019-04-11-cheatsheet-to-regexes-in-haskell.html\">A cheatsheet to regexes in Haskell<\/a>. ~ William Yao. #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1807.08058\">Learning heuristics for automated reasoning through deep reinforcement learning<\/a>. ~ G. Lederman et als. #ATP #DeepLearning<\/li>\n<li><a href=\"http:\/\/ltvanbinsbergen.nl\/thesis\/thesis.pdf\">Executable formal specification of programming languages with reusable components<\/a>. ~ L.T. van Binsbergen. #PhD_Thesis #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1802.06221\">A new foundational crisis in mathematics, is it really happening?<\/a> ~ M. D\u017eamonja. #Logic #Math #HoTT<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/4\/15\/declaring-victory-and-starting-again\">Declaring victory! (and starting again!)<\/a> ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/@avik.das\/a-graphical-introduction-to-dynamic-programming-2e981fa7ca2?sk=37cd14642cf1a83eb0bb33d231442837\">A graphical introduction to dynamic programming<\/a>. ~ Avik Das. #Algorithms #Programming #Python<\/li>\n<li><a href=\"https:\/\/codingnest.com\/modern-sat-solvers-fast-neat-and-underused-part-3-of-n\">Modern SAT solvers: fast, neat and underused (part 3 of N)<\/a>. ~ M. Ho\u0159e\u0148ovsk\u00fd. #Logic #SAT<\/li>\n<li><a href=\"https:\/\/github.com\/wilfredinni\/python-cheatsheet\">Basic Cheat Sheet for Python (PDF, Markdown and Jupyter Notebook)<\/a>. ~ Carlos Montecinos Geisse. #Python #Programming<\/li>\n<li><a href=\"https:\/\/www.technolush.com\/blog\/evolution-of-programming-languages\">Evolution of programming languages<\/a>. #Programming<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2019-04-17-cubical-probability.html\">Cubical Agda and probability monads<\/a>. ~ Donnacha Ois\u00edn Kidney. #Agda<\/li>\n<li><a href=\"https:\/\/medium.com\/javascript-scene\/can-you-avoid-functional-programming-as-a-policy-7bd0570bcfb2\">Can you avoid functional programming as a policy?<\/a> ~ Eric Elliott. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/shmish111.github.io\/2019\/04\/13\/recursion-schemes-patterns\">Every day recursion schemes<\/a>. ~ David Smith. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/128.84.21.199\/abs\/1904.08468\">Towards evolutionary theorem proving for Isabelle\/HOL<\/a>. ~ Yutaka Nagashima. #ITP #IsabelleHOL #MachineLearning<\/li>\n<li><a href=\"https:\/\/ts.data61.csiro.au\/publications\/nicta_full_text\/8465.pdf\">Eisbach: A proof method language for Isabelle<\/a>. ~ D. Matichuk, T. Murray, M. Wenzel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/ts.data61.csiro.au\/publications\/papers\/Matichuk:phd.pdf\">Automation for proof engineering (Machine-checked proofs at scale)<\/a>. ~ D. Matichuk. #PhD_Thesis #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/www.cogsys.wiai.uni-bamberg.de\/teaching\/ss07\/hs_rc\/slides\/RoGII_lecture_scheele.pdf\">Other classical reasoning methods in Isabelle: From tactics and tacticals to automated reasoning in Isabelle<\/a>. ~ Stephan Scheele. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.theregister.co.uk\/2019\/04\/18\/microsoft_bosque_programming_language\/\">Microsoft debuts Bosque \u2013 a new programming language with no loops, inspired by TypeScript<\/a>. ~ T. Clarbun. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.microsoft.com\/en-us\/research\/uploads\/prod\/2019\/04\/beyond_structured_report_v2.pdf\">Regularized programming with the BOSQUE language (Moving beyond structured programming)<\/a>. ~ Mark Marron. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1812.04088\">Towards machine learning induction<\/a>. ~ Yutaka Nagashima. #ITP #IsabelleHOL #MachineLearning<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/teaching\/ss19\/itp\/content.php\">Course: Interactive theorem proving using Isabelle\/HOL<\/a>. ~ Christian Sternagel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1805.11799\">Automated proof synthesis for propositional logic with deep neural networks<\/a>. ~ Taro Sekiyama, Kohei Suenaga. #ATP #MachineLearning<\/li>\n<li><a href=\"https:\/\/github.com\/data61\/PSL\">PSL: proof strategy language for Isabelle\/HOL<\/a>. ~ Yutaka Nagashima. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/hal.laas.fr\/hal-02088529\/document\">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:\/\/medium.com\/@reinman\/monoids-to-groupoids-492c35105113\">Did Functional Programming get it wrong? (Why do monads feel so clumsy?)<\/a>. ~ reinman. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1904.06750.pdf\">From theory to systems: a grounded approach to programming language education<\/a>. ~ W. Crichton. #Teaching #Programming<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/blogs\/blog-cacm\/236068-soundness-and-completeness-with-precision\/fulltext\">Soundness and completeness: with precision<\/a>. ~ Bertrand Meyer. #CompSci<\/li>\n<li><a href=\"http:\/\/www.comlab.ox.ac.uk\/jeremy.gibbons\/publications\/mr.pdf\">Just do it: Simple monadic equational reasoning<\/a>. ~ Jeremy Gibbons and Ralf Hinze. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fossbytes.com\/microsofts-new-programming-language-bosque-keeps-your-code-simple\">Microsoft\u2019s new programming language \u2018Bosque\u2019 keeps your code simple<\/a>. ~ Manisha Priyadarshini #Programming #Bosque<\/li>\n<li><a href=\"https:\/\/jeremykun.com\/2019\/04\/20\/a-working-mathematicians-guide-to-parsing\">A working mathematician\u2019s guide to parsing<\/a>. ~ Jeremy Kun | Math \u2229 Programming #Programming #LaTeX<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/4\/15\/gxv26jzw4n6989hbajhs2gos9b8utv\">Serializing mazes!<\/a> ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/rjlipton.wordpress.com\/2019\/04\/21\/pnp-proofs\">P=NP proofs<\/a>. ~ R.J. Lipton. #CompSci #Math<\/li>\n<li><a href=\"https:\/\/maex.me\/2019\/04\/rewriting-functions-with-fold-and-reduce\/\">Rewriting functions with fold and reduce<\/a>. ~ Max Str\u00fcbing. #Programming #Haskell #JavaScript<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1904.10414\">The theorem prover museum (Conserving the system heritage of automated reasoning)<\/a>. ~ M. Kohlhase. #ATP #ITP<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2019\/04\/24\/competitive-programming-in-haskell-basic-setup\/\">Competitive programming in Haskell: Basic setup<\/a>. ~ Brent Yorgey. #Haskell<\/li>\n<li><a href=\"https:\/\/thecodeboss.dev\/2018\/06\/declarative-programming-with-prolog-part-1-getting-started\/\">Declarative programming with Prolog<\/a>. ~ Aaron Kraus. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/rjlipton.wordpress.com\/2019\/04\/24\/why-check-a-proof\">Why check a proof?<\/a> ~ R.J. Lipton. #CompSci<\/li>\n<li><a href=\"https:\/\/people.mpi-inf.mpg.de\/~mfleury\/paper\/thesis_draft.pdf\">Formalization of logical calculi in Isabelle\/HOL<\/a>. ~ M. Fleury. #PhD_Thesis #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/people.mpi-inf.mpg.de\/~mfleury\/paper\/optimizing_cdcl.pdf\">A verified SAT solver framework including optimization and partial valuations<\/a>. ~ M. Fleury, C. Weidenbach, D. Zimmer. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/medium.com\/@ben_80237\/continuous-improvement-with-hlint-code-smells-e490886558a1\">Continuous improvement with hlint code smells<\/a>. ~ Ben Weitzman. #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/aymannadeem\/foldilocks\">Demystifying folds with GHCi<\/a>. ~ Ayman Nadeem. #Haskell<\/li>\n<li><a href=\"https:\/\/thoughtbot.com\/blog\/thinking-in-types\">Thinking in types<\/a>. ~ Pat Brisbin. #Haskell<\/li>\n<li><a href=\"https:\/\/typeclasses.com\/learn-haskell\/from-other-languages\">Transitioning to Haskell from other languages<\/a>. ~ @typeclasses #Haskell #Java #JavaScript #Python<\/li>\n<li><a href=\"https:\/\/typeclasses.com\/python\/iterators\">Python iterators<\/a>. ~ @typeclasses #Python #Haskell<\/li>\n<li><a href=\"https:\/\/typeclasses.com\/python\/decorators%20@typeclasses\">Python function decorators<\/a>. #Python #Haskell<\/li>\n<li><a href=\"https:\/\/medium.com\/@patxi\/intro-to-higher-kinded-types-in-haskell-df6b719e7a69\">Intro to Higher Kinded Types in Haskell<\/a>. ~ Patxi Bocos. #Haskell<\/li>\n<li><a href=\"https:\/\/williamyaoh.com\/posts\/2019-04-25-lens-exercises.html\">Exercises for understanding Lenses<\/a>. ~ William Yao. #Haskell<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/4\/29\/compile-driven-development-in-action-refactoring-to-arrays\">Compile driven development in action: refactoring to arrays!<\/a> ~ James Bowen. #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1904.12763v1\">Logic for exact real arithmetic<\/a>. ~ H. Schwichtenberg, F. Wiesnet. #Logic #Mayh #MinLog #Haskell<\/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 abril 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\/6729"}],"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=6729"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6729\/revisions"}],"predecessor-version":[{"id":6731,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6729\/revisions\/6731"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6729"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6729"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6729"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}