{"id":7219,"date":"2020-03-01T18:35:41","date_gmt":"2020-03-01T17:35:41","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7219"},"modified":"2020-08-01T18:38:04","modified_gmt":"2020-08-01T16:38:04","slug":"resumen-de-lecturas-compartidas-durante-febrero-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-febrero-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas durante febrero de 2020"},"content":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante febrero de 2020, 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.ps.uni-saarland.de\/Publications\/documents\/ForsterKunze_2019_Certifying-extraction.pdf\">A certifying extraction with time bounds from Coq to call-by-value \u03bb-calculus<\/a>. ~ Yannick Forster, Fabian Kunze. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/Publications\/documents\/ForsterKunzeRoth_2019_wcbv-Reasonable.pdf\">The weak call-by-value \u03bb-calculus is reasonable for both time and space<\/a>. ~ Yannick Forster, Fabian Kunze, Marc Roth. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/Publications\/documents\/ForsterEtAl_2019_VerifiedTMs.pdf\">Verified programming of Turing machines in Coq<\/a>. ~ Yannick Forster, Fabian Kunze, Maximilian Wuttke. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/www.ps.uni-saarland.de\/~smolka\/drafts\/icl2019.pdf\">Computational type theory and interactive theorem proving with Coq (Version of August 2, 2019)<\/a>. ~ Gert Smolka. #eBook #ITP #Coq #Logic<\/li>\n<li><a href=\"https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1571066103000215\/pdf?md5=bcacb89b9fed98564eccf67546b89243&amp;pid=1-s2.0-S1571066103000215-main.pdf\">Towards a readable formalisation of category theory<\/a>. ~ Greg O\u2019Keefe. #ITP #IsabelleHOL #CategoryTheory<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Subset_Boolean_Algebras.html\">A hierarchy of algebras for boolean subsets<\/a>. ~ Walter Guttmann, Bernhard M\u00f6ller. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/mediatum.ub.tum.de\/doc\/1484146\/1484146.pdf\">Formal specification, monitoring, and verification of autonomous vehicles in Isabelle\/HOL<\/a>. ~ Albert Rizaldi. #PhD_Thesis #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/kenta.blogspot.com\/2020\/02\/ozjcrzwx-ulam-spirals.html\">Ulam spirals<\/a>. ~ Ken T Takusagawa. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/en.wikipedia.org\/wiki\/Karp%27s_21_NP-complete_problems\">Karp&#8217;s 21 NP-complete problems<\/a>. #CompSci<\/li>\n<li><a href=\"https:\/\/www.win.tue.nl\/~kbuchin\/teaching\/2IL15\/Slides\/AlgorithmsLecture_9.pdf\">NP-completeness, part I<\/a>. ~ Kevin Buchin. #CompSci<\/li>\n<li><a href=\"https:\/\/www.win.tue.nl\/~kbuchin\/teaching\/2IL15\/Slides\/AlgorithmsLecture_10.pdf\">NP-completeness, part II<\/a>. ~ Kevin Buchin. #CompSci<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/Publications\/documents\/ForsterEtAl_2019_Completeness.pdf\">Completeness theorems for first-order logic analysed in constructive type theory<\/a>. ~ Yannick Forster, Dominik Kirst, Dominik Wehr. #ITP #Coq #Logic<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/Publications\/details\/Larchey-WendlingForster:2019:H10_in_Coq.html\">Hilbert&#8217;s tenth problem in Coq<\/a>. ~ Dominique Larchey-Wendling, Yannick Forster. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.10490\">Beyond notations: Hygienic macro expansion for theorem proving languages<\/a>. ~ Sebastian Ullrich, Leonardo de Moura. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-02457240\/document\">MOIN: A nested sequent theorem prover for intuitionistic modal logics (system description)<\/a>. ~ Marianna Girlando, Lutz Stra\u00dfburger. #ATP #Prolog #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.08983\">A formal development cycle for security engineering in Isabelle<\/a>. ~ Florian Kamm\u00fcller. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.10512\">Automated proof of Bell-LaPadula security properties<\/a>. ~ Maximiliano Cristi\u00e1, Gianfranco Rossi. #ATP #SetLog<\/li>\n<li><a href=\"https:\/\/github.com\/OpenLogicProject\/OpenLogic\/wiki\/Other-Logic-Textbooks\">List of open and free logic textbooks<\/a>. ~ Richard Zach (@RrrichardZach). #Logic<\/li>\n<li><a href=\"https:\/\/chrispenner.ca\/posts\/kaleidoscopes\">Intro to Kaleidoscopes: Optics for aggregating data through Applicatives<\/a>. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2020\/2\/3\/nix-functional-package-management\">Nix: Functional package management!<\/a> ~ James Bowen (@james_OWA). #Nix<\/li>\n<li><a href=\"http:\/\/matryoshka.gforge.inria.fr\/pubs\/satur_report.pdf\">A comprehensive framework for saturation theorem proving (Technical report)<\/a>. ~ Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/ejgallego\/jscoq\">jsCoq: A port of Coq to Javascript (Run Coq in your browser)<\/a>. ~ Emilio Jes\u00fas Gallego Arias (@ejgallego). #ITP #Coq<\/li>\n<li><a href=\"https:\/\/odone.io\/posts\/2020-02-03-monad-composes-sequentially.html\">Why monad composes operations sequentially<\/a>. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/francis.naukas.com\/2020\/02\/03\/los-primos-de-la-conjetura-de-collatz\/\">Los primos de la conjetura de Collatz<\/a>. ~ Francisco R. Villatoro (@emulenews). #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/danaernst.com\/resources\/free-and-open-source-textbooks\/\">Free and open-source textbooks<\/a>. ~ Dana C. Ernst. #eBooks #Math<\/li>\n<li><a href=\"https:\/\/www.johnborwick.com\/2019\/02\/13\/org-mode-website.html\">How I created my website with Org mode<\/a>. ~ John Borwick (@borwick). #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.11142\">VERONICA: Expressive and precise concurrent information flow security (Extended version with technical appendices)<\/a>. ~ Daniel Schoepe, Toby Murray, Andrei Sabelfeld. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/ieeexplore.ieee.org\/stamp\/stamp.jsp?tp=&amp;arnumber=8970457\">A formal system of axiomatic set theory in Coq<\/a>. ~ Tianyu Sun, Wensheng Yu. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/extras\/fol-trakh\/\">Trakhtenbrot\u2019s theorem in Coq (A constructive approach to finite model theory)<\/a>. ~ Dominik Kirst, Dominique Larchey-Wendling. #ITP #Coq #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/aep\/zz\/blob\/master\/README.md\">ZZ (drunk octopus) is a modern formally provable dialect of C, inspired by Rust<\/a>. ~ Arvid E. Picciani. #ZZ #Programming #SMT #FormalVerification<\/li>\n<li><a href=\"https:\/\/slides.com\/dervism\/java-haskell?token=c5PXw4i\">Java &amp; Haskell: Similarities and differences<\/a>. ~ Dervis Mansuroglu (@dervis_m). #Java #Haskell<\/li>\n<li><a href=\"https:\/\/www.cis.upenn.edu\/~cis262\/notes\/proofslambda.pdf\">Proofs, computability, complexity, and the lambda calculus (An introduction)<\/a>. ~ Jean Gallier, Jocelyn Quaintance. #eBook #Logic #CompSci #LambdaCalculus<\/li>\n<li><a href=\"https:\/\/adamsheffer.wordpress.com\/2020\/02\/04\/an-algorithms-course-with-minimal-prerequisites\/\">An algorithms course with minimal prerequisites<\/a>. ~ Adam Sheffer. #Algorithms<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/Christoph_Benzmueller\/publication\/338829452_Computer-supported_Analysis_of_Arguments_in_Climate_Engineering\/links\/5e2d5775a6fdcc70a14bf745\/Computer-supported-Analysis-of-Arguments-in-Climate-Engineering.pdf\">Computer-supported analysis of arguments in climate engineering<\/a>. ~ David Fuenmayor, Christoph Benzm\u00fcller. #ITP #IsabelleHOL.<\/li>\n<li><a href=\"https:\/\/soap.coffee\/~lthms\/posts\/MiniHTTPServer\/\">Implementing and certifying a Web server in Coq<\/a>. ~ Thomas Letan. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/finkel-lang\/finkel%20\">Finkel: Haskell in S-expression<\/a>. #Haskell #Lisp #Finkel_lang<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2020-02-06-safe-inline-java.html\">Safe memory management in inline-java using linear types<\/a>. ~ Facundo Dominguez. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/dDtZLm7HIJs\">Functional or combinator parsing<\/a>. ~ Graham Hutton (@haskellhutt). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/ericphanson.com\/blog\/2019\/learning-algorithmic-techniques-dynamic-programming\/\">Learning algorithmic techniques: dynamic programming<\/a>. ~ Eric P. Hanson. #Algorithms #Programming #JuliaLang<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.11560\">Toward a mechanized compendium of gradual typing<\/a>. ~ Jeremy G. Siek. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1911.00580\">Introduction to univalent foundations of mathematics with Agda<\/a>. ~ Mart\u00edn H\u00f6tzel Escard\u00f3. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/staff.aist.go.jp\/reynald.affeldt\/fipc\/main.pdf\">Formalizing functional analysis structures in dependent type theory<\/a>. ~ Reynald Affeldt et als. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/res.mdpi.com\/d_attachment\/electronics\/electronics-09-00255\/article_deploy\/electronics-09-00255.pdf\">A formal verification framework for security issues of blockchain smart contracts<\/a>. ~ Tianyu Sun, Wensheng Yu. #ITP #Coq #Blockchain<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/lorentz-implementing-smart-contract-edsl-in-haskell\">Lorentz: Implementing smart contract eDSL in Haskell<\/a>. ~ Kostya Ivanov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/thoughtbot.com\/blog\/thinking-in-types\">Thinking in types<\/a>. ~ Pat Brisbin (@patbrisbin). #Haskell #FunctionalProgramming via @lettier<\/li>\n<li><a href=\"https:\/\/medium.com\/heavenlyx\/functional-programming-the-simple-version-63fe10678f6e\">Functional programming: The simple version<\/a>. ~ Muhammad Tabaza (@Tabz_98). #Haskell #FunctionalProgramming via @SWTechDev<\/li>\n<li><a href=\"https:\/\/medium.com\/nmc-techblog\/advanced-functional-programming-concepts-made-easy-2108d227b5ab\">Advanced Functional Programming concepts made easy<\/a>. ~ Tal Joffe (@TalJoffe). #FunctionalProgramming #JavaScript<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2020\/02\/07\/competitive-programming-in-haskell-primes-and-factoring\/\">Competitive Programming in Haskell: primes and factoring<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.cs.vu.nl\/~jhl890\/pub\/hoelzl2013typeclasses.pdf\">Type classes and filters for mathematical analysis in Isabelle\/HOL<\/a>. ~ Johannes H\u00f6lzl, Fabian Immler, Brian Huffman. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2020\/02\/09\/lean-is-better-for-proper-maths-than-all-the-other-theorem-provers\/\">Lean is better for proper maths than all the other theorem provers<\/a>. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2020\/02\/09\/where-is-the-fashionable-mathematics\/\">Where is the fashionable mathematics?<\/a> ~ Kevin Buzzard (@XenaProject). #Math #ITP #LeanProver #Coq #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2002.00423\">An experimental study of formula embeddings for automated theorem proving in first-order logic<\/a>. ~ Ibrahim Abdelaziz et als. #ATP #MachineLearning<\/li>\n<li><a href=\"http:\/\/rg1-teaching.mpi-inf.mpg.de\/autrea-ws19\/script.pdf\">Automated reasoning I<\/a>. ~ Uwe Waldmann. #eBook #ATP #Logic<\/li>\n<li><a href=\"http:\/\/rg1-teaching.mpi-inf.mpg.de\/autrea2-ss18\/script.pdf%20\">Automated reasoning II<\/a>. ~ Sophie Tourret, Uwe Waldmann. #eBook #ATP #Logic<\/li>\n<li><a href=\"https:\/\/www.colibri.udelar.edu.uy\/jspui\/bitstream\/20.500.12008\/23002\/1\/PI%c3%9119.pdf\">Verificaci\u00f3n de estructura de redes neuronales profundas en tiempo de compilaci\u00f3n (Proyecto TensorSafe)<\/a>. ~ Leonardo Pi\u00f1eyro. #Haskell #DeepLearning<\/li>\n<li><a href=\"http:\/\/cleilaclo2018.mackenzie.br\/docs\/SIESC\/182970.pdf\">MateFun: Functional Programming and Math with adolescents<\/a>. ~ Alejandra Carboni et als. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/www.colibri.udelar.edu.uy\/jspui\/bitstream\/20.500.12008\/23006\/1\/VAZ19.pdf\">Mejoras al int\u00e9rprete MateFun<\/a>. ~ Nicol\u00e1s V\u00e1zquez. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/markkarpov.com\/tutorial\/th.html\">Template Haskell tutorial<\/a>. ~ Mark Karpov (@mrkkrp). #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:\/\/chrisdone.com\/posts\/data-typeable\/\">Typeable and Data in Haskell<\/a>. ~ Chris Done (@christopherdone). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Arith_Prog_Rel_Primes.html\">Arithmetic progressions and relative primes<\/a>. ~ Jos\u00e9 Manuel Rodr\u00edguez Caballero. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/wdi.centralesupelec.fr\/boulanger\/Enseignement\/TutoIsabelle\">Tutoriel: types de donn\u00e9es, fonctions et preuves en Isabelle<\/a>. ~ Fr\u00e9d\u00e9ric Boulanger. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/wdi.centralesupelec.fr\/boulanger\/Enseignement\/Niklaus\">Cours: S\u00e9mantique des langages<\/a>. ~ Fr\u00e9d\u00e9ric Boulanger. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/github.com\/pedroabreu0\/pedroabreu0.github.io\/raw\/master\/docs\/POPL20-poster.pdf\">How small can we make a useful type theory?<\/a> ~ Pedro Abreu (@etapedro). #ITP #Coq #Cedille #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/pedrotst\/coquedille\">Coquedille: A Coq to Cedille transpiler written in Coq<\/a>. ~ Pedro Abreu (@etapedro). #ITP #Coq #Cedille #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/two-wrongs.com\/how-laziness-works\">How laziness works<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.sumtypeofway.com\/posts\/introduction-to-recursion-schemes.html\">An introduction to recursion schemes<\/a>. ~ Patrick Thomson. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.functorial.com\/posts\/2015-12-06-Counterexamples.html\">Counterexamples of type classes<\/a>. ~ Phil Freeman. #Haskell #Purescript #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/oleg.fi\/gists\/posts\/2020-02-09-compiling-haskell-to-javascript.html\">Compiling Haskell to JavaScript, not in the way you&#8217;d expect<\/a>. ~ Oleg Grenrus (@phadej). #Haskell #FunctionalProgramming #JavaScript<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2020\/2\/10\/converting-cabal-to-nix\">Converting Cabal to Nix!<\/a> ~ James Bowen (@james_OWA). #Haskell #Cabal #Nix<\/li>\n<li><a href=\"https:\/\/youtu.be\/qhB1Q4v6TEA\">Liquidate your assets (Reasoning about resource usage in Liquid Haskell)<\/a>. ~ Niki Vazou (@nikivazou). #Haskell<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~rjmh\/tfp\/proceedings\/TFP_2020_paper_16.pdf\">State will do<\/a>. ~ Willem Seynaeve, Koen Pauwels and Tom Schrijvers. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~rjmh\/tfp\/proceedings\/TFP_2020_paper_7.pdf\">PaSe: An extensible and inspectable DSL for micro-animations<\/a>. ~ Ruben P. Pieters and Tom Schrijvers. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/physics-history-haskell-interview\">Physics, History and Haskell<\/a>. (Interview with Rinat Stryungis). ~ Denis Oleynikov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~rjmh\/tfp\/proceedings\/TFP_2020_paper_17.pdf\">A DSL for fluorescence microscopy<\/a>. Birthe van den Berg, Peter Dedecker, Tom Schrijvers. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~rjmh\/tfp\/proceedings\/TFP_2020_paper_20.pdf\">A proof assistant based formalisation of core Erlang<\/a>. ~ P\u00e9ter Bereczky, D\u00e1niel Horp\u00e1csi and Simon Thompson. #ITP #Coq #Erlang<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~rjmh\/tfp\/proceedings\/TFP_2020_paper_2.pdf\">An equational modeling of asynchronous concurrent programming<\/a>. ~ David Janin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~rjmh\/tfp\/proceedings\/TFP_2020_paper_9.pdf\">BinderAnn: Automated reification of source annotations for monadic EDSLs<\/a>. ~ Agust\u00edn Mista and Alejandro Russo. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.mdpi.com\/1996-1073\/13\/3\/712\/pdf\">Formalization of cost and utility in Microeconomics<\/a>. ~ Asad Ahmed, Osman Hasan, Falah Awwad, and Nabil Bastaki. #ITP HOL_Light<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/haskell-in-industry-riskbook\">Haskell in production: Riskbook (an interview with Jezen Thomas)<\/a>. ~ Gints Dreimanis. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/andre.tips\/wmh\/generalized-algebraic-data-types-and-data-kinds\/\">Generalized Algebraic Data Types and Data Kinds<\/a>. ~ Andre Popovitch (@PopovitchAndre). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/notxor.nueva-actitud.org\/blog\/2020\/02\/11\/utilizacion-de-registros-en-emacs\/\">Utilizaci\u00f3n de registros en Emacs<\/a>. #Emacs<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~rjmh\/tfp\/proceedings\/TFP_2020_paper_8.pdf\">Generating next step hints for task oriented programs using symbolic execution<\/a>. ~ Nico Naus and Tim Steenvoorden. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/339129400_Mac_Lane%27s_Comparison_Theorem_for_the_Kleisli_Construction_Formalized_in_Coq\">Mac Lane\u2019s comparison theorem for the Kleisli construction formalized in Coq<\/a>. ~ Burak Ekici, and Cezary Kaliszyk. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.cs.cornell.edu\/courses\/cs3110\/2020sp\/textbook\">Functional programming in OCaml<\/a>. ~ Michael R. Clarkson. #eBook #OCaml #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.gigamonkeys.com\/book\/\">Practical Common Lisp<\/a>. ~ Peter Seibel. #eBook #CommonLisp<\/li>\n<li><a href=\"https:\/\/www.slideshare.net\/paulszulc\/maintainable-software-architecture-in-haskell-with-polysemy\">Maintainable software architecture in Haskell (with Polysemy)<\/a>. ~ Pawe\u0142 Szulc (@EncodePanda). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/logiccourse.com\/textbook\/logic-course-adventure\/\">The Logic course adventure (An active learning textbook for formal logic)<\/a>. ~ Ian Schnee. #eBook #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/coq-community\/awesome-coq\">Awesome Coq Awesome (A curated list of awesome Coq libraries, plugins, tools, and resources)<\/a>. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/armkeh.github.io\/blog\/EqualityOfFunctions.html\">Equality of functions in Agda<\/a>. ~ Mark Armstrong. #ITP #Agda #FunctionalProgramming via @armk_eh<\/li>\n<li><a href=\"https:\/\/artagnon.com\/articles\/equality\">Equality in mechanized mathematics<\/a>. ~ Ramkumar Ramachandra. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.fosskers.ca\/blog\/rio-en.html\">Porting to Rio<\/a>. ~ Colin Woodbury (@fosskers). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2020\/02\/15\/competitive-programming-in-haskell-modular-arithmetic-part-1\/\">Competitive programming in Haskell: modular arithmetic, part 1<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/tidsskrift.dk\/brics\/article\/view\/21869\/19296\">There and Back Again (TABA)<\/a>. ~ Olivier Danvy, and Mayer Goldberg. #Programming #Algoritms<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2020-02-15-taba.html\">Typing TABA (There and Back Again)<\/a>. ~ Donnacha Ois\u00edn Kidney (@oisdk). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2001.07488\">Profunctor optics, a categorical update<\/a>. ~ Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregian, Bartosz Milewski, Emily Pillmore, and Mario Rom\u00e1n. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.stackbuilders.com\/tutorials\/python\/using-types-in-python-with-mypy\/\">How to start using Python type annotations with Mypy<\/a>. ~ Carlos Villavicencio. #Python #Mypy<\/li>\n<li><a href=\"http:\/\/logicae.usal.es\/TICTTL\/actas\/JamesCaldwell.pdf\">Teaching natural deduction as a subversive activity<\/a>. ~ James Caldwell. #Logic<\/li>\n<li><a href=\"https:\/\/tel.archives-ouvertes.fr\/tel-01250842v1\/document\">Certifications of programs with computational effects<\/a>. ~ Burak Ekici. #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/cek\/docs\/19\/mfck-tableaux19.pdf\">Certification of nonclausal connection tableaux proofs<\/a>. ~ Michael F\u00e4rber, and Cezary Kaliszyk. #ITP #HOL_Light<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2002.06047\">Flexible coinduction in Agda<\/a>. ~ Luca Ciccone. #MSc_Thesis #ITP #Agda<\/li>\n<li><a href=\"http:\/\/dev.stephendiehl.com\/hask\/\">What I wish I knew when learning Haskell (Version 2<\/a>.5). ~ Stephen Diehl (@smdiehl). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/categorical-combinators-for-graphviz-in-python\/\">Categorical combinators for Graphviz in Python<\/a>. ~ Philip Zucker (@SandMouth). #Python<\/li>\n<li><a href=\"https:\/\/medium.com\/swlh\/how-to-make-mondrian-art-in-haskell-a1a5d430ac32\">How to make mondrian art in Haskell (Unleash your inner functional artist)<\/a>. ~ Marc Fichtel (@mc_razzy). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/josephg.com\/blog\/3-tribes\/\">3 tribes of programming<\/a>. ~ Joseph Gentle (@josephgentle). #Programming<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-02478907\/document\">Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi<\/a>. ~ Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1902.00297\">Signatures and induction principles for higher inductive-inductive types<\/a>. ~ Ambrus Kaposi, and Andr\u00e1s Kov\u00e1cs. #ITP #Agda #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/f.hypotheses.org\/wp-content\/blogs.dir\/4029\/files\/2018\/11\/cardone_slides.pdf\">From Curry to Haskell<\/a>. ~ Felice Cardone. #Haskell #FunctionalProgramming #Logic<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-02477578\/document\">A Why3 proof of GMP algorithms<\/a>. ~ Rapha\u00ebl Rieu-Helft. #Why3 #FormalVerification<\/li>\n<li><a href=\"http:\/\/users.ece.utexas.edu\/~gligoric\/papers\/JainETAL20mCoqTool.pdf\">mCoq: Mutation analysis for Coq verification projects<\/a>. ~ Kush Jain et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/youtu.be\/Og847HVwRSI\">Most popular programming languages 1965-2019<\/a>. #Programming<\/li>\n<li><a href=\"http:\/\/lisp-univ-etc.blogspot.com\/2020\/02\/programming-algorithms-compression.html\">Programming algorithms: Compression<\/a>. ~ Vsevolod Dyomkin. #Algorithms #CommonLisp<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2020-02-19-linear-type-exception.html\">On linear types and exceptions<\/a>. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/leanpub.com\/hy-lisp-python\/read\">A Lisp programmer living in Python-land: The Hy programming language<\/a>. ~ Mark Watson. #eBook #Programing #Lisp #Python #Hy<\/li>\n<li><a href=\"https:\/\/svhol.pbmichel.com\/\">Isabelle\/HOL and Proof General reference [Isabelle\/HOL support wiki<\/a>]. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/whatisrt.github.io\/dependent-types\/2020\/02\/18\/agda-vs-coq-vs-idris.html\">Agda vs. Coq vs. Idris<\/a>. #ITP #Agda #Coq #Idris<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/haskell-type-level-witness\">Type witnesses in Haskell<\/a>. ~ Sandeep Chandrika. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/paperswelove.org\/\">&#8220;Papers we love&#8221; is a repository of academic computer science papers and a community who loves reading them<\/a>. @papers_we_love #CompSci<\/li>\n<li><a href=\"https:\/\/github.com\/papers-we-love\/papers-we-love\">Papers from the computer science community to read and discuss<\/a>. #CompSci<\/li>\n<li><a href=\"https:\/\/dspace.mit.edu\/bitstream\/handle\/1721.1\/5794\/AIM-349.pdf\">Scheme: An interpreter for extended lambda calculus (1975)<\/a>. ~ Gerald J. Sussman, and Guy L. Steele. #Programming #Scheme #CompSci<\/li>\n<li><a href=\"https:\/\/www.aaai.org\/ojs\/index.php\/aimagazine\/article\/view\/1029\">What is a knowledge representation?<\/a>. ~ Randall Davis, Howard Shrobe, and Peter Szolovits (1993). #KR #AI<\/li>\n<li><a href=\"https:\/\/www.cs.cmu.edu\/~crary\/819-f09\/Hoare69.pdf%20\">An axiomatic basis for computer programming<\/a>. ~ C.A.R. Hoare (1969). #CompSci<\/li>\n<li><a href=\"http:\/\/www.mat.uc.cl\/~cmartine\/documents\/WFP.pdf\">Why functional programming matters<\/a>. ~ John Hughes (1989). #FunctionalProgramming #CompSci<\/li>\n<li><a href=\"http:\/\/www.cs.nott.ac.uk\/~pszgmh\/fold.pdf\">A tutorial on the universality and expressiveness of fold<\/a>. ~ Graham Hutton (1999). #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.cs.tufts.edu\/%7Enr\/cs257\/archive\/john-hughes\/quick.pdf\">QuickCheck: \u0391 lightweight tool for random testing of Haskell programs<\/a>. ~ Koen Claessen and John Hughes (2000). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.irif.fr\/~mellies\/mpri\/mpri-ens\/articles\/moggi-computational-lambda-calculus-and-monads.pdf\">Computational lambda-calculus and monads<\/a>. ~ Eugenio Moggi (1988). #CompSci<\/li>\n<li><a href=\"https:\/\/www.cs.bham.ac.uk\/~mhe\/papers\/exhaustive.pdf\">Infinite sets that admit fast exhaustive search<\/a>. ~ Mart\u0131\u0301n Escard\u00f3 (2007). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/repository.upenn.edu\/cgi\/viewcontent.cgi?article=1773&amp;context=cis_papers\">Monoids: Theme and variations (Functional Pearl)<\/a>. ~ Brent A. Yorgey (2012). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cs.um.edu.mt\/~svrg\/FormalMethods\/2012-2013\/QuickCheck.pdf\">QuickCheck testing for fun and profit<\/a>. ~ John Hughes (2007). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.cs.cmu.edu\/afs\/cs\/user\/crary\/www\/819-f09\/Landin64.pdf\">The mechanical evaluation of expressions<\/a>. ~ P.J. Landin (1964). #CompSci<\/li>\n<li><a href=\"https:\/\/londmathsoc.onlinelibrary.wiley.com\/doi\/epdf\/10.1112\/plms\/s2-42.1.230\">On computable numbers, with an application to the Entscheidungsproblem<\/a>. ~ A.M. Turing (1937). #CompSci #Math<\/li>\n<li><a href=\"http:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/propositions-as-types\/propositions-as-types.pdf\">Propositions as types<\/a>. ~ Philip Wadler (2014). #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/www.cs.cmu.edu\/~crary\/819-f09\/McCarthy60.pdf\">Recursive functions of symbolic expressions and their computation by machine, Part I<\/a>. ~ John McCarthy (1960). #CompSci #Lisp<\/li>\n<li><a href=\"http:\/\/www.cs.cmu.edu\/~crary\/819-f09\/Strachey67.pdf\">Fundamental concepts in programming languages<\/a>. ~ Christopher Strachey (2000). #CompSci<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02316859v2\/document\">Graph theory in Coq: Minors, treewidth, and isomorphisms<\/a>. ~ Christian Doczkal and Damien Pous. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02333553v3\/document\">Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq<\/a>. ~ Christian Doczkal, and Damien Pous. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.cs.us.es\/~jalonso\/apuntes\/Pensamientos_de_Machado.html\">Pensamientos de Antonio Machado<\/a>. ~ Guiomar Godoy. #Filosof\u00eda<\/li>\n<li><a href=\"http:\/\/www-sop.inria.fr\/marelle\/personnel\/Laurent.Thery\/math.html\">A selected bibliography on formalised mathematics<\/a>. ~ Laurent Th\u00e9ry. #ITP #Math<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/Publications\/details\/Doczkal:2016:PhDThesis.html\">A machine-checked constructive metatheory of computation tree logic<\/a>. ~ Christian Doczkal (2016). #PhD_Thesis #ITP #Coq #Logic<\/li>\n<li><a href=\"http:\/\/people.rennes.inria.fr\/Assia.Mahboubi\/\/vu.html\">Course: Machine-checked Mathematics<\/a>. ~ Assia Mahboubi. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.research-collection.ethz.ch\/bitstream\/handle\/20.500.11850\/400029\/2\/phdthesis-acreto-online.pdf\">On memory addressing<\/a>. ~ Reto Achermann. #PhD_Thesis #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/kwarc.info\/people\/frabe\/Research\/KR_oafexp_20.pdf\">Experiences from exporting major proof assistant libraries<\/a>. ~ Michael Kohlhase, and Florian Rabe. #ITP #Coq #HOL_Light #IsabelleHOL #Mizar #PVS #MMT<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2002.06047\">Flexible coinduction in Agda<\/a>. ~ Luca Ciccone. #MSc_Thesis #ITP #Agda<\/li>\n<li><a href=\"https:\/\/github.com\/martinescardo\/TypeTopology\/\">Various new theorems in constructive univalent mathematics written in Agda<\/a>. ~ Mart\u00edn Escard\u00f3. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2002.07079\">The Cantor-Schr\u00f6der-Bernstein Theorem for \u221e-groupoids<\/a>. ~ Mart\u0131\u0301n Escard\u00f3. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/github.com\/drdo\/logic-translation\">Translation from FOL to LTL+Past and LTL, via separation of LTL+Past<\/a>. ~ Daniel Oliveira. #Logic #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/drdo\/logic-translation\/raw\/master\/doc\/Thesis.pdf\">Linear temporal logic: separation and translation<\/a>. ~ Daniel Oliveira. #MSc_Thesis #Logic #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/fenix.tecnico.ulisboa.pt\/downloadFile\/563568428791213\/or-????-separation.pdf\">Revisiting separation: Algorithms and complexity<\/a>. ~ Daniel Oliveira, and Jo\u00e3o Rasga. #Logic #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/notxor.nueva-actitud.org\/blog\/2019\/01\/05\/sobre-listas-y-atoms\/\">Sobre listas y atoms<\/a>. #Emacs #Elisp<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2002.09282\">Isabelle\/Spartan: A dependent type theory framework for Isabelle<\/a>. ~ Joshua Chen. #ITP #IsabellleHOL #HoTT<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Goodstein_Lambda.html\">Implementing the Goodstein function in \u03bb-calculus<\/a>. ~ Bertram Felgenhauer. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/blog.poisson.chat\/posts\/2020-02-24-quickcheck-higherorder.html\">Testing higher-order properties with QuickCheck<\/a>. ~ Li-yao Xia (@lysxia). #Haskell #FunctionalProgramming #QuickCheck<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2020-02-20-final-bft.html\">Another breadth-first traversal<\/a>. ~ Donnacha Ois\u00edn Kidney (@oisdk). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/jrjohansson\/scientific-python-lectures\">Lectures on scientific computing with Python<\/a>. ~ Robert Johansson (2017). #Python<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2002.04803\">Machine Learning in Python: Main developments and technology trends in data science, machine learning, and artificial intelligence<\/a>. ~ Sebastian Raschka, Joshua Patterson, Corey Nolet. #MachineLearning #AI #Python<\/li>\n<li><a href=\"https:\/\/youtu.be\/UwYLaGzhDb4\">Category theory as a tool for thought<\/a>. ~ Daniel Beskin. #CategoryTheory #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.chronicle.com\/article\/The-Scientific-Paper-Is\/248045\">The scientific paper is outdated (For the sake of research, their careers, and their mental health, scientists should spend more time developing software)<\/a>. ~ Ryan Abernathey. #<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2002.10212\">A mechanised semantics for HOL with ad-hoc overloading<\/a>. ~ Johannes \u00c5man Pohjola, Arve Gengelbach. #ITP #HOL4<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/VeriComp.html\">A generic framework for verified compilers in Isabelle\/HOL<\/a>. ~ Martin Desharnais. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/essay.utwente.nl\/80680\/1\/Staal_BA_EEMCS.pdf\">An analysis of programming paradigms in high-level synthesis tools<\/a>. ~ Pieter Staal. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/iohk.io\/en\/research\/library\/papers\/marloweimplementing-and-analysing-financial-contracts-on-blockchain\/\">Marlowe: implementing and analysing financial contracts on blockchain<\/a>. ~ Pablo Lamela Seijas et als. #Haskell #ITP #IsabelleHOL #Blockchain #Cardano<\/li>\n<li><a href=\"https:\/\/www.comp.nus.edu.sg\/~hobor\/Publications\/2020\/CertifiedDijkstra.pdf\">A machine-checked C implementation of Dijkstra\u2019s shortest path algorithm<\/a>. ~ Anshuman Mohan, Shengyi Wang, and Aquinas Hobor. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.hindawi.com\/journals\/wcmc\/2020\/7346763\/\">Formal verification of hardware components in critical systems<\/a>. ~ Wilayat Khan et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/new.kwarc.info\/people\/frabe\/Research\/rabe_mmtsys_20.pdf\">MMT: The Meta Meta Tool (system description)<\/a>. ~ Florian Rabe. #ITP #MMT<\/li>\n<li><a href=\"https:\/\/youtu.be\/JboZel47XU0\">Type-based formal verification<\/a>. ~ Alejandro Serrano (@trupill). #Haskell #Verification<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2020-02-26-monad-bayes-3.html\">Probabilistic programming with monad\u2011bayes, Part 3: A bayesian neural network<\/a>. ~ Siddharth Bhat, Simeon Carstens, Matthias Meschede. #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>. ~ Christian Doczka. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/raw.githubusercontent.com\/jonaprieto\/athena\/master\/pubs\/paper\/paper.pdf\">Proof-reconstruction in type theory for propositional logic<\/a>. ~ Jonathan Prieto-Cubides, Andr\u00e9s Sicard-Ram\u00edrez. #ITP #Agda #Metis #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/jonaprieto\/athena\">Athena: a tool that translates Metis ATP proofs to the Agda programming language to check their correctness<\/a>. ~ Jonathan Prieto-Cubides. #Haskell #ITP #Agda #Metis #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/jonaprieto\/agda-prop\">agda-prop: A library for classical propositional logic in Agda<\/a>. ~ Jonathan Prieto-Cubides. #ITP #Agda #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/jonaprieto\/agda-metis\">agda-metis: Metis prover reasoning for propositional logic in Agda<\/a>. ~ Jonathan Prieto-Cubides. #ITP #Agda #Metis<\/li>\n<li><a href=\"https:\/\/github.com\/Alastair-Carr\/Natural-Deduction-Pack\/raw\/master\/Natural%20Deduction%20Pack.pdf\">The natural deduction pack<\/a>. ~ Alastair Carr. #Logic<\/li>\n<li><a href=\"https:\/\/www.ssrg.ece.vt.edu\/papers\/tacas20.pdf\">Highly automated formal proofs over memory usage of assembly code<\/a>. ~ Freek Verbeek et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/bartoszmilewski.com\/2020\/02\/24\/math-is-your-insurance-policy\/\">Math is your insurance policy<\/a>. ~ Bartosz Milewski (@BartoszMilewski). #Programming<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?ThEdu19.1\">Automating the generation of high school geometry proofs using Prolog in an educational context<\/a>. ~ Ludovic Font et als. #Prolog #LogicProgramming #Math<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?ThEdu19.3\">A mobile application for self-guided study of formal reasoning<\/a>. ~ David M. Cerna, Rafael P.D. Kiesel, Alexandra Dzhiganskaya. #Logic #Teaching #Android<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?ThEdu19.4\">Tools in term rewriting for education<\/a>. ~ Sarah Winkler, Aart Middeldorp. #Logic #Teaching<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?ThEdu19.5\">Teaching a formalized logical calculus<\/a>. ~ Asta Halkj\u00e6r From et als. #Logic #Teaching #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/sicp.comp.nus.edu.sg\/\">Structure and interpretation of computer programs \u2014 JavaScript adaptation<\/a>. #eBook #JavaScript #SICP<\/li>\n<li><a href=\"http:\/\/math.chapman.edu\/~jipsen\/structures\/doku.php\/\">Mathematical structures<\/a>. ~ Contributors of math.chapman.edu. #Math<\/li>\n<li><a href=\"https:\/\/rjlipton.wordpress.com\/2020\/02\/28\/reductions-and-jokes\/\">Reductions and jokes<\/a>. ~ R.J. Lipton &amp; K.W. Regan. #CompSci #Math<\/li>\n<li><a href=\"https:\/\/www.math.utah.edu\/~cherk\/mathjokes.html\">Mathematical humor<\/a>. ~ Andrej and Elena Cherkaev. #Math<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante febrero de 2020, 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\/7219"}],"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=7219"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7219\/revisions"}],"predecessor-version":[{"id":7220,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7219\/revisions\/7220"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7219"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7219"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7219"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}