{"id":6914,"date":"2019-10-01T06:57:12","date_gmt":"2019-10-01T04:57:12","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6914"},"modified":"2020-01-07T06:59:27","modified_gmt":"2020-01-07T05:59:27","slug":"resumen-de-lecturas-compartidas-durante-septiembre-de-2019","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-septiembre-de-2019\/","title":{"rendered":"Resumen de lecturas compartidas durante septiembre de 2019"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante septiembre 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=\"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-el-curso-2018-19\/\">Resumen de lecturas compartidas durante el curso 2018-19<\/a>. #GLC<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Jacobson_Basic_Algebra.html\">A case study in basic algebra<\/a>. ~ Clemens Ballarin. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/typeslogicscats.gitlab.io\/posts\/functor-applicative-monad.html\">Functor, applicative, and monad<\/a>. ~ TypesLogicsCats #FunctionalProgramming #OCaml #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/mstksg\/emd\">Empirical mode decomposition and Hilbert-Huang transform in pure Haskell<\/a>. ~ Justin Le (@mstk). #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/topology-tool-kit.github.io\/\">TTK: The Topology ToolKit (Topological data analysis and visualization)<\/a>. ~ Julien Tierny (@JulienTierny) et als. #MachineLearning #DataScience #Python<\/li>\n<li><a href=\"https:\/\/github.com\/conal\/talk-2018-deep-learning-rebooted\">A functional reboot for deep learning<\/a>. ~ Conal Elliott (@conal). #MachineLearning #DeepLearning #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/conal.net\/papers\/essence-of-ad\">The simple essence of automatic differentiation<\/a>. ~ Conal Elliott (@conal). #MachineLearning #DeepLearning #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/github.com\/guibou\/PyF\">PyF: Haskell quasiquoter for string formatting<\/a>. ~ Guillaume Bouchard. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/web.cecs.pdx.edu\/~mpj\/pubs\/springschool.html\">Functional programming with overloading and higher-order polymorphism<\/a>. ~ Mark P. Jones. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.well-typed.com\/blog\/2019\/09\/announcing-the-optics-library\/\">Announcing the optics library<\/a>. ~ Adam Gundry. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/odone.io\/posts\/2019-09-02-merging-io-and-either-into-one-monad.html\">Merging IO and Either into one monad<\/a>. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1908.11105\">FunSeqSet: Towards a purely functional data structure for the linearisation case of dynamic trees problem<\/a>. ~ J.C. Saenz-Carrasco. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1908.10926\">Performance analysis of zippers<\/a>. ~ V\u0131\u0301t \u0160efl. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/fm.csl.sri.com\/SSFT15\/Timeline.pages.pdf\">A timeline for logic, \u03bb-calculus, and programming language theory<\/a>. ~ Dana S. Scott #Logic #LambdaCalculus #Programming #ITP #CompSci<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?FROM2019.1.pdf\">Verifying the DPLL algorithm in Dafny<\/a>. ~ C.C. Andrici, \u015e. Ciob\u00e2c\u0103. #Logic #SAT #FormalVerification #Dafny<\/li>\n<li><a href=\"https:\/\/project.inria.fr\/from2019\/files\/2019\/08\/from2019_full.pdf\">(Co)inductive proof systems for compositional proofs in reachability logic<\/a>. ~ V. Rusu, D. Nowak. #ITP #IsabelleHOL #Coq<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/8\/26\/making-a-learning-model\">Making a learning model<\/a>. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/confengine.com\/functional-conf-2018\/proposal\/6774\/high-performance-haskell\">High performance Haskell<\/a>. ~ Harendra Kumar. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/alicja.dev\/zines\/haskell_functors\">Functors and lifting<\/a>. ~ Alicja Raszkowska (@mamrotynka). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/335583243_From_LCF_to_IsabelleHOL\">From LCF to Isabelle\/HOL<\/a>. ~ L. Paulson, T. Nipkow, M. Wenzel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1909.01414\">From type theory to setoids and back<\/a>. ~ Erik Palmgren. #ITP #Agda<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/relational-algebra-with-fancy-types\/\">Relational algebra with fancy types<\/a>. ~ Philip Zucker (@SandMouth). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2019-09-06-why-haskell-is-important.html\">Why Haskell is important<\/a>. ~ Mark Karpov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/people.csail.mit.edu\/asolar\/SynthesisCourse\/TOC.htm\">Introduction to program synthesis<\/a>. ~ Armando Solar-Lezama.<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11081\/pdf\/LIPIcs-ITP-2019-26.pdf\">Ornaments for proof reuse in Coq<\/a>. ~ Talia Ringer et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/imo-grand-challenge.github.io\">IMO (International Mathematical Olympiad) grand challenge<\/a>. #AI #Math #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/github.com\/IMO-grand-challenge\/formal-encoding\">Formal encoding of IMO (International Mathematical Olympiad) problems<\/a>. ~ Daniel Selsam. #AI #Math #ITP #LeanProver<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/Talks\/london.pdf\">Automated reasoning for the working mathematician<\/a>. ~ Jeremy Avigad. #ITP #ATP #Math<\/li>\n<li><a href=\"https:\/\/github.com\/avigad\/arwm\">Automated reasoning for the working mathematician: notes on some experiments with the use of automation in Isabelle<\/a>. ~ Jeremy Avigad. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.hillelwayne.com\/post\/theorem-prover-showdown\">The great theorem prover showdown<\/a>. ~ Hillel (@hillelogram). #ITP<\/li>\n<li><a href=\"https:\/\/github.com\/levjj\/esverify-theory\/\">Formalism and proofs for esverify<\/a>. ~ Christopher Schuster. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/www.maxwell.vrac.puc-rio.br\/35851\/35851.PDF\">Formaliza\u00e7\u00e3o de algoritmos de criptografia em um assistente de provas interativo<\/a>. ~ Guilherme Gomes Felix da Silva. #MSc_Thesis #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/blogs.scientificamerican.com\/cross-check\/okay-maybe-proofs-arent-dying-after-all\">Okay, maybe proofs aren&#8217;t dying after all<\/a>. ~ John Horgan. #Math<\/li>\n<li><a href=\"https:\/\/github.com\/slasser\/vermillion\">LL(1) parser generator verified in Coq<\/a>. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.nowpublishers.com\/article\/Details\/PGL-045\">QED at large: A survey of engineering of formally verified software<\/a>. ~ Talia Ringer et als. #ITP #FormalVerification<\/li>\n<li><a href=\"http:\/\/wwwf.imperial.ac.uk\/~buzzard\/one_off_lectures\/msr.pdf\">The future of mathematics?<\/a> ~ Kevin Buzzard. #Math #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/www.math.u-psud.fr\/~pmassot\/enseignement\/math114\/\">Introduction aux math\u00e9matiques formalis\u00e9es<\/a>. ~ Patrick Massot. #Math #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/100-thms\/docs\/100-theorems.md\">100 theorems for Lean<\/a>. ~ Floris van Doorn. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/web.cs.wpi.edu\/~dd\/unif.pdf\">A Coq formalization of boolean unification<\/a>. ~ Daniel J. Dougherty. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/cpp2017.mpi-sws.org\/Paulson.pdf%20\">Porting HOL Light\u2019s multivariate analysis library: Some lessons<\/a>. ~ Lawrence C. Paulson. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/esb-dev.github.io\/mat\/nsc.pdf\">Nat\u00fcrliches Schlie\u00dfen in Coq (Ein einf\u00fchrendes Tutorial)<\/a>. ~ Burkhardt Renz. #Logic #ITP #Coq<\/li>\n<li><a href=\"https:\/\/stacks.stanford.edu\/file\/druid:jt562cf4590\/dselsam_dissertation_final-augmented.pdf\">Neural networks and the satisfiability problem<\/a>. ~ Daniel Selsam. #PhD_Thesis #Logic #SAT #NeuralNetworks<\/li>\n<li><a href=\"https:\/\/github.com\/dselsam\/neurosat\">NeuroSAT: Learning a SAT solver from single-bit supervision<\/a>. ~ Daniel Selsam. #Logic #SAT #NeuralNetworks<\/li>\n<li><a href=\"https:\/\/lexi-lambda.github.io\/blog\/2019\/09\/07\/demystifying-monadbasecontrol\/\">Demystifying MonadBaseControl<\/a>. ~ Alexis King (@lexi_lambda). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/335312902_Logic_Algebra_and_Geometry_at_the_Foundation_of_Computer_Science\">Logic, algebra, and geometry at the foundation of computer science<\/a>. ~ T. Hoare, A. Mendes, J.F. Ferreira. #Math #CompSci<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=221\">Breve historia de la Inteligencia Artificial<\/a>. ~ F. Sancho (@sanchocaparrini). #IA #Historia<\/li>\n<li><a href=\"https:\/\/sf.snu.ac.kr\/compcertm\/\">CompCertM: CompCert with lightweight modular verification and multi-language linking<\/a>. ~ Youngju Song et als. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/lamb-the-lambda.com\/haskell\/2019\/09\/07\/five-cartesian.html\">Five ways to compute the cartesian product with Haskell<\/a>. ~ Andrew Ribeiro (@AndrewJRibeiro). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blogs.dropbox.com\/tech\/2019\/09\/our-journey-to-type-checking-4-million-lines-of-python\/\">Our journey to type checking 4 million lines of Python<\/a>. ~ Jukka Lehtosalo. #Python<\/li>\n<li><a href=\"http:\/\/informatica.blogs.uoc.edu\/2019\/09\/09\/ia-hombres-maquinas\">IA: hombres y m\u00e1quinas<\/a>. ~ Jos\u00e9 Ram\u00f3n Rodr\u00edguez. #IA<\/li>\n<li><a href=\"https:\/\/cse.buffalo.edu\/~rapaport\/Papers\/phics.pdf\">Philosophy of Computer Science<\/a>. ~ William J. Rapaport. #CompSci #Philosophy<\/li>\n<li><a href=\"https:\/\/www.nytimes.com\/2019\/09\/06\/opinion\/ai-explainability.html\">How to build Artificial Intelligence we can trust<\/a>. ~ Gary Marcus (@GaryMarcus). #AI<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/9\/2\/running-training-iterations\">Running training iterations<\/a>. | Monday Morning Haskell. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/r6.ca\/blog\/20171010T001746Z.html\">Functor-oriented programming<\/a>. ~ Russell O\u2019Connor. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/odone.io\/posts\/2019-09-09-fun-with-typeclasses.html\">Fun with Typeclasses<\/a>. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Hybrid_Systems_VCs.html\">Verification components for hybrid systems in Isabelle\/HOL<\/a>. ~ Jonathan Julian Huerta y Munive. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Fourier.html\">Fourier series in Isabelle\/HOL<\/a>. ~ Lawrence C Paulson. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11088\/pdf\/LIPIcs-ITP-2019-33.pdf\">The DPRM theorem in Isabelle<\/a>. ~ J. Bayer et als. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11076\/pdf\/LIPIcs-ITP-2019-21.pdf\">Virtualization of HOL4 in Isabelle<\/a>. ~ F. Immler, J. R\u00e4dle, M. Wenzel. #ITP #IsabelleHOL #HOL4<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11068\/pdf\/LIPIcs-ITP-2019-13.pdf\">Formal proofs of Tarjan&#8217;s strongly connected components algorithm in Why3, Coq and Isabelle<\/a>. ~ R. Chen et als. #ITP #IsabelleHOL #Coq #Why3<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11059\/pdf\/LIPIcs-ITP-2019-4.pdf\">A verified compositional algorithm for AI planning<\/a>. ~ M. Abdulaziz, C. Gretton, M. Norrish. #ITP #HOL4 #AI<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11060\/pdf\/LIPIcs-ITP-2019-5.pdf\">Proving tree algorithms for succinct data structures<\/a>. ~ R. Affeldt et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/her.esy.fun\/slides\/Intro-to-FP-with-Haskell.html\">Introduction \u00e0 la programmation fonctionnelle avec Haskell<\/a>. ~ Yann Esposito (@yogsototh). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/falacias.escepticos.es\">Falacias l\u00f3gicas explicadas gr\u00e1ficamente<\/a>. #L\u00f3gica<\/li>\n<li><a href=\"https:\/\/rationalwiki.org\/wiki\/Pseudomathematics\">Pseudomathematics<\/a>. #Math<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11061\/pdf\/LIPIcs-ITP-2019-6.pdf\">Data types as quotients of polynomial functors<\/a>. ~ J. Avigad, M. Carneiro, S. Hudon. #ITP #LeanProver<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11062\/pdf\/LIPIcs-ITP-2019-7.pdf\">Primitive Floats in Coq<\/a>. ~ G. Bertholon, E. Martin-Dorel, P. Roux. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11063\/pdf\/LIPIcs-ITP-2019-8.pdf\">A certificate-based approach to formally verified approximations<\/a>. ~ F. Br\u00e9hard, A. Mahboubi, D. Pous. #ITP #Coq #Math<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11064\/pdf\/LIPIcs-ITP-2019-9.pdf\">Higher-order Tarski Grothendieck as a foundation for formal proof<\/a>. ~ C.E. Brown, C. Kaliszyk, K. Pak. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11065\/pdf\/LIPIcs-ITP-2019-10.pdf\">Generic authenticated data structures, formally<\/a>. ~ M. Brun, D. Traytel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11066\/pdf\/LIPIcs-ITP-2019-11.pdf\">A verified and compositional translation of LTL to deterministic Rabin automata<\/a>. ~ J. Brunner, B. Seidl, S. Sickert. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11067\/pdf\/LIPIcs-ITP-2019-12.pdf\">Formalizing computability theory via partial recursive functions<\/a>. ~ M. Carneiro. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/github.com\/ChrisPenner\/astar-monad\">A smart A* search monad transformer which supports backtracking user-state<\/a>. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming #AI<\/li>\n<li><a href=\"https:\/\/slides.com\/volpegabriel\/why-types-matte\">Why types matter<\/a>. ~ Gabrie\u03bb Volpe (@volpegabriel87).r#\/ #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/nikita-volkov.github.io\/\/refined\/\">Announcing the refinement types library<\/a>. ~ Nikita Volkov (@NikitaYVolkov). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/lisp-univ-etc.blogspot.com\/2019\/09\/programming-algorithms-hash-tables.html%20\">Programming algorithms: Hash-tables<\/a>. ~ Vsevolod Dyomkin. #Programming #CommonLisp #Algorithms<\/li>\n<li><a href=\"https:\/\/kite.com\/blog\/python\/functional-programming\/\">Best practices for using functional programming in Python<\/a>. ~ Amandine Lee (@momandine). #Python #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/artint.info\/\">Artificial Intelligence: Foundations of computational agents, second edition<\/a>. ~ David Poole, Alan Mackworth. #eBook #AI<\/li>\n<li><a href=\"https:\/\/blog.sigplan.org\/2019\/09\/12\/program-verification-has-it-lost-its-punch\/\">&#8220;Program Verification&#8221;: Has it lost its punch?<\/a> ~ Nikhil Swamy. #FormalVerification<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11069\/pdf\/LIPIcs-ITP-2019-14.pdf\">First-order guarded coinduction in Coq<\/a>. ~ L. Czajka. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11070\/pdf\/LIPIcs-ITP-2019-15.pdf\">Formalizing the solution to the cap set problem<\/a>. ~ S.R. Dahmen, J. H\u00f6lzl, R.Y. Lewis. #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11071\/pdf\/LIPIcs-ITP-2019-16.pdf\">Nine chapters of analytic number theory in Isabelle\/HOL<\/a>. ~ M. Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/t.co\/Otgbgo8xxG?amp=1\">Nine chapters of analytic number theory in Isabelle\/HOL (Slides)<\/a>. ~ Manuel Eberl (@pruvisto). #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11072\/pdf\/LIPIcs-ITP-2019-17.pdf\">A certifying extraction with time bounds from Coq to call-by-value lambda calculus<\/a>. ~ Y. Forster, F. Kunze. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11073\/pdf\/LIPIcs-ITP-2019-18.pdf\">Formal proof and analysis of an incremental cycle detection algorithm<\/a>. ~ A. Gu\u00e9neau et als. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11074\/pdf\/LIPIcs-ITP-2019-19.pdf\">A formalization of forcing and the unprovability of the continuum hypothesis<\/a>. ~ J.M. Han, F. van Doorn. #ITP #LeanProver<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11075\/pdf\/LIPIcs-ITP-2019-20.pdf\">Refinement with time (Refining the run-time of algorithms in Isabelle\/HOL)<\/a>. ~ M.P.L. Haslbeck, P. Lammich. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1909.05618\">Predicate transformer semantics for hybrid systems: Verification components for Isabelle\/HOL<\/a>. ~ J.J. Huerta y Munive, G. Struth. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/sicp.comp.nus.edu.sg\/sicpjs.pdf\">Structure and interpretation of computer programs (JavaScript adaptation)<\/a>. ~ H. Abelson et als. #eBook #Programming #JavaScript<\/li>\n<li><a href=\"https:\/\/alva.re\/wp-content\/uploads\/2019\/07\/elle_preprint_072019.pdf\">Elle: Foundationally verified compilation for Ethereum<\/a>. ~ M.M. Alvarez. #ITP #IsabelleHOL #Ethereum<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11077\/pdf\/LIPIcs-ITP-2019-22.pdf\">Generating verified LLVM from Isabelle\/HOL<\/a>. ~ P. Lammich. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11080\/pdf\/LIPIcs-ITP-2019-25.pdf\">Binary-compatible verification of filesystems with ACL2<\/a>. ~ M.P. Mehta, W.R. Cook. #ITP #ACL2<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11082\/pdf\/LIPIcs-ITP-2019-27.pdf\">Verifying that a compiler preserves concurrent value-dependent information-flow security<\/a>. ~ R. Sison, T. Murray. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11083\/pdf\/LIPIcs-ITP-2019-28.pdf\">Quantitative continuity and computable analysis in Coq<\/a>. ~ F. Steinberg, L. Th\u00e9ry, H. Thies. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11084\/pdf\/LIPIcs-ITP-2019-29.pdf\">Deriving proved equality tests in Coq-Elpi: Stronger induction principles for containers in Coq<\/a>. ~ E. Tassi. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11085\/pdf\/LIPIcs-ITP-2019-30.pdf\">Complete non-orders and fixed points<\/a>. ~ A. Yamada, J. Dubut. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11086\/pdf\/LIPIcs-ITP-2019-31.pdf\">Verified decision procedures for modal logics<\/a>. ~ M. Wu, R. Gor\u00e9. #ITP #LeanProver #Logic<\/li>\n<li><a href=\"https:\/\/www.welcometothejungle.co\/fr\/articles\/btc-deep-learning-clojure-haskell\">The beauty of functional languages in Deep Learning\u200a\u2014\u200aClojure and Haskell<\/a>. ~ Jun Wu. #Clojure #Haskell #FunctionalProgramming #DeepLearning<\/li>\n<li><a href=\"https:\/\/blog.poisson.chat\/posts\/2019-09-13-reverse.html\">Making Haskell run fast: the many faces of reverse<\/a>. ~ Li-yao Xia. #Haskell #FunctionalProgramming #ITP #Coq<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11090\/pdf\/LIPIcs-ITP-2019-35.pdf\">Declarative proof translation<\/a>. ~ C. Kaliszyk, K. Pak. #ITP #IsabelleHOL #Mizar<\/li>\n<li><a href=\"http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/11091\/pdf\/LIPIcs-ITP-2019-36.pdf\">Formalization of the domination chain with weighted parameters<\/a>. ~ D.E. Sever\u00edn. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1909.01414\">From type theory to setoids and back<\/a>. ~ E. Palmgren. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/www21.in.tum.de\/~eberlm\/pubs\/sds_isabelle.html\">Verifying randomised social choice<\/a>. ~ M. Eberl (@pruvisto). #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/www.andrew.cmu.edu\/user\/avigad\/Papers\/mutilated.pdf\">A formalization of the mutilated chessboard problem in Lean<\/a>. ~ Jeremy Avigad. #ITP #LeanProver<\/li>\n<li><a href=\"http:\/\/www.jens-otten.de\/tutorial_tableaux19\/\">How to build an automated theorem prover<\/a>. ~ Jens Otten. #Logic #ATP #Prolog<\/li>\n<li><a href=\"https:\/\/www.mat.ufrn.br\/cade-27\/wp-content\/uploads\/2019\/09\/tutorial-RL.pdf\">Building theorem provers using rewriting logic<\/a>. ~ Carlos Olarte. #Logic #ATP #Maude<\/li>\n<li><a href=\"https:\/\/www.mat.ufrn.br\/cade-27\/wp-content\/uploads\/2019\/09\/2019CN-CADE.pdf\">Machine-oriented reasoning<\/a>. ~ Cl\u00e1udia Nalon. #Logic #ATP<\/li>\n<li><a href=\"http:\/\/jens-otten.de\/tutorial_cade19\">Build your own first-order prover<\/a>. ~ Jens Otten. #Logic #ATP #Prolog<\/li>\n<li><a href=\"http:\/\/cl-informatik.uibk.ac.at\/users\/swinkler\/arcade\/pdfs\/2.pdf\">Stronger higher-order automation: A report on the ongoing Matryoshka project<\/a>. ~ Jasmin Blanchette et als. #ITP #ATP<\/li>\n<li><a href=\"http:\/\/fmv.jku.at\/papers\/HeuleKieslBiere-NFM19.pdf\">Clausal proofs of mutilated chessboards<\/a>. ~ M.J.H. Heule, B. Kiesl, A. Biere. #ATP #PR<\/li>\n<li><a href=\"https:\/\/morgenthum.dev\/articles\/why-prefer-fp\">Why I prefer functional programming<\/a>. ~ Mario Morgenthum. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.bbvaopenmind.com\/tecnologia\/mundo-digital\/lenguaje-programacion-parte-1\/\">\u00bfQu\u00e9 es un lenguaje de programaci\u00f3n? (Parte 1)<\/a>. ~ Alejandro Serrano (@trupill). #Programaci\u00f3n<\/li>\n<li><a href=\"https:\/\/www.bbvaopenmind.com\/tecnologia\/mundo-digital\/la-torre-de-babel-informatica-de-los-lenguajes-de-programacion\/\">La Torre de Babel inform\u00e1tica de los lenguajes de programaci\u00f3n<\/a>. ~ Alejandro Serrano (@trupill). #Programaci\u00f3n<\/li>\n<li><a href=\"http:\/\/profs.sci.univr.it\/~bonacina\/talks\/SSFT2019OrdBasedStrat-slides.pdf\">Overview of automated reasoning and ordering-based strategies<\/a>. ~ Maria Paola Bonacina. #Logic #ATP<\/li>\n<li><a href=\"https:\/\/staff.aist.go.jp\/reynald.affeldt\/coq2019\/coqws2019-steinberg-thies-slides.pdf\">Computable analysis, exact real arithmetic and analytic functions in Coq<\/a>. ~ F. Steinberg, H. Thies. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/staff.aist.go.jp\/reynald.affeldt\/coq2019\/coqws2019-tabareau-slides.pdf\">Not a single proof assistant for all, but proof assistants for everyone<\/a>. ~ Nicolas Tabareau. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/basics.sjtu.edu.cn\/~yuxin\/publications\/Coqprob.pdf\">Formalisation of probabilistic testing semantics in Coq<\/a>. ~ Y. Deng, J.F. Monin. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/odone.io\/posts\/2019-09-16-mars-rover-kata-in-haskell.html\">Mars Rover Kata in Haskell<\/a>. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/vitez.me\/building-lenses\">Building lenses (Implementing basic Haskell lenses in twenty exercises)<\/a>. ~ Mitchell Vitez. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/williamyaoh.com\/posts\/2019-09-16-time-cheatsheet.html\">A cheatsheet to the time library<\/a>. ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/9\/16\/adding-random-exploration\">Monday Morning Haskell: Adding random exploration<\/a>. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/basics.sjtu.edu.cn\/~yuxin\/teaching\/Coq\/fpintro2019.pdf\">Functional programming in Coq<\/a>. ~ Yuxin Deng. #FunctionalProgramming #ITP #Coq #LambdaCalculus<\/li>\n<li><a href=\"http:\/\/www.cs.yale.edu\/homes\/piskac\/papers\/2019HallahanETALquasiquoter.pdf\">G2Q: Haskell constraint solving<\/a>. ~ W.T. Hallahan, A. Xue, R. Piskac. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1909.04160\">Structural and semantic pattern matching analysis in Haskell<\/a>. ~ P. Kalvoda, T.S. Kerckhove. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.stackbuilders.com\/news\/from-type-theory-to-haskell-in-10-minutes\">From type theory to Haskell in 10 minutes<\/a>. ~ Matt Campbell. #Haskell #LambdaCalculus #TypeTheory<\/li>\n<li><a href=\"https:\/\/maxhallinan.com\/posts\/2019\/09\/17\/what-is-datatype-generic-programming\/\">What is datatype-generic programming?<\/a> ~ Max Hallinan. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/EggBaconAndSpam\/eggbaconandspam.github.io\/blob\/master\/posts\/2019-09-16-Seekable-Parsers.md\">Seekable parsers in Haskell<\/a>. ~ Frederik Ramcke. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.logicmatters.net\/2019\/09\/17\/j-donald-monk-lectures-on-set-theory\/\">J. Donald Monk, Mathematical logic and lectures on set theory<\/a>. #eBook #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.gwern.net\/The-Existential-Risk-of-Mathematical-Error\">The existential risk of Math errors<\/a>. ~ Gwern Branwen. #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1906.06251\">Effective problem solving using SAT solvers<\/a>. ~ Curtis Bright et als. #SAT_solving<\/li>\n<li><a href=\"http:\/\/dx.doi.org\/10.4204\/EPTCS.306.8\">Prolog coding guidelines: Status and tool support<\/a>. ~ F. Nogatz, P. K\u00f6rner, S. Krings. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1909.07479\">On correctness of an n queens program<\/a>. ~ W. Drabent. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Generic_Join.html\">Formalization of multiway-join algorithms in Isabelle\/HOL<\/a>. ~ Thibault Dardinier. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/chrispenner.ca\/posts\/slick-template\">Slick 1.0 Release &#8211; Now with a quick and easy template!<\/a> ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/occasionallycogent.com\/prolog_fundamentals_catchup\/index.html\">Prolog fundamentals catchup<\/a>. ~ James Norman Vladimir Cash (@jamesnvc). #Prolog #LogicProgramming<\/li>\n<li><a href=\"http:\/\/www.pathwayslms.com\/swipltuts\/html\/index.html\">Tutorial: Creating Web applications in SWI-Prolog<\/a>. ~ Anne Ogborn. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/prologhub.pl\/functional-prolog-map-filter-and-reduce\/\">Functional Prolog: map, filter and reduce<\/a>. ~ Paul Brown. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/www.bbvaopenmind.com\/tecnologia\/inteligencia-artificial\/la-deuda-de-la-inteligencia-artificial-con-el-matematico-godel\/\">La deuda de la Inteligencia Artificial con el matem\u00e1tico G\u00f6del<\/a>. ~ Javier Mu\u00f1oz de la Cuesta. #L\u00f3gica #IA<\/li>\n<li><a href=\"https:\/\/github.com\/sheyll\/newtype-zoo\">A zoo of Haskell newtype wrappers<\/a>. ~ Sven Heyll. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/donyaquick.com\/interesting-music-in-four-lines-of-code\/\">Interesting music in four lines of code<\/a>. ~ Donya Quick. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/shemesh.larc.nasa.gov\/people\/cam\/publications\/vscode-pvs-draft.pdf\">An integrated development environment for the Prototype Verification System (PVS)<\/a>. ~ P. Masci, C.A. Mu\u00f1oz. #ITP #PVS<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1909.05464\">A formal semantics of Findel (Financial Derivatives Language) in Coq<\/a>. ~ A. Arusoaie #ITP #Coq<\/li>\n<li><a href=\"https:\/\/repository.tudelft.nl\/islandora\/object\/uuid:229b0db1-06e9-4cbd-9e90-e2e16bd162bb\">Formal verification of upper bounds on translative packing densities<\/a>. ~ I. Mulder. #MSc_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2019-09-20-monad-bayes-1.html\">Probabilistic programming with Monad\u2011Bayes. Part 1: first steps<\/a>. ~ S. Bhat, S. Carstens, M. Meschede. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/learning-haskell\">Learning Haskell: A resource guide<\/a>. ~ Denis Oleynikov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/bartoszmilewski.com\/2019\/09\/20\/the-power-of-adjunctions\/\">The power of adjunctions<\/a>. ~ Bartosz Milewski. #CategoryTheory #Programming<\/li>\n<li><a href=\"https:\/\/chrispenner.ca\/posts\/lens-regex-pcre\">Optics + Regex: Greater than the sum of their parts<\/a>. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/svenkeidel.de\/papers\/analysis-components.pdf\">Sound and reusable components for abstract interpretation<\/a>. ~ S. Keidel, S. Erdweg. #Haskell #FunctionalProgramming via @Iceland_jack<\/li>\n<li><a href=\"http:\/\/jhc.sjtu.edu.cn\/uploadfile\/2019\/0905\/20190905014559847.pdf\">Certifying graph-manipulating C programs via localizations within data structures<\/a>. ~ Shengyi Wang et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/staticanalysis.org\/tapas2019\/talks\/TAPAS_2019_paper_16.pdf\">Leveraging highly automated theorem proving for certification<\/a>. ~ Deni Raco et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/iris-project.org\/pdfs\/2019-sosp-perennial-final.pdf\">Verifying concurrent, crash-safe systems with Perennial<\/a>. ~ Tej Chajed et als. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?ICLP2019.26\">Lazy stream programming in Prolog<\/a>. ~ Paul Tarau, Jan Wielemaker, Tom Schrijvers. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Linear_Programming.html\">Linear programming in Isabelle\/HOL<\/a>. ~ Julian Parsert and Cezary Kaliszyk. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/linear-algebra-of-types\/\">Linear algebra of types<\/a>. ~ Philip Zucker (@SandMouth). #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=223\">Introducci\u00f3n a la L\u00f3gica<\/a>. ~ F. Sancho (@sanchocaparrini). #L\u00f3gica<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=222\">Brev\u00edsima historia de la L\u00f3gica<\/a>. ~ F. Sancho (@sanchocaparrini). #L\u00f3gica<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/9\/23\/tweaks-fixes-and-some-results\">Monday morning Haskell: Tweaks, fixes, and some results<\/a>. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming #AI<\/li>\n<li><a href=\"https:\/\/svejcar.dev\/posts\/2019\/09\/23\/haskell-on-raspberry-pi-4\/\">Haskell on Raspberry PI 4<\/a>. ~ Vaclav Svejcar. #Haskell #FunctionalProgramming #Raspberry<\/li>\n<li><a href=\"https:\/\/odone.io\/posts\/2019-09-23-refactoring-the-mars-rover-kata-in-haskell.html.\">Refactoring the Mars Rover Kata in Haskell<\/a>. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/realpython.com\/emacs-the-best-python-editor\">Emacs &#8211; The best Python editor?<\/a> ~ Kyle Purdon (@PurdonKyle). #Emacs #Python<\/li>\n<li><a href=\"https:\/\/www21.in.tum.de\/~traytel\/papers\/rv19-verimon\/verimon.pdf\">A formally verified monitor for metric first-order temporal logic<\/a>. ~ J. Schneider et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/people.inf.ethz.ch\/trayteld\/papers\/atva19-adaptive\/aom.pdf\">Adaptive online first-order monitoring<\/a>. ~ J. Schneider et als #ITP #IsabelLEHOL<\/li>\n<li><a href=\"https:\/\/philpapers.org\/go.pl?id=BLUIFP&amp;u=https%3A%2F%2Fphilpapers.org%2Farchive%2FBLUIFP.pdf\">Isabelle for philosophers<\/a>. ~ Ben Blumson. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/www.kestrel.edu\/home\/people\/coglio\/rlp.pdf\">Ethereum\u2019s recursive length prefix in ACL2<\/a>. ~ Alessandro Coglio. #ITP #ACL2 #Ethereum<\/li>\n<li><a href=\"http:\/\/www.well-typed.com\/blog\/2019\/09\/eventful-ghc\/\">Eventful GHC (debugging \/ profiling Haskell via the GHC eventlog)<\/a>. ~ Alp Mestanogullari (@alpmestan). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1909.11342\">A formal proof of Hensel&#8217;s lemma over the p-adic integers<\/a>. ~ Robert Y. Lewis. #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/homepage.divms.uiowa.edu\/~viswanathn\/qual.pdf\">Comparison of proof producing systems in SMT solvers<\/a>. ~ Arjun Viswanathan. #ATP #SMT<\/li>\n<li><a href=\"http:\/\/www.cs.us.es\/~fsancho\/?e=224\">L\u00f3gica de primer orden: una introducci\u00f3n informal<\/a>. F. Sancho (@sanchocaparrini). #L\u00f3gica<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/news\/239748-number-theorist-fears-all-published-math-is-wrong\/fulltext\">Number theorist fears all published Math is wrong<\/a>. ~ Mordechai Rorvig. #Math #ITP #AI<\/li>\n<li><a href=\"https:\/\/blog.ploeh.dk\/2019\/09\/23\/unit-testing-wai-applications\/\">Unit testing wai applications<\/a>. ~ Mark Seemann (@ploeh). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1909.10451\">Efficient stochastic programming in Julia<\/a>. ~ M. Biel, M. Johansson. #Programming #JuliaLang<\/li>\n<li><a href=\"https:\/\/www.theoj.org\/jose-papers\/jose.00029\/10.21105.jose.00029.pdf\">Mikrokosmos: an educational lambda calculus interpreter<\/a>. ~ M. Rom\u00e1n. #LambdaCalculus #Haskell<\/li>\n<li><a href=\"http:\/\/lisp-univ-etc.blogspot.com\/2019\/09\/programming-algorithms-trees.html\">Programming algorithms: Trees<\/a>. ~ Vsevolod Dyomkin. #Programming #CommonLisp #Algorithms<\/li>\n<li><a href=\"https:\/\/bonotake.github.io\/deep%20learning%20and%20cs\/2019\/08\/02\/origin-of-differentiable-programming.html\">Where did \u201cdifferentiable programming\u201d come from?<\/a> ~ Takeo Imai (@bonotake). #DeepLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1909.12582\">Towards Coq-verified Esterel semantics and compiling<\/a>. ~ G. Berry, L. Rieg. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/333918631_Quantum_Computing_in_Haskell\">Quantum computing in Haskell<\/a>. ~ Christopher Wright. #BSc_Thesis #Haskell #FunctionalProgramming<\/li>\n<\/ul>\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante septiembre 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\/6914"}],"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=6914"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6914\/revisions"}],"predecessor-version":[{"id":6915,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6914\/revisions\/6915"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6914"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6914"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6914"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}