{"id":6717,"date":"2018-12-01T10:53:05","date_gmt":"2018-12-01T09:53:05","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6717"},"modified":"2019-09-01T10:56:02","modified_gmt":"2019-09-01T08:56:02","slug":"resumen-de-lecturas-compartidas-durante-noviembre-de-2018","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-noviembre-de-2018\/","title":{"rendered":"Resumen de lecturas compartidas durante noviembre de 2018"},"content":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante noviembre de 2018, en <a href=\"https:\/\/twitter.com\/Jose_A_Alonso\">Twitter<\/a> fundamentalmente sobre programaci\u00f3n funcional y demostraci\u00f3n asistida por ordenador.<\/p>\n<p>Las lecturas est\u00e1n ordenadas seg\u00fan su fecha de publicaci\u00f3n en <a href=\"https:\/\/twitter.com\/Jose_A_Alonso\">Twitter<\/a>.<\/p>\n<p>Al final de cada art\u00edculo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.<\/p>\n<p>Una recopilaci\u00f3n de todas las lecturas compartidas se encuentra en <a href=\"https:\/\/github.com\/jaalonso\/Lecturas_GLC\">GitHub<\/a>.<\/p>\n<p><!--more--><\/p>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-octubre-de-2018\">Resumen de lecturas compartidas durante octubre de 2018<\/a>. #FunctionalProgramming #Haskell #ITP #IsabelleHOL #Coq #Agda<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/GewirthPGCProof.html\">Formalisation and evaluation of Alan Gewirth&#8217;s proof for the principle of generic consistency in Isabelle\/HOL<\/a>. ~ D. Fuenmayo. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"http:\/\/orbilu.uni.lu\/bitstream\/10993\/37013\/1\/IOlogic-farjami.pdf\">I\/O logic in HOL<\/a>. ~ A. Farjami, P. Meder, X. Parent, C. Benzm\u00fcller. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/orbilu.uni.lu\/bitstream\/10993\/37014\/1\/Aqvist-farjami.pdf\">\u00c5qvist\u2019s dyadic deontic logic E in HOL<\/a>. ~ C. Benzm\u00fcller, A. Farjami, X. Parent. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1810.11979\">Formal proofs of Tarjan&#8217;s algorithm in Why3, Coq, and Isabelle<\/a>. ~ R. Chen, C. Cohen, J.J. Levy, S. Merz, L. Thery. #ITP #Why3 #Coq #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1811.00796\">Automated theorem proving in intuitionistic propositional logic by deep reinforcement learning<\/a>. ~ M. Kusumoto, K. Yahata, M. Sakai. #ATP #DeepLearning<\/li>\n<li><a href=\"https:\/\/dev.to\/supermanitu\/haskell-by-example---the-birthday-bar-12m7\">Haskell by example: The birthday bar<\/a>. ~ Jan van Br\u00fcgge #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/pl-rants.net\/posts\/haskell-opt-journey\/\">Haskell: journey from 144 min to 17 min<\/a>. ~ Denis. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/vanemden.wordpress.com\/2018\/10\/29\/history-of-structured-programming\/\">History of &#8220;Structured programming&#8221;<\/a>. ~ Maarten van Emden. #Programming<\/li>\n<li><a href=\"https:\/\/medium.com\/@stites\/hasktorch-v0-0-1-28d9ab270f3f\">Hasktorch: a library for tensors and neural networks in Haskell<\/a>. ~ Sam Stites. #FunctionalProgramming #Haskell #DeepLearning<\/li>\n<li><a href=\"http:\/\/matryoshka.gforge.inria.fr\/pubs\/metathy_paper.pdf\">Formalizing the metatheory of logical calculi and automatic provers in Isabelle\/HOL<\/a>. ~ J.C. Blanchette. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/www.sciencedirect.com\/science\/article\/pii\/S157106611830080X\/pdf?md5=9ea092c87333b6b917921a1ae9f85aa7&amp;pid=1-s2.0-S157106611830080X-main.pdf\">Mechanizing focused linear logic in Coq<\/a>. ~ B. Xavier, C. Olarte, G. Reis, V. Nigam. #ITP #Coq #Logic<\/li>\n<li><a href=\"http:\/\/bit.ly\/2yUuSKK\">Formalization of universal algebra in Agda<\/a>. ~ E. Gunther, A. Gadea, M. Pagano. #ITP #Agda<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~patrikj\/papers\/TypeTheory4ModProg_preprint_2018-05-19.pdf\">Type theory as a framework for modelling and programming<\/a>. ~ C. Ionescu, P. Jansson, N. Botta. #FunctionalProgramming #TypeTheory<\/li>\n<li><a href=\"https:\/\/competition.isabelle.systems\/competitions\">Proving for Fun<\/a>: proving competitions and learning material for Interactive Proof Assistants such as Isabelle. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/vaibhavsagar.com\/blog\/2018\/11\/03\/moving-towards-dialogue\/\">Moving towards dialogue<\/a>. ~ Vaibhav Sagar. #FunctionalProgramming #Haskell #Idris<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2018\/11\/5\/elm-iii-building-a-bridge-adding-effects\">Elm III: adding effects<\/a>. ~ James Bowen. #FunctionalProgramming #Elm<\/li>\n<li><a href=\"http:\/\/bit.ly\/2OrSjja\">Graphics programming in Elm develops Math knowledge &amp; social cohesion<\/a>. ~ J. Zhang et als. #Teaching #Math #FunctionalProgramming #Elm<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-01563373\/document\">A Lisp way to type theory and formal proofs<\/a>. ~ Fr\u00e9d\u00e9ric Peschanski. #ITP #LaTTe #Clojure #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/latte-central\/LaTTe\">LaTTe: a Laboratory for Type Theory experiments (in Clojure)<\/a>. ~ Frederic Peschanski. #ITP #LaTTe #Clojure #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/european-lisp-symposium.org\/static\/proceedings\/2018.pdf\">Proceedings of the 11 th European Lisp Symposium (April 16-17, 2018)<\/a>. #Lisp #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/dailynous.com\/2018\/11\/07\/new-free-open-source-multi-purpose-multi-system-logic-software\/\">Carnap: a new free open-source multi-purpose multi-system logic software<\/a>. ~ Graham Leach-Krouse. #Logic #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/gleachkr\/Carnap\">Carnap: A formal logic framework that runs in the browser<\/a>. ~ Graham Leach-Krouse. #Logic #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/carnap.io\">Carnap.io: A formal logic framework for Haskell<\/a>. ~ Graham Leach-Krouse. #Logic #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dev.to\/supermanitu\/haskell-by-example---utopian-tree-1da2\">Haskell by example: Utopian tree<\/a>. ~ Jan van Br\u00fcgge. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/technocrat.rbind.io\/2018\/11\/07\/r-and-haskell-meant-for-each-other\/\">R and Haskell, meant for each other?<\/a>. ~ Richard Careaga. #Rstats #Haskell<\/li>\n<li><a href=\"https:\/\/tweag.github.io\/HaskellR\/\">HaskellR: Programming R in Haskell<\/a>. #Rstats #Haskell<\/li>\n<li><a href=\"http:\/\/bit.ly\/2RHnl8T\">Why is functional programming gaining traction? Why now?<\/a> ~ Eric Normand. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1811.03176\">SAT-based explicit LTLf satisfiability checking<\/a>. ~ J. Li, K.Y. Rozier, G. Pu, Y. Zhang, M.Y. Vardi. #Logic #SAT #ATP<\/li>\n<li><a href=\"https:\/\/robertwpearce.com\/hakyll-pt-1-setup-and-initial-customization.html\">Hakyll Pt. 1: Setup &amp; initial customization<\/a>. ~ Robert Pearce. #Haskell #Hakyll #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/tech.finn.no\/2018\/10\/18\/haskell-at-finn-no\/\">Haskell at FINN.no<\/a>. ~ Sjur Millidahl. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/2018\/11\/05\/signal-processing\">Signal processing in Haskell<\/a>. ~ Rinat Stryungis. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/qfpl.io\/posts\/waargonaut-the-jsoner\/\">Waargonaut the JSONer<\/a>. ~ Sean Chalmers. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/pcarbonn\/H-Calc\">So, you want to write a DSL interpreter <\/a>\u2026 H-Calc!. #Haskell #DSL #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=3264832\">On the naturalness of proofs<\/a>. ~ V.J. Hellendoorn, P.T. Devanbu, M.A. Alipour. #ITP #HOL_Light #Coq<\/li>\n<li><a href=\"https:\/\/www.logicmatters.net\/2018\/11\/05\/tarski-on-truth-very-briefly\">Tarski on truth: a thumbnail sketch<\/a>. ~ Peter Smith. #Logic<\/li>\n<li><a href=\"https:\/\/kevinlynagh.com\/notes\/shipping-puzzle\/\">Exploring a shipping puzzle<\/a>. ~ Kevin Lynagh. #Clojure #Alloy #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1810.13430\">Exceptionally monadic error handling (Looking at bind and squinting really hard)<\/a>. ~ J. Malakhovski. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/robertylewis.com\/padics\/padics.pdf\">A formal proof of Hensel&#8217;s lemma over the p-adic integers<\/a>. ~ R.Y. Lewis. #ITP #Lean #Math<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2018-11-10-a-very-simple-prime-sieve.html\">A very simple prime sieve in Haskell<\/a>. ~ Donnacha Ois\u00edn Kidney #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/markkarpov.com\/post\/existential-quantification.html\">Existential quantification<\/a>. ~ Mark Karpov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/danieljharvey.github.io\/posts\/2018-11-11-typeclasses-show.html\">Typeclasses: Show<\/a>. ~ Daniel J. Harvey #Haskell<\/li>\n<li><a href=\"https:\/\/omegaup.com\/img\/libropre3.pdf\">Problemas y algoritmos<\/a>. ~ Luis Vargas. #Libro #Algoritmos #Programacion #Cpp<\/li>\n<li><a href=\"http:\/\/pier.guillen.com.mx\/algoritmos.htm\">Algoritmos<\/a>. ~ Pier Paolo Guillen Hernandez. #Algoritmos<\/li>\n<li><a href=\"http:\/\/www.unirioja.es\/cu\/joheras\/papers\/immiia.pdf\">Inform\u00e1tica para las Matem\u00e1ticas, Matem\u00e1ticas para la Inform\u00e1tica, Inform\u00e1tica aplicada<\/a>. ~ J. Aransay et als. #Matematicas #Informatica<\/li>\n<li><a href=\"http:\/\/binaire.blog.lemonde.fr\/2018\/11\/12\/a-la-recherche-du-logiciel-parfait\">\u00c0 la recherche du logiciel parfait<\/a>. ~ Xavier Leroy. #ITP<\/li>\n<li><a href=\"https:\/\/dev.to\/eddroid\/teaching-functional-programming-two-big-picture-approaches-3nli\">Teaching Functional Programming: two big picture approaches<\/a>. ~ Ed Toro. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2018\/11\/12\/elm-iv-navigation\">Elm IV: navigation!<\/a> ~ James Bowen. #FunctionalProgramming #Elm<\/li>\n<li><a href=\"https:\/\/github.com\/jrclogic\/SMCDEL\">SMCDEL: A symbolic model checker for Dynamic Epistemic Logic<\/a>. ~ Malvin Gattinger. #Logic #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/jrclogic\/SMCDEL\/raw\/master\/SMCDEL.pdf\">SMCDEL: an implementation of symbolic model checking for Dynamic Epistemic Logic with Binary Decision Diagrams<\/a>. ~ Malvin Gattinger. #Logic #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/malv.in\/2018\/funcproglog\/\">Course: Functional programming for logicians<\/a>. ~ Malvin Gattinger and Jana Wagemaker. #Logic #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/homepages.cwi.nl\/~jve\/papers\/15\/html\">Davis, Putnam, Logemann, Loveland (DPLL) theorem proving in Haskell<\/a>. ~ Jan van Eijck. #Logic #Haskell #FunctionalProgramming #ATP<\/li>\n<li><a href=\"https:\/\/malv.in\/posts\/2016-11-16-why-io-input-types-are-confusing.html\">Why IO input types are confusing<\/a>. ~ Malvin Gattinger. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cse.iitk.ac.in\/users\/spramod\/papers\/memocode18.pdf\">UCLID5: Integrating modeling, verification, synthesis, and learning<\/a>. ~ S.A. Seshia, P. Subramanyam. #FormalVerification #ITP<\/li>\n<li><a href=\"https:\/\/mathscholar.org\/2018\/09\/simple-proofs-of-great-theorems\">Simple proofs of great theorems<\/a>. #Math<\/li>\n<li><a href=\"https:\/\/mathscholar.org\/2018\/09\/simple-proofs-the-irrationality-of-pi\/\">Simple proofs: The irrationality of pi<\/a>. #Math<\/li>\n<li><a href=\"https:\/\/mathscholar.org\/2018\/09\/simple-proofs-the-fundamental-theorem-of-algebra\/\">Simple proofs: The fundamental theorem of algebra<\/a>. #Math<\/li>\n<li><a href=\"https:\/\/mathscholar.org\/2018\/09\/simple-proofs-the-impossibility-of-trisection\/\">Simple proofs: The impossibility of trisection<\/a>. #Math<\/li>\n<li><a href=\"http:\/\/qfpl.io\/posts\/intro-to-state-machine-testing-2\/\">Introduction to state machine testing: part 2<\/a>. ~ Andrew McMiddlin #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/a-touch-of-topological-quantum-computation-in-haskell-pt-i\">A touch of topological quantum computation in Haskell pt. I<\/a>. ~ Philip Zucker. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1811.05094\">A SAT+CAS approach to finding good matrices: new examples and counterexamples<\/a>. ~ C. Bright et als. #SAT #CAS<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1811.05116v1\">Programs as the language of science<\/a>. ~ G. Pantelis. #CompSci<\/li>\n<li><a href=\"https:\/\/github.com\/jaalonso\/Examenes_de_PF_con_Haskell\/releases\/download\/v10.1\/Examenes_de_PF_con_Haskell.pdf\">Libro de ex\u00e1menes de programaci\u00f3n funcional con Haskell (versi\u00f3n del 14 de noviembre de 2018)<\/a>. #ProgramacionFuncional #Haskell #I1M2018<\/li>\n<li><a href=\"http:\/\/flint.cs.yale.edu\/flint\/publications\/sacc.pdf\">An abstract stack based approach to verified compositional compilation to machine code<\/a>. ~ P. Wilke, Y. Wang, Z. Shao. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/adam.chlipala.net\/papers\/FiatCryptoSP19\/\">Simple high-level code for cryptographic arithmetic (with proofs, without compromises)<\/a>. ~ A. Erbsen, J. Philipoom, J. Gross, R. Sloan, A. Chlipala. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?doid=3243631.3236784\">Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report)<\/a>. ~ J. Breitner, A. Spector-Zabusky, Y. Li, C. Rizkallah, J. Wiegley, S. Weirich. #ITP #Coq #Haskell<\/li>\n<li><a href=\"https:\/\/functor.tokyo\/blog\/2018-11-15-termonad\">Termonad: A terminal emulator configurable in Haskell<\/a>. ~ Dennis Gosnell. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cis.upenn.edu\/~bcpierce\/courses\/670Fall04\/GreatWorksInPL.shtml\">Great works in programming languages<\/a>. ~ Benjamin C. Pierce. #CompSci<\/li>\n<li><a href=\"https:\/\/alternativebit.fr\/posts\/haskell\/ex-hack-alpha\/\">Ex-Hack: a Haskell example-based documentation<\/a>. ~ @ninjatrappeur #Haskell<\/li>\n<li><a href=\"https:\/\/youtu.be\/Xfu-Mt4YDWQ\">GTK+ programming with Haskell<\/a>. ~ Oskar Wickstr\u00f6m. #Haskell<\/li>\n<li><a href=\"https:\/\/octopi.chalmers.se\/2018\/11\/08\/typed-holes\/\">Typed-holes and valid hole fits<\/a>. ~ Matth\u00edas P\u00e1ll Gissurarson. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mpg.is\/papers\/gissurarson2018suggesting.pdf\">Suggesting valid hole fits for typed-holes (experience report)<\/a>. ~ Matth\u00edas P\u00e1ll Gissurarson. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/haskellweekly.news\/issues\/133.html\">Haskell Weekly 133: News from the Haskell community (November 15 2018)<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/sketis.net\/2018\/isabelle-mmt-export-of-isabelle-theories-and-import-as-omdoc-content\">Isabelle\/MMT: export of Isabelle theories and import as OMDoc content<\/a>. ~ Makarius Wenzel. #ITP #IsabelleHOL #MMT<\/li>\n<li><a href=\"http:\/\/www.macs.hw.ac.uk\/~ek19\/pddl-verification.pdf\">Proof-carrying plans<\/a>. ~ C. Schwaab et als. #ITP #Agda IA #Planning<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/Publications\/documents\/ForsterEtAl_2018_On-Synthetic-Undecidability.pdf\">On synthetic undecidability in Coq, with an application to the Entscheidungsproblem<\/a>. ~ Y. Forster, D. Kirst, G. Smolka. #ITP #Coq #Logic<\/li>\n<li><a href=\"https:\/\/members.loria.fr\/DLarchey\/files\/papers\/BFE_CPP19.pdf\">Breadth-first extraction: lessons from a small exercice in algorithm certification<\/a>. ~ D. Larchey-Wendling, R. Matthes. #ITP #Coq #Algorithms<\/li>\n<li><a href=\"https:\/\/members.loria.fr\/DLarchey\/files\/papers\/UNDEC_CPP19.pdf\">Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines<\/a>. ~ Y. Forster, D. Larchey-Wendling. #ITP #Coq #Logic<\/li>\n<li><a href=\"https:\/\/books.google.es\/books?id=jI15DwAAQBAJ&amp;lpg=PP1&amp;hl=es&amp;pg=PP\">Practical Web Development with Haskell (Master the essential skills to build fast and scalable Web applications)<\/a>. ~ Ecky Putrady. #Haskell<\/li>\n<li><a href=\"https:\/\/robertwpearce.com\/hakyll-pt-2-generating-a-sitemap-xml-file.html\">Hakyll Pt. 2: Generating a sitemap XML file<\/a>. ~ Robert Pearce. #Haskell #Hakyll #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/plato.stanford.edu\/entries\/logic-firstorder-emergence\">The emergence of first-order logic<\/a>. ~ William Ewald. #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/pdf\/1405.7615\">Formal verification of control systems properties with theorem proving<\/a>. ~ D. Araiza-Illan, K. Eder, A. Richards. #ITP<\/li>\n<li><a href=\"https:\/\/taylor.fausak.me\/2018\/11\/18\/2018-state-of-haskell-survey-results\">2018 state of Haskell survey results<\/a>. ~ Taylor Fausak. #Haskell<\/li>\n<li><a href=\"https:\/\/itnext.io\/pros-and-cons-of-functional-programming-32cdf527e1c2\">Pros and cons of functional programming<\/a>. ~ Iren Korkishko. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.math3ma.com\/blog\/the-tensor-product-demystified\">The tensor product, demystified<\/a>. ~ Tai-Danae Bradley. #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Matroids.html\">Matroids in Isabelle\/HOL<\/a>. ~ Jonas Keinholz. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1810.05806.pdf\">Human-competitive patches in automatic program repair with Repairnator<\/a>. ~ M. Monperrus et als. #Programming<\/li>\n<li><a href=\"http:\/\/bit.ly\/2Q4jNAD\">Creative Maths Challenge<\/a>. #Math<\/li>\n<li><a href=\"https:\/\/www.johndcook.com\/blog\/2018\/11\/20\/curry-howard-lambek\">Curry-Howard-Lambek correspondence<\/a>. ~ John D. Cook. #CompSci<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2018-11-20-fast-verified-structures.html\">Keeping formal verification in bounds<\/a>. ~ Donnacha Ois\u00edn Kidney. #Haskell #Agda<\/li>\n<li><a href=\"https:\/\/upcommons.upc.edu\/handle\/2117\/113325\">Analysis and solution of a collection of algorithmic problems<\/a>. ~ R.E. L\u00f3pez. #Algorithms #Programming #Cpp<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Generic_Deriving.html\">Deriving generic class instances for datatypes in Isabelle\/HOL<\/a>. ~ Jonas R\u00e4dle, Lars Hupel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/dld.bz\/hftr9\">What is elementary geometry?<\/a> ~ Alfred Tarski #Math #Logic #History<\/li>\n<li><a href=\"https:\/\/github.com\/BartoszMilewski\/Publications\/raw\/master\/Oredev.pdf\">Programming with Math<\/a>. ~ Bartosz Milewski. #Logic #Math #Programming #Haskell<\/li>\n<li><a href=\"https:\/\/www.codementor.io\/harshittyagi\/high-performance-mathematical-paradigms-in-python-pjc5yocqm\">High-performance mathematical paradigms in Python<\/a>. ~ Harshit Tyagi #Python #Math<\/li>\n<li><a href=\"http:\/\/www.ps.uni-saarland.de\/~kirst\/bachelor.php\">Formalised set theory: well-orderings and the axiom of choice<\/a>. ~ Dominik Kirst. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/extras\/types15\/\">Axiomaticl set theory in type theory<\/a>. ~ Gert Smolka. #ITP #Coq #Math<\/li>\n<li><a href=\"http:\/\/irreal.org\/blog\/?p=7632\">Writing a Thesis with Org Mode<\/a>. #Emacs #OrgMode<\/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 G\u00f3mez. #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/write.as\/dani\/an-emacs-library-for-frictionless-blogging\">An Emacs Library for frictionless Blogging<\/a>. ~ Daniel G\u00f3mez. #Emacs #OrgMode<\/li>\n<li><a href=\"http:\/\/bit.ly\/2Qg7nFD\">Producto de Euler y ceros<\/a>. ~ Juan Arias de Reyna. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/courses.ps.uni-saarland.de\/icl_18\/2\/Resources\">Course: Introduction to computational logic<\/a>. ~ Gert Smolka. #ITP #Coq #Logic<\/li>\n<li><a href=\"https:\/\/dimjasevic.net\/marko\/2018\/11\/20\/function-totality-abstraction-tool-in-programming\/\">Function totality: Abstraction tool in programming<\/a>. ~ Marko Dimja\u0161evi\u0107. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/kowainik.github.io\/posts\/2018-11-18-state-pattern-matching\">State monad comes to help sequential pattern matching<\/a>. ~ Dmitrii Kovanikov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1608.02644.pdf\">Holophrasm: a neural automated theorem prover for higher-order logic<\/a>. ~ D. Whalen. #ITP #NeuralNetworks<\/li>\n<li><a href=\"https:\/\/www.cs.kent.ac.uk\/people\/staff\/dat\/miranda\/whyfp90.pdf\">Why functional programming matters<\/a>. ~ J. Hughes. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/sandrolovnicki\/pLam\">pLam: command line interpreter for learning and exploring pure \u03bb-calculus<\/a>. ~ Sandro Lovni\u010dki. #Haskell #LambdaCalculus<\/li>\n<li><a href=\"https:\/\/www.i-programmer.info\/news\/204-challenges\/12323-new-site-for-googles-coding-competitions-.html\">New site for Google&#8217;s coding competitions<\/a>. ~ Sue Gee. #CompetitiveProgramming<\/li>\n<li><a href=\"http:\/\/matt.might.net\/articles\/quick-quickcheck\/\">An introduction to QuickCheck by example: Number theory and Okasaki&#8217;s red-black trees<\/a>. ~ Matt Might. #Haskell #QuickCheck #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/hmemcpy\/milewski-ctfp-pdf\/releases\/download\/v1.1-rc\/category-theory-for-programmers-scala.pdf\">Category theory for programmers. (Scala edition)<\/a>. ~ B. Milewski, I. Tabachnik. #CategoryTheory #Haskell #Scala #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/tech.kinja.com\/haskell-for-scala-developers-1581854668\">Haskell for Scala developers<\/a>. ~ Claire Neveu. #Haskell #Scala #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/john.cs.olemiss.edu\/~hcc\/csci450\/ELIFP\/ExploringLanguages.html\">Exploring languages with interpreters and functional programming<\/a>. ~ H. Conrad Cunningham. #CompSci #Programming #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.wisdomandwonder.com\/article\/10805\/emacsorg-mode-choosing-the-best-writing-and-publishing-software\">(Emacs+Org-Mode) Choosing the best writing and publishing software<\/a>. #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/dev.to\/leandrotk_\/functional-programming-principles-in-javascript-26g7\">Functional programming principles in Javascript<\/a>. ~ @leandrotk_ #FunctionalProgramming #JavaScript<\/li>\n<li><a href=\"http:\/\/blog.poisson.chat\/posts\/2018-11-26-type-surgery.html\">Surgery for data types<\/a>. ~ Xia Li-yao. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/settheory.net\/links\">Directory of links on logic and foundations of mathematics<\/a>. ~ Sylvain Poirier. #Logic #Math<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2018\/10\/15\/getting-started-with-purescript\">Getting started with Purescript!<\/a> ~ James Bowen. #Purescript #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.fpcomplete.com\/blog\/2018\/10\/is-rust-functional\">Is Rust functional?<\/a> ~ M. Snoyman. #Rust #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.fpcomplete.com\/blog\/2018\/11\/haskell-and-rust\">Haskell and Rust<\/a>. ~ Chris Allen. #Haskell #Rust #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/citation.cfm?id=361612\">Computer programming as an art<\/a>. ~ Donald Knuth. #Programming #CompSci<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1811.11093\">Counting polynomial roots in Isabelle\/HOL: A formal proof of the Budan-Fourier theorem<\/a>. ~ W.Li, L.C. Paulson. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Graph_Saturation.html\">Graph saturation in Isabelle\/HOL<\/a>. ~ S.J.C. Joosten. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/www.cis.upenn.edu\/~bcpierce\/papers\/deepweb-overview.pdf\">From C to interaction trees: Specifying, verifying, and testing a networked server<\/a>. ~ N. Koh et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1811.10818\">Experience report on formally verifying parts of OpenJDK&#8217;s API with KeY<\/a>. ~ A. Kn\u00fcppel, T. Th\u00fcm, C. Pardylla, I. Schaefer. #ATP #KeY<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1811.10814\">Lightweight interactive proving inside an automatic program verifier<\/a>. ~ S. Dailler, C. March\u00e9, Y. Moy. #ITP #ATP<\/li>\n<li><a href=\"https:\/\/github.com\/bor0\/gidti\">Gentle introduction to dependent types with Idris<\/a>. ~ Boro Sitnikovski. #Idris #FunctionalProgramming #ITP<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1811.10819\">Isabelle\/jEdit as IDE for domain-specific formal languages and informal text documents<\/a>. ~ M. Wenzel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/www.cs.utexas.edu\/users\/EWD\/ewd06xx\/EWD697.PDF\">Some beautiful arguments using mathematical induction<\/a>. ~ E.W. Dijkstra. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/users.soe.ucsc.edu\/~cschuster\/phd\/phd_thesis.pdf\">Towards live programming environments for statically verified JavaScript<\/a>. ~ C. Schuster. #PhD_Thesis #ITP #LeanProver #JavaScript<\/li>\n<li><a href=\"https:\/\/github.com\/levjj\/esverify-theory\/\">Formalism and proofs for esverify<\/a>. ~ C. Schuster. #IPT #LeanProver #JavaScript<\/li>\n<li><a href=\"https:\/\/esverify.org\">esverify: Program verification for ECMAScript\/JavaScript<\/a>. ~ C. Schuster. #IPT #LeanProver #JavaScript<\/li>\n<li><a href=\"https:\/\/github.com\/hide-kawabata\/traf\">Traf: A proof tree viewer that works with Coq through Proof General<\/a>. ~ Hideyuki Kawabata. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/bitbucket.org\/nadiapolikarpova\/synquid\/\">Synquid: synthesizes programs from refinement types<\/a>. ~ Nadia Polikarpova. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www-kb.is.s.u-tokyo.ac.jp\/~koba\/papers\/aplas18-long.pdf\">Automated synthesis of functional programs with auxiliary functions<\/a>. ~ S. Eguchi, N. Kobayashi, T. Tsukada. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Auto2_HOL.html\">Auto2 prover<\/a>. ~ B. Zhan. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Functional_Ordered_Resolution_Prover.html\">A verified functional implementation of Bachmair and Ganzinger&#8217;s ordered resolution prover<\/a>. ~ A. Schlichtkrull, J.C. Blanchette, D. Traytel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/blockstream.com\/2018\/11\/28\/simplicity-github\">Simplicity: High-assurance smart contracting<\/a>. ~ R. Oconnor, A. Poelstra. #Haskell #Coq #ITP #FunctionalProgramming #Blockchain<\/li>\n<li><a href=\"https:\/\/github.com\/ElementsProject\/simplicity\">Simplicity: a blockchain programming language designed as an alternative to Bitcoin script<\/a>. ~ R. Oconnor. #Haskell #Coq #ITP #FunctionalProgramming #Blockchain<\/li>\n<li><a href=\"https:\/\/youtu.be\/HnOix9TFy1A\">Type-driven program synthesis<\/a>. ~ N. Polikarpova #Haskell #FunctionalProgramming<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante noviembre de 2018, en Twitter fundamentalmente sobre programaci\u00f3n funcional y demostraci\u00f3n asistida por ordenador. Las lecturas est\u00e1n ordenadas seg\u00fan su fecha de publicaci\u00f3n en Twitter. Al final de cada art\u00edculo se encuentran etiquetas relativas a los sistemas que usa o a su contenido. Una recopilaci\u00f3n de&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[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\/6717"}],"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=6717"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6717\/revisions"}],"predecessor-version":[{"id":6718,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6717\/revisions\/6718"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6717"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6717"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6717"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}