{"id":7611,"date":"2021-08-31T16:47:39","date_gmt":"2021-08-31T14:47:39","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7611"},"modified":"2021-08-31T16:47:39","modified_gmt":"2021-08-31T14:47:39","slug":"resumen-de-lecturas-compartidas-durante-agosto-de-2021","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-agosto-de-2021\/","title":{"rendered":"Resumen de lecturas compartidas durante agosto de 2021"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante agosto 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:\/\/bit.ly\/3DxZPnp\">New Software Foundations release<\/a>. ~ Benjamin C. Pierce et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2108.04194\">Modal logic S5 satisfiability in answer set programming<\/a>. ~ Mario Alviano,a Sotiris Batsakis, George Baryannis. #Logic #ASP #LogicProgramming<\/li>\n<li><a href=\"https:\/\/raw.githubusercontent.com\/BartoszMilewski\/Publications\/master\/TheDaoOfFP\/DaoFP.pdf\">The Dao of Functional Programming (Last updated: August 30, 2021)<\/a>. ~ Bartosz Milewski (@BartoszMilewski). #Haskell #FunctionalProgramming #CategoryTheory<\/li>\n<li><a href=\"https:\/\/youtube.com\/playlist?list=PLyrlk8Xaylp6_QTmXGuRe3lShaRGaMtgc\">HIW (The Haskell Implementors\u2019 Workshop) 2021 videos<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.ppig.org\/files\/2021-PPIG-32nd-tavante.pdf\">A data-centered user study for proof assistant tools<\/a>. ~ Hanneli C.A. Tavante. #ITP #Coq#LeanProver<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2108.11155\">Latent effects for reusable language components: Extended version<\/a>. ~ Birthe van den Berg, Tom Schrijvers, Casper Bach-Poulsen, Nicolas Wu. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.cs.kent.ac.uk\/people\/staff\/dao7\/publ\/timo-hope21.pdf\">Formalising algebraic effects with non-recoverable failure<\/a>. ~ Timotej Tomandl, Dominic Orchard. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/Mertcan-Temel\/publication\/354010466_Sound_and_Automated_Verification_of_Real-World_RTL_Multipliers\/links\/611ed85f169a1a01031224fd\/Sound-and-Automated-Verification-of-Real-World-RTL-Multipliers.pdf\">Sound and automated verification of real-world RTL multipliers<\/a>. ~ Mertcan Temel, Warren A. Hunt Jr. #ITP #ACL2<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2108.12301\">Computer algebra in Julia<\/a>. ~ Dmitry S. Kulyabov, Anna V. Korolkova. #CAS #JuliaLang #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/GhkoPskC3eY\">Dijkstra: O homem que tornou a computa\u00e7\u00e3o uma ci\u00eancia<\/a>. ~ Adriano Santos. #CompSci<\/li>\n<li><a href=\"https:\/\/katyhristova.medium.com\/what-is-category-theory-and-why-is-it-trendy-b94ce59fe42b\">What is category theory and why is it trendy?<\/a> ~ Katerina Hristova. #Math #CategoryTheory<\/li>\n<li><a href=\"https:\/\/youtu.be\/LwwzVpolxm8\">Geometry in Lean, a report for mathematicians<\/a>. ~ Nicol\u00f2 Cavalleri, Anthony Bordg. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/qac1O4Co0IU\">Formalizing the Gromov-Hausdorff space<\/a>. ~ S\u00e9bastien Gou\u00ebzel. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/ryanglscott.github.io\/2021\/08\/22\/leibniz-equality-in-haskell-part-1\/\">Leibniz equality in Haskell, part 1<\/a>. ~ Ryan Scott. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/leanpub.com\/magicalhaskell\">Magical Haskell (modern functional programming and type theory in a fun and accessible way)<\/a>. ~ Anton Antich. #Haskell #FunctionalProgramming #eBook<\/li>\n<li><a href=\"https:\/\/cdsmithus.medium.com\/nascent-ghc-proposal-source-rewrite-rules-and-optional-constraints-810a2f6051eb\">Nascent GHC proposal: Source rewrite rules and optional constraints<\/a>. ~ Chris Smith. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/news\/255113-life-as-a-logician\/fulltext\">Life as a logician (An interview with Martin Davis by Allyn Jackson)<\/a>. #Logic #Math #CompSci #AI #MachineLearning<\/li>\n<li><a href=\"https:\/\/youtu.be\/8P-X8YgsCZ0\">Une id\u00e9e assez folle, l&#8217;Intelligence Artificielle <\/a>\u2026 (un film sur le parcours d&#8217;Alain Colmerauer). #AI #LogicProgramming #Prolog<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2108.10868\">Towards formalising Schutz&#8217; axioms for Minkowski spacetime in Isabelle\/HOL<\/a>. ~ Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2108.10700\">Scalar actions in Lean&#8217;s mathlib<\/a>. ~ Eric Wieser. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/magazines\/2021\/9\/255036-ai-ethics\/fulltext\">AI ethics: A call to faculty<\/a>. ~ Illah Reza Nourbakhsh. #AI<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/c811dd774f9590e9106c0780ea0983c60b659c78\/src\/data\/nat\/mul_ind.lean\">Multiplicative induction principles for \u2115<\/a>. ~ Eric Rodriguez. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/OCQfkhqg8Yg\">Formalizing Fibonacci squares<\/a>. ~ Harun Khan. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/daemons.it\/posts\/programacion-literaria-para-sysadminsdevops\/\">Programaci\u00f3n literaria para sysadmins \/ devops<\/a>. ~ drymer. #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/www.ijcai.org\/proceedings\/2021\/0273.pdf\">Faster smarter proof by induction in Isabelle\/HOL<\/a>. ~ Yutaka Nagashima. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/15b1461951d8821c1354dcf01a89ce09e798965b\/archive\/imo\/imo2006_q3.lean\">Formalization in Lean of IMO 2006 Q3<\/a>. ~ Tian Chen. #ITP #LeanProver #Math #IMO<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2108.06944v1\">Verifying C11-style weak memory libraries via refinement<\/a>. ~ Sadegh Dalvandi, Brijesh Dongol. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/youtu.be\/wUUcuaegljk\">The design of mathematical language<\/a>. ~ Jeremy Avigad. #Logic #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/-uGhuknZHJI\">Verified optimization<\/a>. ~ Alexander Bentkamp, Jeremy Avigad. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/pudd4F749tE\">Automatically generalizing theorems using typeclasses<\/a>. ~ Alexander Best. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/github.com\/google\/formal-ml\">Formal ML: A LEAN library for proving foundational results in measure theory, probability, statistics, and machine learning, based upon mathlib<\/a>. #ITP #LeanProver #Math #MachineLearning<\/li>\n<li><a href=\"https:\/\/github.com\/RaitoBezarius\/berkovich-spaces\">Formalization of Ostrowski theorems in Lean theorem prover<\/a>. ~ Ryan Lahfad\u2020, Julien Marquet, Hadrien Barral. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2108.08079\">On correctness and completeness of an n queens program<\/a>. ~ W\u0142odzimierz Drabent. #LogicProgramming #Prolog<\/li>\n<li><a href=\"https:\/\/www.microsiervos.com\/archivo\/ia\/colisiones-matematicas-neuralhash.html\">Colisiones matem\u00e1ticas que muestran c\u00f3mo confundir al algoritmo Neural Hash<\/a>. ~ @Alvy. #AI #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2108.08009\">XAI methods for neural time series classification: A brief review<\/a>. ~ Ilija \u0160imi\u0107, Vedran Sabol, Eduardo Veas. #DeepLearning #XAI<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2108.07804\">A framework for understanding AI-induced field change: How AI technologies are legitimized and institutionalized<\/a>. ~ Benjamin Cedric Larsen. #AI<\/li>\n<li><a href=\"https:\/\/books.google.es\/books?id=DjM9EAAAQBAJ&amp;lpg=PP1&amp;pg=PP.1#v=onepage&amp;q&amp;f=true\">A first course in Artificial Intelligence<\/a>. ~ Osondu Oguike #eBook #AI<\/li>\n<li><a href=\"https:\/\/www.cantorsparadise.com\/machine-learning-and-the-continuum-hypothesis-87bb9bb23e90\">Machine learning and the continuum hypothesis (How the unprovable concerns the unlearnable)<\/a>. ~ Robert Passmann. #MachineLearning #Math<\/li>\n<li><a href=\"https:\/\/awakesecurity.com\/blog\/spectacle-a-language-for-writing-and-checking-formal-specifications-in-haskell\/\">Announcing Spectacle \u2013 A language for writing and checking formal specifications in Haskell<\/a>. ~ Jacob Leach. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/53d97e1ad2b5e30eff5f9246a689ec37361f63d0\/archive\/oxford_invariants\/2021summer\/week3_p1.lean\">The Oxford Invariants Puzzle Challenges (Summer 2021, Week 3, Problem 1) in Lean<\/a>. ~ Ya\u00ebl Dillies, Bhavik Mehta. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/books.google.es\/books?id=bhkSEAAAQBAJ&amp;lpg=PP1&amp;pg=PP1#v=onepage&amp;q&amp;f=true\">Ideas that created the future: Classic papers of Computer Science<\/a>. ~ Harry R. Lewis. #eBook #CompSci<\/li>\n<li><a href=\"https:\/\/gilmi.me\/blog\/post\/2021\/08\/14\/hs-core-tools\">Core Haskell tools<\/a>. ~ Gil Mizrahi. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/twobithistory.org\/2018\/10\/14\/lisp.html\">How Lisp became God&#8217;s own programming language<\/a>. ~ @TwoBitHistory. #Lisp #Programming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2108.06015\">Natural deduction calculus for first-order logic<\/a>. ~ Yazeed Alrubyli. #Logic #Math<\/li>\n<li><a href=\"https:\/\/easychair.org\/publications\/preprint\/RDH3\">Assimilating the structure of formal and informal proof<\/a>. ~ Kensho Tsurusaki, Akiko Aizawa. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/repositorio.inesctec.pt\/bitstream\/123456789\/12455\/1\/P-00V-35V.pdf\">Balancing the formal and the informal in user-centred design<\/a>. ~ JC Campos, MD Harrison, P Masci. #ITP #PVS<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2108.02995\">Extracting functional programs from Coq, in Coq<\/a>. ~ Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.cybok.org\/media\/downloads\/Formal_Methods_for_Security_v1.0.0.pdf\">Formal methods for security knowledge area<\/a>. ~ David Basin. #FormalMethods<\/li>\n<li><a href=\"https:\/\/publications.waset.org\/10012167\/haskellfl-a-tool-for-detecting-logical-errors-in-haskell\">HaskellFL: A tool for detecting logical errors in Haskell<\/a>. ~ Vanessa Vasconcelos, Mariza A. S. Bigonha. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/cdsmithus.medium.com\/abstraction-in-reflex-and-codeworld-a1b42ad36923\">Abstraction in Reflex and CodeWorld<\/a>. ~ Chris Smith. #Haskell #CodeWorld #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.cofree.coffee\/2021-08-13-that-one-cool-reader-trick\/\">That one cool reader trick<\/a>. ~ Solomon. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.haskellforall.com\/2021\/08\/namespaced-de-bruijn-indices.html\">Namespaced De Bruijn indices<\/a>. ~ Gabriella Gonzalez. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1801.00631\">Deep Learning: A critical appraisal<\/a>. ~ Gary Marcus. #DeepLearning<\/li>\n<li><a href=\"https:\/\/github.com\/conal\/talk-2018-deep-learning-rebooted\">A functional reboot for Deep Learning<\/a>. ~ Conal Elliott. #DeepLearning #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"http:\/\/conal.net\/papers\/language-derivatives\/\">Symbolic and automatic differentiation of languages<\/a>. ~ Conal Elliott. #Agda #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/alByz_LoANE\">What is the point of Lean&#8217;s maths library?<\/a> ~ Kevin Buzzard. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/vitez.me\/counting-cardinalities\">Counting cardinalities<\/a>. ~ Mitchell Vitez. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/adam.chlipala.net\/papers\/FrapICFP21\/FrapICFP21.pdf\">Skipping the binder bureaucracy with mixed embeddings in a semantics course (Functional Pearl)<\/a>. ~ Adam Chlipala. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/www.cs.ru.nl\/~wouters\/Publications\/HoareLogicStateMonad.pdf\">The Hoare State Monad (Proof Pearl)<\/a>. ~ Wouter Swierstra. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2021\/08\/11\/competitive-programming-in-haskell-monoidal-accumulation\/\">Competitive programming in Haskell: monoidal accumulation<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/master\/archive\/imo\/imo2001_q6.lean\">Formalization in Lean of IMO 2001 Q6<\/a>. ~ Sara D\u00edaz, Johan Commelin. #ITP #LeanProver #Math #IMO<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2108.01883v1\">Reasoning about iteration and recursion uniformly based on big-step semantics<\/a>. ~ Ximeng Li, Qianying Zhang, Guohui Wang, Zhiping Shi, Yong Guan. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/academiccommons.columbia.edu\/doi\/10.7916\/d8-3tsv-1117\/download\">A secure and formally verified commodity multiprocessor hypervisor<\/a>. ~ Shih-Wei Li. #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/master\/src\/data\/matrix\/kronecker.lean\">Kronecker product of matrices (in Lean)<\/a>. ~ Filippo A. E. Nuccio, Eric Wieser. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/malv.in\/posts\/2021-01-09-depth-first-and-breadth-first-search-in-haskell.html\">Depth-first and breadth-first search in Haskell<\/a>. ~ Malvin Gattinger. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.slideshare.net\/pjschwarz\/left-and-right-folds-comparison-of-a-mathematical-definition-and-a-programmatic-one-polyglot-fp-for-fun-and-profit-haskell-and-scala\">Left and right folds (Comparison of a mathematical definition and a programmatic one)<\/a>. ~ Philip Schwarz. #Haskell #Scala #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2108.03574\">Elementary recursive algorithms<\/a>. ~ Yiannis N. Moschovakis. #Algorithms #Logic #Math #CompSci<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2108.02995\">Extracting functional programs from Coq, in Coq<\/a>. ~ Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/synacktiv\/toy-wasm-symbexp\">A toy WASM symbolic interpreter<\/a>. ~ Simon Marechal et als. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Relational_Forests.html\">Relational forests (in Isabelle\/HOL)<\/a>. ~ Walter Guttmann. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.imperial.ac.uk\/media\/imperial-college\/faculty-of-engineering\/computing\/public\/2021-ug-projects\/Theorem-proving-with-classical-logic.pdf\">Theorem proving in classical logic<\/a>. ~ David Davies. #Haskell #FunctionalProgramming #Logic<\/li>\n<li><a href=\"https:\/\/easychair.org\/publications\/preprint_download\/KLfT\">Automatically generalizing theorems using typeclasses<\/a>. ~ Alex J. Best. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/blog.cofree.coffee\/2021-08-05-a-brief-intro-to-monad-transformers\/\">A brief intro to monad transformers<\/a>. ~ Solomon. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2108.00484\">Elements of differential geometry in Lean: A report for mathematicians<\/a>. ~ Anthony Bordg, Nicol\u00f2 Cavalleri. #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?FIDE2021.6\">Plotting in a formally verified way<\/a>. ~ Guillaume Melquiond. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.edukera.com\/\">Edukera: Teach Logic and Math with a proof assistant<\/a>. #ITP #Coq #Edukera #Logic #Math<\/li>\n<li><a href=\"https:\/\/medium.com\/coinmonks\/archetype-a-dsl-for-tezos-6f55c92d1035\">Archetype, a DSL for Tezos<\/a>. ~ Benoit Rognier. #ITP #Coq #Edukera #Archetype<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?FIDE2021.7\">A logic theory pattern for linearized control systems<\/a>. ~ Andrea Domenici, Cinzia Bernardeschi. #ITP #PVS<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?FIDE2021.9\">Verifying time complexity of binary search using Dafny<\/a>. ~ Shiri Morshtein, Ran Ettinger, Shmuel Tyszberowicz. #ATP #FormalVerification #Dafny<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?FIDE2021.10\">Explaining counterexamples with giant-step assertion checking<\/a>. ~ Benedikt Becker, Cl\u00e1udio Belo Louren\u00e7o, Claude March\u00e9. #ATP #Why3 #FormalVerification<\/li>\n<li><a href=\"https:\/\/arxiv.org\/html\/2108.02369v1\">VeriFly: On-the-fly assertion checking with CiaoPP (extended abstract)<\/a>. ~ Miguel A. Sanchez-Ordaz, Isabel Garcia-Contreras, V\u00edctor P\u00e9rez, Jose F. Morales, Pedro Lopez-Garcia, Manuel V. Hermenegildo.\/#EPTCS338.13 #Prolog #CiaoPP<\/li>\n<li><a href=\"https:\/\/blog.noredink.com\/post\/658510851000713216\/haskell-for-the-elm-enthusiast\">Haskell for the Elm enthusiast<\/a>. ~ No Red Ink. #Haskell #Elm #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blog.kalvad.com\/haskell-series-part-2\/\">Haskell series part 2 (This is the second article of a series on the functional language Haskell for beginners)<\/a>. ~ Pierre Guillemot. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/danso.ca\/blog\/frommaybe-is-just-a-fold\/\">fromMaybe is Just a fold<\/a>. ~ Dan Soucy. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/antitypical.com\/posts\/2021-07-28-when-howard-met-curry\/\">When Howard Met Curry<\/a>. ~ Rob Rix. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/project-archive.inf.ed.ac.uk\/msc\/20204462\/msc_proj.pdf\">Axiomatic Minkowski spacetime in Isabelle\/HOL<\/a>. ~ Richard Schmoetten. #MSc_Thesis #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/afp.theoremproving.org\/\">Archive of Formal Proofs<\/a>. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/github.com\/carlinmack\/afp\">Archive of Formal Proofs redesign<\/a>. ~ Carlin MacKenzie. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/github.com\/FrickHazard\/thomaes-function\">Lean proof of Thomaes (popcorn) function<\/a>. ~ Ender Doe. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/9789811236488_0001\">Proof and computation: Perspectives for mathematics, computer science, and philosophy<\/a>. ~ Klaus Mainzer. #Logic #Math #CompSci #ITP<\/li>\n<li><a href=\"https:\/\/www.cs.purdue.edu\/homes\/bendy\/OADT\/oadt.pdf\">Oblivious Algebraic Data Types<\/a>. ~ Qianchuan Ye, Benjamin Delaware. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/ryanglscott.github.io\/2021\/08\/01\/equality-constraints-in-kinds\/\">GHC curiosities: Equality constraints in kinds<\/a>. ~ Ryan Scott. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.philipzucker.com\/egglog2-monic\/\">Egglog 2: Automatically proving the pullback of a monic is monic<\/a>. ~ Philip Zucke. #CategoryTheory<\/li>\n<li><a href=\"http:\/\/www.wouterspekkink.org\/academia\/writing\/tool\/doom-emacs\/2021\/02\/27\/writing-academic-papers-with-org-mode.html\">Writing academic papers with org-mode<\/a>. ~ Wouter Spekkink. #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/morrowm.github.io\/posts\/2021-08-02-shoes.html\">Tying shoes with GADTs<\/a>. ~ MorrowM. #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 agosto 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\/7611"}],"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=7611"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7611\/revisions"}],"predecessor-version":[{"id":7612,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7611\/revisions\/7612"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7611"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7611"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7611"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}