{"id":7609,"date":"2021-08-01T19:38:21","date_gmt":"2021-08-01T17:38:21","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7609"},"modified":"2021-08-30T19:39:30","modified_gmt":"2021-08-30T17:39:30","slug":"resumen-de-lecturas-compartidas-durante-julio-de-2021","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-julio-de-2021\/","title":{"rendered":"Resumen de lecturas compartidas durante julio de 2021"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante julio de 2021, 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:\/\/www21.informatik.tu-muenchen.de\/students\/past\/interval_newton\/assets\/newton.pdf\">Formalisation of interval methods for nonlinear root-finding<\/a>. ~ Daniel Seidl. #BSc_Thesis #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2107.11838\">New algebraic normative theories for ethical and legal reasoning in the LogiKEy framework<\/a>. ~ Ali Farjami. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/dspace.library.uu.nl\/handle\/1874\/403363\">The categorical origin of monads in Haskell<\/a>. ~ Marien Matser. #BSc_Thesis #Haskell #FunctionalProgramming #CategoryTheory<\/li>\n<li><a href=\"https:\/\/analyticsindiamag.com\/what-separates-ai-from-an-idiot-savant-is-common-sense-hector-levesque\/\">What separates AI from an idiot savant is common sense: Hector Levesque<\/a>. #AI #KRR<\/li>\n<li><a href=\"https:\/\/mathscholar.org\/2021\/07\/computer-theorem-prover-verifies-sophisticated-new-result\/\">Computer theorem prover verifies sophisticated new result<\/a>. ~ David H Bailey. #ITP #ATP #Math #AI<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2107.14044\">Ethical AI for Social Good<\/a>. ~ Ramya Akula, Ivan Garibay. #AI<\/li>\n<li><a href=\"https:\/\/www.foxhound.systems\/blog\/composable-data-validation\/\">Composable data validation with Haskell<\/a>. ~ Ben Levy, Christian Charukiewicz. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.sumtypeofway.com\/posts\/ode-to-a-streaming-bytestream.html\">Ode to a streaming ByteString (Or: lazy I\/O without shooting yourself in the foot)<\/a>. ~ Patrick Thomson. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/coot.me\/posts\/containers-strict-foldr.html\">Strictness of foldr&#8217; from containers<\/a>. ~ Marcin Szamotulski. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/easychair.org\/publications\/preprint\/k1hv\">Formalization of Gambler\u2019s Ruin Problem in Isabelle\/HOL<\/a>. ~ Zibo Yang. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/easychair.org\/publications\/preprint\/XmvS\">Formalization of RBD-based Cause Consequence Analysis in HOL<\/a>. ~ Mohamed Abdelghany, Sofiene Tahar. #ITP #HOL4<\/li>\n<li><a href=\"https:\/\/easychair.org\/publications\/preprint\/gGb9\">Inductive Benchmarks for Automated Reasoning<\/a>. ~ M\u00e1rton Hajdu, Petra Hozzov\u00e1, Laura Kov\u00e1cs, Johannes Schoisswohl, Andrei Voronkov. #ATP<\/li>\n<li><a href=\"https:\/\/easychair.org\/publications\/preprint\/sD76\">Formalizing the Gromov-Hausdorff Space<\/a>. ~ S\u00e9bastien Gou\u00ebzel. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/easychair.org\/publications\/preprint\/38w1\">Formalizing rotation number and its properties in Lean<\/a>. ~ Yury Kudryashov. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/easychair.org\/publications\/preprint\/mC9X\">Scalar actions in Lean&#8217;s Mathlib<\/a>. ~ Eric Wieser. #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/flaviomoura.info\/files\/fmm21.pdf\">A formalization of the (compositional) Z property<\/a>. ~ Fl\u00e1vio L. C. de Moura,a Leandro O. Rezende. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/flaviomoura.info\/files\/reportZtoConfl.pdf\">Confluence via the Z property in Coq<\/a>. ~ Fl\u00e1vio L. C. de Moura, Leandro O. Rezende. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2107.13509\">The who in explainable AI: How AI background shapes perceptions of AI explanations<\/a>. ~ Upol Ehsan, Samir Passi, Q. Vera Liao, Larry Chan, I-Hsiang Lee, Michael Muller, Mark O. Riedl. #AI #XAI<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/research\/group\/logic\/TypesSS05\/Extra\/wiedijk_2.pdf\">The QED Manifesto<\/a>. #ATP #ITP<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/lean-computer-program-confirms-peter-scholze-proof-20210728\/\">Proof assistant makes jump to big-league Math<\/a>. ~ Kevin Hartnett. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/353208312_Integrating_an_Automated_Prover_for_Projective_Geometry_as_a_New_Tactic_in_the_Coq_Proof_Assistant\">Integrating an automated prover for projective geometry as a new tactic in the Coq proof assistant<\/a>. ~ Nicolas Magaud. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/353526866_Is_computer_algebra_ready_for_conjecturing_and_proving_geometric_inequalities_in_the_classroom\">Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom?<\/a> ~ Zolt\u00e1n Kov\u00e1cs, Tom\u00e1s Recio, Robert Vajda, M. Pilar V\u00e9lez. #GeoGebra #Math<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/Zoltan-Kovacs-3\/publication\/353466393_Is_computer_algebra_ready_for_conjecturing_and_proving_geometric_inequalities_in_the_classroom\/links\/60ff0d602bf3553b29142ca4\/Is-computer-algebra-ready-for-conjecturing-and-proving-geometric-inequalities-in-the-classroom.pdf?origin=homeFeed_download&amp;_iepl%5BactivityId%5D=1396227761647622&amp;_iepl%5BactivityTimestamp%5D=1627257600&amp;_iepl%5BactivityType%5D=person_publish_publication&amp;_iepl%5Bcontexts%5D%5B0%5D=homeFeed&amp;_iepl%5BrecommendationActualVariant%5D=&amp;_iepl%5BrecommendationDomain%5D=&amp;_iepl%5BrecommendationScore%5D=&amp;_iepl%5BrecommendationTargetActivityCombination%5D=&amp;_iepl%5BrecommendationType%5D=&amp;_iepl%5BfeedVisitIdentifier%5D=&amp;_iepl%5BpositionInFeed%5D=11&amp;_iepl%5BsingleItemViewId%5D=KUZ4i5ThvdxaoZf1ctK2jh1s&amp;_iepl%5BviewId%5D=mkX7HMc1c9d9Y7Hyr4ISW4R9&amp;_iepl%5BhomeFeedVariantCode%5D=ncls&amp;_iepl%5B__typename%5D=HomeFeedTrackingPayload&amp;_iepl%5BinteractionType%5D=publicationDownload&amp;_iepl%5BtargetEntityId%5D=PB%3A353466393\">Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom? [Slides<\/a>] ~ Zolt\u00e1n Kov\u00e1cs, Tom\u00e1s Recio, Robert Vajda, M. Pilar V\u00e9lez. #GeoGebra #Math<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007%2F978-3-030-52200-1_27.pdf\">A formalization of properties of continuous functions on closed intervals<\/a>. ~ Yaoshun Fu, Wensheng Yu. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/github.com\/coderfys\/Analysis\">Formal analysis in Coq<\/a>. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/raw.githubusercontent.com\/mirefek\/geo_logic\/master\/article\/geo_logic.pdf\">GeoLogic \u2013 Graphical interactive theorem prover for Euclidean geometry<\/a>. ~ Miroslav Olsak. #ITP #Logic #Math<\/li>\n<li><a href=\"https:\/\/github.com\/mirefek\/geo_logic\">GeoLogic: Tool for euclidean geometry aware of logic<\/a>. ~ Miroslav Olsak. #ITP #Logic #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2107.11674\">Case studies in formal reasoning about lambda-calculus: Semantics, Church-Rosser, standardization and HOAS<\/a>. ~ Lorenzo Gheri, Andrei Popescu. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/www.math.uni-bonn.de\/ag\/logik\/teaching\/2021SS\/Introduction_Naproche.pdf\">An introduction to the Naproche natural language proof checker<\/a>. ~ Peter Koepke. #ITP #IsabelleHOL #Naproche #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/~hagemeier\/files\/thesis.pdf\">Intuitionistic epistemic logic in Coq<\/a>. ~ Christian Albert Hagemeier. #BSc_Thesis #ITP #Coq #Logic<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/magazines\/2021\/8\/254304-what-does-saying-that-programming-is-hard-really-say-and-about-whom\/fulltext\">What does saying that &#8216;Programming is hard&#8217; really say, and about whom? ~ Brett A<\/a>. Becker. #Programming<\/li>\n<li><a href=\"https:\/\/gist.github.com\/MantasBaksys\/5db553021d417b62f33a8c821581498f\">Formalization in Lean of IMO 2021 Q1<\/a>. ~ Mantas Baksys. #ITP #LeanProver #Math #IMO<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2107.10988\">Formalizing Galois theory (in Lean)<\/a>. ~ Thomas Browning, Patrick Lutz. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/frasertweedale.github.io\/blog-fp\/posts\/2021-07-26-hakyll-without-sources.html\">Hakyll how-to: pages without source files<\/a>. ~ Fraser Tweedale. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.cantorsparadise.com\/why-math-is-an-art-not-a-science-94d234cacb76\">Why math is an art, not a science<\/a>. ~ Peter Flom. #Math<\/li>\n<li><a href=\"https:\/\/github.com\/b-mehta\/combinatorics\">Combinatorics in Lean<\/a>. ~ Bhavik Mehta. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/056d709743bfc8371400dfbe1b2d4b627d89f6ef\/src\/model_theory\/basic.lean\">First-order languages and structures in Lean<\/a>. ~ Aaron Anderson, Jesse Michael Han, Floris van Doorn. #ITP #LeanProver #Logic #Math<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/8a0d5e07c88b8b6a36f183e4b1b8d8a4d81f9df8\/src\/group_theory\/complement.lean\">Schur\u2013Zassenhaus theorem in Lean<\/a>. ~ Thomas Browning. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/j5RIZAzooAg\">Univalence from a computer science point-of-view<\/a>. ~ Dan Licata. #Logic #Math #CompSci<\/li>\n<li><a href=\"https:\/\/mpodlasin.com\/articles\/haskell-i\">Haskell (The most gentle introduction ever)<\/a>. ~ Mateusz Podlasin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www21.in.tum.de\/~wenzelm\/papers\/romantic.pdf\">A comparison of the mathematical proof languages Mizar and Isar<\/a>. ~ Freek Wiedijk, Markus Wenzel. #ITP #Mizar #IsabelleHOL #Isar<\/li>\n<li><a href=\"https:\/\/www.cs.ru.nl\/~freek\/notes\/mv.pdf\">The mathematical vernacular<\/a>. ~ Freek Wiedijk. #ITP #Mizar #IsabelleIsar<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/53c830592cc48471c873df6b6ba726b764fcd7f0\/src\/analysis\/convex\/krein_milman.lean\">The Krein-Milman theorem in Lean<\/a>. ~ Ya\u00ebl Dillies. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.ma.imperial.ac.uk\/~buzzard\/M4000x_html\/M40001\/M40001_C1.html\">Sets and logic in Lean<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.ma.imperial.ac.uk\/~buzzard\/M4000x_html\/M40001\/M40001_C2.html\">Functions and equivalence relations in Lean<\/a>. ~ Kevin Buzzard. #ITP #LeanProver #Logic #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/0809.1552\">A computer verified, monadic, functional implementation of the integral<\/a>. ~ Russell O&#8217;Connor, Bas Spitters. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/luctielen.com\/posts\/static_analysis_using_haskell_and_datalog\/\">Static analysis using Haskell and Datalog<\/a>. ~ Luc Tielen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/brandonchinn178.github.io\/blog\/2021\/07\/23\/foralls-in-data-types.html\">`forall`s in Data Types<\/a>. ~ Brandon Chinn. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/cb21104b83e13a814b913cecc9601f55405bd888\/archive\/mccune.lean\">Every group is a McCune group (in Lean)<\/a>. ~ Bhavik Mehta. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-030-81685-8_2\">Balancing automation and control for formal verification of microprocessors<\/a>. #ITP #ACL2<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2107.10034\">Learning theorem proving components<\/a>. ~ Karel Chvalovsk\u00fd, Jan Jakub\u016fv, Miroslav Ol\u0161\u00e1k, Josef Urban. #ATP #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.02549\">Connecting constructive notions of ordinals in Homotopy Type Theory<\/a>. ~ Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. #HoTT #ITP #Agda #Logic #Math<\/li>\n<li><a href=\"https:\/\/books.google.es\/books?id=NvI4EAAAQBAJ&amp;lpg=PR3&amp;hl=es&amp;pg=PR\">Artificial intelligence (A textbook)<\/a>. ~ Charu C. Aggarwal.3#v=onepage&amp;q&amp;f=false #eBook #AI<\/li>\n<li><a href=\"https:\/\/mathematicswithoutapologies.wordpress.com\/2021\/07\/21\/announcing-a-new-newsletter-on-mechanizing-mathematics\">Announcing a new newsletter on mechanizing mathematics<\/a>. ~ Michael Harris. #ITP #ATP #Math<\/li>\n<li><a href=\"https:\/\/siliconreckoner.substack.com\/about\">Silicon Reckoner: an opinionated newsletter about the implications of mechanization of mathematics<\/a>. ~ Michael Harris. #ITP #ATP #Math<\/li>\n<li><a href=\"http:\/\/fmv.jku.at\/papers\/Fleury-EDA-Challenge-2021.pdf\">IsaSAT and Kissat entering the EDA Challenge 2021<\/a>. ~ Mathias Fleury. #ITP #IsabelleHOL #SATSolvers<\/li>\n<li><a href=\"https:\/\/github.com\/impermeable\/waterproof\">Waterproof: an educational environment for writing mathematical proofs in interactive notebooks<\/a>. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/pure.tue.nl\/ws\/portalfiles\/portal\/174693710\/BFP_Jan_Moraal.pdf\">Measure theory in Waterproof (Interactive theorem-proving for measure theory in an educational setting)<\/a>. ~ Jan Moraal. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.cs.princeton.edu\/~appel\/papers\/comp-opt-certicoq.pdf\">Compositional optimizations for CertiCoq<\/a>. ~ Zoe Paraskevopoulou, John M. Li, Andrew W. Appel. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/tel-03286314\/document\">Noetherian induction for computer-assisted first-order reasoning<\/a>. ~ Sorin Stratulat. #ITP #Coq #Logic #Math<\/li>\n<li><a href=\"https:\/\/eprints.ucm.es\/id\/eprint\/66943\/1\/BLAZQUEZ%20SABORIDO%2069815_JORGE_BLAZQUEZ_SABORIDO_Verificacion_de_estructuras_de_datos_enlazadas_en_Dafny_784051_493349558%20%281%29.pdf\">Verification of linked data structures in Dafny<\/a>. ~ Jorge Bl\u00e1zquez Saborido. #TFG #ATP #SMT #Dafny<\/li>\n<li><a href=\"https:\/\/rpeszek.github.io\/posts\/2021-07-18-prob-tree-scheme.html\">Probability tree diagrams. Recursion schemes. Why finding the right solution is sometimes hard?<\/a> ~ Robert Peszek. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/ocramz.github.io\/haskell\/automatic-differentiation\/2021\/07\/19\/ad-delcont.html\">Purely-functional reverse-mode automatic differentiation with delimited continuations<\/a>. ~ Marco Zocca. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2107.08821\">Proceedings of ICML 2021 workshop on theoretic foundation, criticism, and application trend of explainable AI<\/a>. #AI #MachineLearning #XAI<\/li>\n<li><a href=\"https:\/\/lucidmanager.org\/productivity\/publishing-with-org-mode-export\/\">Publishing articles and books with Org Mode export<\/a>. ~ Peter Prevos. #Emacs #OrgMode #LaTeX<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/master\/src\/combinatorics\/hales_jewett.lean\">The Hales-Jewett theorem (in Lean)<\/a>. ~ David W\u00e4rn. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.genbeta.com\/herramientas\/emacs-editor-texto-libre-vocacion-sistema-operativo-sus-extensiones-usadas-suplen-toda-clase-aplicaciones\">Emacs, el editor de texto libre con vocaci\u00f3n de sistema operativo: sus &#8216;extensiones&#8217; m\u00e1s usadas suplen toda clase de aplicaciones<\/a>. ~ Marcos Merino. #Emacs<\/li>\n<li><a href=\"https:\/\/forkast.news\/video-audio\/watch-charles-hoskinson-co-founder-of-ethereum-and-iohk-on-why-cardano-is-a-better-platform-part-i-2-2\/\">Of all the programming languages in the world, why Haskell? ~ Charles Hoskinson<\/a>. #Haskell #FunctionalProgramming #Cardano<\/li>\n<li><a href=\"https:\/\/github.com\/manateelazycat\/emacs-application-framework\">Emacs Application Framework (EAF)<\/a>. #Emacs<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2107.05225\">Incremental vulnerability detection via back-propagating symbolic execution of insecurity separation logic<\/a>. ~ Toby Murray, Pengbo Yan, Gidon Ernst. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2107.05493\">Integrating an automated prover for projective geometry as a new tactic in the Coq proof assistant<\/a>. ~ Nicolas Magaud. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/dione.lib.unipi.gr\/xmlui\/bitstream\/handle\/unipi\/13557\/AI_MSc_Thesis_EiriniVandorou.pdf\">Reasoning on figures of theoretical geometry theorems<\/a>. ~ Eirini Vandorou. #MSc_Thesis #Clojure #FunctionalProgramming #Prolog #LogicProgramming #Math<\/li>\n<li><a href=\"https:\/\/www.parsonsmatt.org\/2021\/07\/16\/hspec_hooks.html\">Hspec hooks<\/a>. ~ Matt Parsons. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/i.cs.hku.hk\/~bruno\/papers\/icfp2021.pdf\">Distributing intersection and union types with splits and duality (Functional pearl)<\/a>. ~ Xuejing Huang, Bruno C.D.S. Oliveira. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mally.stanford.edu\/Papers\/logicism.pdf\">A defense of logicism<\/a>. ~ Hannes Leitgeb, Uri Nodelman, Edward N. Zalta. #Logic #Math<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?LFMTP2021.1\">Facilitating meta-theory reasoning<\/a>. ~ Giselle Reis. #Logic #CompSci #SELLF #TATU #QUATI #OCaml #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?LFMTP2021.2\">Touring the MetaCoq project<\/a>. ~ Matthieu Sozeau. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?LFMTP2021.4\">Automating induction by reflection<\/a>. ~ Johannes Schoisswohl, Laura Kov\u00e1cs. #ATP #Logic<\/li>\n<li><a href=\"https:\/\/repositum.tuwien.at\/handle\/20.500.12708\/16472\">Automated induction by reflection<\/a>. ~ Johannes Schoisswohl. #MSc_Thesis #ATP #Logic<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?LFMTP2021.5\">Countability of inductive types formalized in the object-logic level<\/a>. ~ Qinxiang Cao, Xiwei Wu. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?LFMTP2021.6\">SMLtoCoq: Automated generation of Coq specifications and proof obligations from SML programs with contracts<\/a>. ~ Laila El-Beheiry, Giselle Reis, Ammar Karkour. #ITP #Coq #SML #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?LFMTP2021.7\">Systematic translation of formalizations of type theory from intrinsic to extrinsic style<\/a>. ~ Florian Rabe, Navid Roux. #MMT #LogicalFramework<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2107.07373\">A reinforcement learning environment for mathematical reasoning via program synthesis<\/a>. ~ Joseph Palermo, Johnny Ye, Alok Singh. #AI #MachineLearning #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2107.07045\">Explainable AI: current status and future directions<\/a>. ~ Prashant Gohel, Priyanka Singh, Manoranjan Mohanty. #XAI #AI #MachineLearning<\/li>\n<li><a href=\"https:\/\/cuddly-octo-palm-tree.com\/posts\/2021-07-11-cwafi-4\/\">Cheap interpreter, part 4: stack machines<\/a>. ~ Gary Verhaegen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.kalvad.com\/haskell-series-part-1\/\">Haskell series part 1<\/a>. ~ Pierre Guillemot. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.parsonsmatt.org\/2021\/07\/12\/template_haskell_performance_tips.html\">Template Haskell performance tips<\/a>. ~ Matt Parsons. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/libros.csic.es\/product_info.php?cPath=164&amp;products_id=1493&amp;PHPSESSID=ccd9b6102a86d43bb8272bb1de415d03\">Artificial Intelligence, Robotics &amp; Data Science (CSIC Scientific Challenges: Towards 2030, Volume 11)<\/a>. #AI #DataScience #MachineLearning<\/li>\n<li><a href=\"https:\/\/blog.desdelinux.net\/copilot-el-asistente-de-ai-de-github-recibio-fuertes-criticas-de-la-comunidad-open-source\">Copilot, el asistente de AI de GitHub recibi\u00f3 fuertes cr\u00edticas de la comunidad open source<\/a>. ~ Darkcrizt. #AI #Copilot #Programaci\u00f3n<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/careers\/253975-hrs-role-in-understanding-and-mitigating-ai-bias\/fulltext\">HR&#8217;s role in understanding and mitigating AI bias<\/a>. ~ Laura Baldwin. #AI<\/li>\n<li><a href=\"https:\/\/stopachka.essay.dev\/post\/5\/risp-in-rust-lisp\">(Risp (in (Rust) (Lisp)))<\/a>. ~ Stepan Parunashvili. #Rust #Lisp<\/li>\n<li><a href=\"https:\/\/www.fotonixx.com\/posts\/rust-fizzbuzz\/\">Writing an (overly) idiomatic Fizzbuzz with Rust<\/a>. ~ Ryan Frazier. #RustLang<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2007.00752\">Is Rust used safely by software developers?<\/a> ~ Ana Nora Evans, Bradford Campbell, Mary Lou Soffa. #RustLang<\/li>\n<li><a href=\"https:\/\/neptune.ai\/blog\/explainability-auditability-ml-definitions-techniques-tools\">Explainability and auditability in ML: Definitions, techniques, and tools<\/a>. ~ Ejiro Onose. #AI #MachineLearning #XAI<\/li>\n<li><a href=\"https:\/\/pure.tue.nl\/ws\/portalfiles\/portal\/174690614\/Final_thesis_Cottaar.pdf\">Reinforcement learning for interactive theorem proving (Creating an artificial student)<\/a>. ~ Jolijn Cottaar. #ITP #Coq #MachineLearning<\/li>\n<li><a href=\"https:\/\/is.muni.cz\/th\/zedur\/Game_development_in_Haskell_Archive.pdf\">Game development in Haskell<\/a>. ~ Jan Rychl\u00fd. #BSc_Thesis #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/frontdoor.php?source_opus=13914\">A mechanised proof of the time invariance thesis for the weak call-by-value \u03bb-calculus<\/a>. ~ Yannick Forster, Fabian Kunze, Gert Smolka, Maximilian Wuttke. #ITP #Coq #CompSci<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2107.06015\">A classification of artificial intelligence systems for mathematics education<\/a>. ~ Steven Van Vaerenbergh, Adri\u00e1n P\u00e9rez-Suay. #AI #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/XspZEqNl6Wo\">GHC: Dependency analysis of Haskell declarations<\/a>. ~ Artyom Kuznetsov. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Finitely_Generated_Abelian_Groups.html\">Finitely generated abelian groups (in Isabelle\/HOL)<\/a>. ~ Joseph Thommes, Manuel Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/perso.univ-rennes1.fr\/sebastien.gouezel\/articles\/gromov_hausdorff.pdf\">Formalizing the Gromov-Hausdorff space<\/a>. ~ S\u00e9bastien Gou\u00ebzel. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.xixilogic.org\/events\/wp-content\/uploads\/2021\/07\/proceedingsfinal.pd\">A flexible approach to argumentation framework analysis using theorem proving<\/a>. ~ David Fuenmayor, Alexander Steen.f#page=26 #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/matela.com.br\/express.pdf\">Express: Applications of dynamically typed Haskell expressions<\/a>. ~ Rudy Matela. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/link.springer.com\/article\/10.1007\/s40753-021-00140-1\">Learning about proof with the theorem prover Lean: the abundant numbers task<\/a>. ~ Athina Thoma, Paola Iannone. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.extrema.is\/articles\/haskell-books\">Haskell books: a tagged index of English books related to the Haskell programming language<\/a>. ~ Travis Cardwell. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2107.02353\">General automation in Coq through modular transformations<\/a>. ~ Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/14256\/%20\">Synthetic undecidability of MSELL via FRACTRAN mechanised in Coq<\/a>. ~ Dominique Larchey-Wendling. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/14260\/pdf\/LIPIcs-FSCD-2021-22.pdf\">Type-theoretic constructions of the final coalgebra of the finite powerset functor<\/a>. ~ Niccol\u00f2 Veltri. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2107.02354\">Alethe: Towards a generic SMT proof format<\/a>. ~ Hans-J\u00f6rg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine. #ATP #SMT<\/li>\n<li><a href=\"http:\/\/www.cse.chalmers.se\/~jomoa\/papers\/VPT21QuickSpec.pdf\">Conjectures, tests and proofs: An overview of theory exploration<\/a>. ~ Moa Johansson, Nicholas Smallbone. #Haskell #FunctionalProgramming #QuickSpec<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2107.02352\">A framework for proof-carrying logical transformations<\/a>. ~ Quentin Garchery. #FunctionalProgramming #OCaml #Why3<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007%2F978-3-030-79876-5.pd\">Isabelle\u2019s metalogic: Formalization and proof checker<\/a>. ~ Tobias Nipkow, Simon Ro\u00dfkopf.f#page=104 #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007%2F978-3-030-79876-5.pd\">Reliable reconstruction of fine-grained proofs in a proof assistant<\/a>. ~ Hans-J\u00f6rg Schurr, Mathias Fleury, Martin Desharnais.f#page=459 #ATP #SMT #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007%2F978-3-030-79876-5.pd\">The Isabelle\/Naproche natural language proof assistant<\/a>. ~ Adrian De Lon et als.f#page=619 #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/mathlib_docs\/computability\/turing_machine.html\">Turing machines in Lean<\/a>. ~ Mario Carneiro et als. #ITP #LeanProver #CompSci<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/blog\/2021-07-08-linear-traversable\/\">Exploring linear Traversable using generics<\/a>. ~ Sjoerd Visscher. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/bdtechtalks.com\/2021\/07\/05\/openai-github-gpt-3-copilot\/\">What OpenAI and GitHub\u2019s &#8220;AI pair programmer&#8221; means for the software industry<\/a>. ~ Ben Dickson. #AI #Programming #Copilot<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/news\/253847-using-ai-to-drill-down-in-physics\/fulltext\">Using AI to Drill Down in Physics<\/a>. ~ Bennie Mols. #AI<\/li>\n<li><a href=\"https:\/\/www.microsiervos.com\/archivo\/matematicas\/matematicas-dinamicas-visualizaciones-codigo-abierto.html\">Matem\u00e1ticas din\u00e1micas: estupendas visualizaciones a partir de c\u00f3digo abierto<\/a>. ~ @Alvy. #Matem\u00e1ticas #Computaci\u00f3n<\/li>\n<li><a href=\"https:\/\/www.dynamicmath.xyz\/\">Dynamic mathematics (Interactive mathematical applets &amp; animations)<\/a>. ~ Juan Carlos Ponce. #Math<\/li>\n<li><a href=\"https:\/\/raw.githubusercontent.com\/sofsanfer\/TFM\/main\/output\/document.pdf\">Formalizaci\u00f3n del teorema de existencia de modelo en Isabelle\/HOL<\/a>. ~ Sof\u0131\u0301a Santiago Fern\u00e1ndez. #TFM #ITP #IsabelleHOL #L\u00f3gica #Matem\u00e1tica<\/li>\n<li><a href=\"https:\/\/www.lix.polytechnique.fr\/iwc2021\/IWC2021_proceedings.pdf#page=29\">Formalized signature extension results for confluence, commutation and unique normal forms<\/a>. ~ A. Lochmann, F. Mitterwallner, A. Middeldorp. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/fitelson.org\/walsh.pdf\">Answers to some open questions of Ulrich &amp; Meredith<\/a>. ~ Matthew Walsh, Branden Fitelson. #ATP #Otter #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/SpecCheck.html?utm_source=dlvr.it&amp;utm_medium=twitter\">SpecCheck: Specification-based testing for Isabelle\/ML<\/a>. ~ Kevin Kappelmann, Lukas Bulwahn. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/media.suub.uni-bremen.de\/bitstream\/elib\/4986\/4\/Dissertation_Bornebusch.pdf\">Coq meets C\u03bbaSH (Proposing a hardware design synthesis flow that combines proof assistants with functional hardware description languages)<\/a>. ~ Fritjof Bornebusch. #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/utmsjoe.mk\/files\/Vol.12.No.1\/3.MODELS_FOR_SOFTWARE_VERIFICATION_PROVING_PROGRAM_CORRECTNESS.pdf\">Models for software verification: Proving program correctness<\/a>. ~ Boro Sitnikovski, Lidija Goracinova-Ilieva, Biljana Stojcevska. #FormalVerification #Coq #Dafny<\/li>\n<li><a href=\"http:\/\/ksiresearch.org\/seke\/seke21paper\/paper047.pdf\">Using LSTM to predict tactics in Coq<\/a>. ~ X. Luan, X. Zhang, M. Sun. #ITP #Coq #MachineLearning #NeuralNetwork<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2107.01883\">A theory of higher-order subtyping with type intervals<\/a>. ~ Sandro Stucki, Paolo G. Giarrusso. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/bit.ly\/3AO50OI\">Curry-Howard correspondence: An intuitive language for mathematics<\/a>. ~ Xiao Tan. #MSc_Thesis #Logic #CompSci<\/li>\n<li><a href=\"https:\/\/www.ams.org\/journals\/notices\/202106\/rnoti-p930.pdf\">Practical suggestions for mathematical writing<\/a>. ~ R. Bell, B. Kadets, P. Srinivasan, N. Triantafillou, I. Vogt. #Math<\/li>\n<li><a href=\"https:\/\/odr.chalmers.se\/bitstream\/20.500.12380\/302935\/1\/CSE%2021-74%20Engsmyre%20Wikstr%c3%b6m.pdf\">Complementing the digital programming tutor Ask-Elle with program synthesis<\/a>. ~ Gustav Engsmyre, Karl Wikstr\u00f6m. #MSc_Thesis #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/FredericLeRoux\/LEAN_ESPACES_METRIQUES\">Code Lean contenant les preuves d&#8217;un cours standard sur les espaces m\u00e9triques<\/a>. ~ Frederic Le Roux. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2021\/7\/5\/function-application-using-the-dollar-sign-\">Function application: Using the dollar sign ($)<\/a>. ~ James Bowen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/introduction-to-template-haskell\">A brief introduction to Template Haskell<\/a>. ~ Heitor Toledo Lassarote de Paula. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/news\/253785-will-ai-rewrite-coding\/fulltext\">Will AI rewrite coding?<\/a> ~ Samuel Greengard. #AI<\/li>\n<li><a href=\"https:\/\/exlean.org\/groups-i\/\">Groups I<\/a>. Omar Harhara. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.iiia.csic.es\/sat2021\/program\/Slides39.pdf\">Chinese remainder encoding for hamiltonian cycles [Slides<\/a>]. ~ Marijn Heule. #ATP #SATSolvers #Math<\/li>\n<li><a href=\"https:\/\/www.iiia.csic.es\/sat2021\/program\/Presentation39.mp4\">Chinese remainder encoding for hamiltonian cycles [Video<\/a>]. ~ Marijn Heule. #ATP #SATSolvers #Math<\/li>\n<li><a href=\"https:\/\/www.iiia.csic.es\/sat2021\/program\/Slides48.pdf%20\">DiMo: Discrete modelling using propositional logic [Slides<\/a>]. ~ Norbert Hundeshagen, Martin Lange and Georg Siebert. #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.iiia.csic.es\/sat2021\/program\/Presentation48.mp4\">DiMo: Discrete modelling using propositional logic [Video<\/a>]. ~ Norbert Hundeshagen, Martin Lange and Georg Siebert. #Logic #Math<\/li>\n<li><a href=\"https:\/\/dumbarton.fm.cs.uni-kassel.de\/assets\/manual\/DiMoManual_v0.2.2.pdf\">DiMo: A tool for discrete modelling using propositional logic (version 0<\/a>.2.2). ~ Martin Lange. #Logic #Math<\/li>\n<li><a href=\"https:\/\/repository.tudelft.nl\/islandora\/object\/uuid:989e34ff-c81f-43ba-a851-59dca559ab90\/datastream\/OBJ\/download\">Verifying correctness of Haskell programs using the programming language Agda and framework agda2hs<\/a>. ~ Dixit Sabharwal, Jesper G.H. Cockx, Lucas F.B. Escot. #ITP #Agda #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.itl.waw.pl\/czasopisma\/JTIT\/2021\/2\/107.pdf\">Security verification in the context of 5G sensor networks<\/a>. ~ Piotr Remlein, Urszula Stachowiak. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/repository.tudelft.nl\/islandora\/object\/uuid:5f308592-49ac-4395-985c-77f8c48a52f2\/datastream\/OBJ\/download\">Deriving a symbolic executor for definitional interpreters suitable for the study of heuristics<\/a>. ~ Laura-Ana P\u00eercalaboiu, Casper Bach Poulsen, Cas van der Rest. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/gopiandcode.uk\/logs\/log-certified-synthesis.html\">Goodbye C developers: The future of programming with certified program synthesis<\/a>. ~ Kiran Gopinathan. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/ilyasergey.net\/assets\/pdf\/papers\/certisuslik-icfp21.pdf\">Certifying the synthesis of heap-manipulating programs<\/a>. ~ Y. Watanabe, K. Gopinathan, George P\u00eerlea, Nadia Polikarpova, I. Sergey. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/costa.fdi.ucm.es\/wst2021\/WST2021_proceedings.pd\">Formalizing higher-order termination in Coq<\/a>. ~ Deivid Vale, Niels van der Weide.f#page=71 #ITP #Coq<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/hal-03274013\/document\">Formalization of a sign determination algorithm in real algebraic geometry<\/a>. ~ Cyril Cohen. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.cs.bham.ac.uk\/%7emhe\/agda-new\/CantorSchroederBernstein.html\">The Cantor-Schr\u00f6der-Bernstein for homotopy types, or \u221e-groupoids, in Agda<\/a>. ~ Martin Escardo. #ITP #Agda #Logic #Math<\/li>\n<li><a href=\"https:\/\/link.springer.com\/article\/10.1007\/s40062-021-00284-6\">The Cantor\u2013Schr\u00f6der\u2013Bernstein Theorem for \u221e-groupoids<\/a>. ~ Martin Escardo. #Logic #Math<\/li>\n<li><a href=\"https:\/\/repository.tudelft.nl\/islandora\/object\/uuid:2c32c354-42e4-466e-9869-b7c68b4388ec\/datastream\/OBJ\/download\">Practical verification of the Haskell ranged-sets library<\/a>. ~ Ioana Savu, Jesper Cockx, Lucas Escot. #ITP #Agda #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/repository.tudelft.nl\/islandora\/object\/uuid:065b9e87-43e5-4e3c-8e37-04f1b50c8cf7\/datastream\/OBJ\/download\">Producing a verified implementation of sequences using agda2hs<\/a>. ~ Shashank Anand, Jesper Cockx, Lucas Escot. #ITP #Agda #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/raw.githubusercontent.com\/barry-jay-personal\/tree-calculus\/master\/tree_book.pdf\">Reflective programs in tree calculus<\/a>. ~ Barry Jay. #eBook #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/barry-jay-personal\/tree-calculus\">Proofs in Coq for the book &#8220;Reflective programs in tree calculus&#8221;<\/a>. ~ Barry Jay. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/webspace.science.uu.nl\/~swier004\/publications\/2010-fundamentae-informatica.pdf\">A tutorial implementationof a dependently typed lambda calculus<\/a>. ~ Andres L\u00f6h, Conor McBride, Wouter Swierstra. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/youtu.be\/tYqbbRsx8DI\">Formalising contemporary mathematics in simple type theory<\/a>. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.12224v1\">Isabelle&#8217;s metalogic: Formalization and proof checker<\/a>. ~ Tobias Nipkow, Simon Ro\u00dfkopf. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/rpeszek.github.io\/posts\/2021-06-28-polysemy-arrows.html\">Arming polysemy with Arrows<\/a>. ~ Robert Peszek. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.jerf.org\/iri\/post\/2958\">Functors and monads for people who have read too many &#8220;Tutorials&#8221;<\/a>. ~ Jeremy Bowers. #Haskell #FunctionalProgramming<\/li>\n<\/ul>\n<\/div>\n<div id=\"postamble\" class=\"status\"><\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante julio de 2021, 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\/7609"}],"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=7609"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7609\/revisions"}],"predecessor-version":[{"id":7610,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7609\/revisions\/7610"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7609"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7609"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7609"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}