{"id":8184,"date":"2024-05-04T09:14:45","date_gmt":"2024-05-04T07:14:45","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8184"},"modified":"2024-05-04T09:14:45","modified_gmt":"2024-05-04T07:14:45","slug":"04-may-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/04-may-24\/","title":{"rendered":"Resumen de lecturas compartidas durante abril de 2024"},"content":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante abril de 2024, en <a href=\"https:\/\/mathstodon.xyz\/@Jose_A_Alonso\">Mastodon<\/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:\/\/mathstodon.xyz\/@Jose_A_Alonso\">Mastodon<\/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:\/\/arxiv.org\/abs\/2402.10494\">Mechanised uniform interpolation for modal logics K, GL, and iSL<\/a>. ~ Hugo F\u00e9r\u00e9e, Iris van der Giessen, Sam van Gool, Ian Shillito. #ITP #Coq #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2212.09570\">Solving quantified modal logic problems by translation to classical logics<\/a>. ~ Alexander Steen, Geoff Sutcliffe, Christoph Benzm\u00fcller. #ATP #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.18067\">Type inference for Isabelle2Cpp<\/a>. ~ Dongchen Jiang, Chenxi Fu. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.philipzucker.com\/sqrt2\/\">Experiments in the irrationality of Sqrt 2 with SMT<\/a>. ~ Philip Zucker (@sandmouth@types.pl). #ATP #SMT #Math<\/li>\n<li><a href=\"https:\/\/formalweb3.uibk.ac.at\/docs\/24\/kajjck-lpar24.pdf\">Prover9 unleashed: Automated configuration for enhanced proof discovery<\/a>. ~ Kristina Aleksandrova, Jan Jakubuv, Cezary Kaliszyk. #ATP #Prover9<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/ghc-dependent-types-in-haskell-3\">Serokell\u2019s Work on GHC: Dependent types, Part 3<\/a>. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0097316524000438\">The number of primitive words of unbounded exponent in the language of an HD0L-system is finite<\/a>. ~ Karel Klouda, \u0160t\u011bp\u00e1n Starosta. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.14223\">Error credits: Resourceful reasoning about error bounds for higher-order probabilistic programs<\/a>. ~ Alejandro Aguirre et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.14069\">On the systematic creation of faithfully rounded commutative truncated booth multipliers<\/a>. ~ Theo Drane, Samuel Coward, Mertcan Temel, Joe Leslie-Hurd. #ITP #ACL2<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.14919\">Stalnaker&#8217;s epistemic logic in Isabelle\/HOL<\/a>. ~ Laura P. Gamboa Guzman, Kristin Y. Rozier. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.15214\">Embedding differential dynamic logic in PVS<\/a>. ~ J. Tanner Slagel, Mariano Moscato, Lauren White, C\u00e9sar A. Mu\u00f1oz, Swee Balachandran, Aaron Dutle. #ITP #PVS<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.14920\">Formalizing factorization on euclidean domains and abstract euclidean algorithms<\/a>. ~ Thaynara Arielly de Lima, Andr\u00e9ia Borges Avelar, Andr\u00e9 Luiz Galdino, Mauricio Ayala-Rinc\u00f3n. #ITP #PVS #Math<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/research\/computing-education-in-the-era-of-generative-ai\/\">Computing education in the era of generative AI<\/a>. ~ Paul Denny et als. #AI #Education<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/367962741_Human-machine_collaboration_in_the_teaching_of_proof\">Human-machine collaboration in the teaching of proof<\/a>. ~ Gila Hanna, Brendan Larvor, Xiaoheng Kitty Yan. #ITP #Lean4 #Math<\/li>\n<li><a href=\"https:\/\/liberabaci.gitlabpages.inria.fr\/\">LiberAbaci: Teaching mathematics with the help of Coq<\/a>. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/adabeat.com\/fp\/benefits-of-functional-programming\/\">Benefits of functional programming<\/a>. ~ Ada Beat. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.math.ias.edu\/avi\/book\">Mathematics and computation<\/a>. ~ Avi Wigderson. #eBook #Math #CompSci<\/li>\n<li><a href=\"https:\/\/link.springer.com\/article\/10.1007\/s11858-024-01577-9\">Using the proof assistant Lean in undergraduate mathematics classrooms<\/a>. ~ Brendan Larvor, Gila Hanna, Xiaoheng Yan. #ITP #Lean4 #Math<\/li>\n<li><a href=\"https:\/\/inria.hal.science\/hal-04550762\/document\">Teaching divisibility and binomials with Coq<\/a>. ~ Sylvie Boldo, Fran\u00e7ois Cl\u00e9ment, David Hamelin, Micaela Mayero, Pierre Rousselin. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/dwrensha.github.io\/compfiles\/\">Compfiles: Catalog of math problems formalized in Lean<\/a>. ~ David Renshaw (@david@social.wub.site) et als. #ITP #Lean4 #Math #IMO<\/li>\n<li><a href=\"https:\/\/lean-ja.github.io\/lean99\/\">Lean 99: Ninety-nine Lean problems<\/a>. ~ Kitamado. #FunctionalProgramming #Lean4<\/li>\n<li><a href=\"https:\/\/cs-syd.eu\/posts\/2024-04-20-static-linking-haskell-nix\">Getting your Haskell executable statically linked with Nix<\/a>. ~ Tom Sydney Kerckhove. #FunctionalProgramming #Haskell #Nix<\/li>\n<li><a href=\"https:\/\/oleg.fi\/gists\/posts\/2024-04-21-a-note-about-coercions.html\">A note about coercions<\/a>. ~ Oleg Grenrus (@phadej). #FunctionalProgramming #ITP #Agda<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.11638\">Chain Bounding and the leanest proof of Zorn&#8217;s lemma<\/a>. ~ Guillermo L. Incatasciato, Pedro S\u00e1nchez Terraf. #ITP #Lean4 #Math<\/li>\n<li><a href=\"https:\/\/hal.science\/hal-04546712\/document\">Formalization of derived categories in Lean\/mathlib<\/a>. ~ Jo\u00ebl Riou. #ITP #Lean4 #Math #CategoryTheory<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-031-57853-3_17\">Effective parallel formal verification of reconfigurable discrete-event systems formalizing with Isabelle\/HOL<\/a>. ~ Sohaib Soualah, Mohamed Khalgui &amp; Allaoua Chaoui. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.10952\">Can language models solve olympiad programming?<\/a> ~ Quan Shi et als. #LLMs #Programming<\/li>\n<li><a href=\"https:\/\/hai.stanford.edu\/news\/ai-index-state-ai-13-charts\">AI index: State of AI in 13 charts<\/a>. ~ Shana Lynch. #AI<\/li>\n<li><a href=\"https:\/\/outsiderart.substack.com\/p\/cyc-historys-forgotten-ai-project\">Cyc: history&#8217;s forgotten AI project<\/a>. ~ I. A. Fisher. #AI<\/li>\n<li><a href=\"https:\/\/doi.org\/10.1016\/j.apal.2024.103413\">The formal verification of the ctm approach to forcing<\/a>. ~ Emmanuel Gunther et als. #ITP #Isabelle #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/MFOTL_Checker.html\">A verified proof checker for metric first-order temporal logic<\/a>. ~ Andrei Herasimau, Jonathan Julian Huerta y Munive, Leonardo Lima, Martin Raszyk, Dmitriy Traytel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/llm4code.github.io\/assets\/pdf\/papers\/5.pdf\">Applying large language models to enhance the assessment of parallel functional programming assignments<\/a>. ~ Skyler Grandel, Douglas C. Schmidt, Kevin Leach. #FunctionalProgramming #LLMs #ChatGPT<\/li>\n<li><a href=\"https:\/\/terrytao.wordpress.com\/2024\/04\/19\/two-announcements-ai-for-math-resources-and-erdosproblems-com\/\">Two announcements: AI for Math resources, and erdosproblems.com<\/a>. ~ Terence Tao (@tao@mathstodon.xyz). #AI #Math<\/li>\n<li><a href=\"https:\/\/hbr.org\/2024\/04\/why-engineers-should-study-philosophy\">Why engineers should study Philosophy<\/a>. ~ Marco Argenti. #AI #Philosophy<\/li>\n<li><a href=\"https:\/\/oleg.fi\/gists\/posts\/2024-04-12-core-inspection.html\">Core inspection<\/a>. ~ Oleg Grenrus. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/jackkelly.name\/blog\/archives\/2024\/04\/13\/why_streaming_is_my_favourite_haskell_streaming_library\/index.html\">Why streaming is my favourite Haskell streaming library<\/a>. ~Jack Kelly. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.08163\">ViCAR: Visualizing categories with automated rewriting in Coq<\/a>. ~ Bhakti Shah et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.12048\">Symbolic computation for all the fun<\/a>. ~ Chad E. Brown, Mikol\u00e1\u0161 Janota, Mirek Ol\u0161\u00e1k. #AIMO #ATP #SMT #Math<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-45784-5.pd\">Towards a certified proof checker for deep neural network verification<\/a>. ~ Remi Desmartin et als.f#page=203 #ITP #Imandra #DeepLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.09939\">A survey on deep learning for theorem proving<\/a>. ~ Zhaoyu Li et als. #ITP #DeepLearning<\/li>\n<li><a href=\"https:\/\/mpaviotti.github.io\/assets\/papers\/intro-cat24.pdf\">Category theory (Course notes)<\/a>. ~ Domini Corchard, Marco Paviotti. #CategoryTheory<\/li>\n<li><a href=\"https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1570866706000311\">Exact arithmetic on the Stern\u2013Brocot tree<\/a>. ~ Milad Niqui (2007). #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/www.youtube.com\/live\/ksW04Cl2dgo\">The Haskell Unfolder Episode 23: specialisation<\/a>. ~ Edsko de Vries (@EdskoDeVries), Andres L\u00f6h (@kosmikus@functional.cafe). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/jmc.stanford.edu\/articles\/lisp\/lisp.pdf\">History of Lisp<\/a>. ~ John McCarthy (1979). #Lisp<\/li>\n<li><a href=\"https:\/\/the-algorithms.com\">The algorithms (Open source resource for learning data structures &amp; algorithms and their implementation in any programming language)<\/a>. ~ @The_Algorithms. #Algorithms #Programming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.09033\">Logic in mathematics and computer science<\/a>. ~ Richard Zach (@rrrichardzach@mathstodon.xyz). #Logic #Math #CompSci<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-031-57246-3_17\">IsaRare: Automatic verification of SMT rewrites in Isabelle\/HOL<\/a>. ~ Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres N\u00f6tzli, Clark Barrett &amp; Cesare Tinelli. #ITP #IsabelleHOL #SMT<\/li>\n<li><a href=\"https:\/\/math.hawaii.edu\/~bjoern\/Protein-ICMS.pdf\">Protein folding by recursive backtracking<\/a>. ~ Bj\u00f8rn Kjos-Hanssen. #ITP #Lean4<\/li>\n<li><a href=\"https:\/\/samuelgruetter.net\/assets\/liveverif-camera-ready-2024-04-06.pdf\">Live verification in an interactive proof assistant<\/a>. ~ Samuel Gruetter, Viktor Fukala, Adam Chlipala. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-031-57246-3_21\">A state-of-the-art Karp-Miller algorithm certified in Coq<\/a>. ~ Thibault Hilaire, David Ilcinkas &amp; J\u00e9r\u00f4me Leroux. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/samuelgruetter.net\/assets\/garagedoor-camera-ready-2024-04-06.pdf\">Foundational integration verification of a cryptographic server<\/a>. ~ Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Cl\u00e9ment Pit-Claudel &amp; Adam Chlipala. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/cr.yp.to\/papers\/latticeasymp-20240413.pdf\">Asymptotics for the standard block size in primal lattice attacks: second order, formally verified<\/a>. ~ Daniel J. Bernstein. #ITP #HOL_Light<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-42753-4.pd\">Large-scale formal proof for the working mathematician (lessons learnt from the ALEXANDRIA project)<\/a>. ~ Lawrence C. Paulson.f#page=17 #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-42753-4.pd\">Evasiveness through Binary Decision Diagrams<\/a>. ~ Jes\u00fas Aransay, Laureano Lamb\u00e1n, Julio Rubio.f#page=49 #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-42753-4.pd\">Category theory in Isabelle\/HOL as a basis for meta-logical investigation<\/a>. ~ Jonas Bayer, Alexey Gonus, Christoph Benzm\u00fcller, Dana S. Scott.f#page=81 #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-42753-4.pd\">Isabelle formalisation of original representation theorems<\/a>. ~ Marco B. Caminati.f#page=110 #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-42753-4.pd\">Formalization quality in Isabelle<\/a>. ~ Fabian Huch, Yiannos Stathopoulos.f#page=154 #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-031-42753-4_11\">Formalizing free groups in Isabelle\/HOL: The Nielsen-Schreier theorem and the conjugacy problem<\/a>. ~ Aabid Seeyal Abdul Kharim et als. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-031-42753-4_14\">Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method<\/a>. ~ Mohit Tekriwal et als. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-031-42753-4_15\">Multiple-inheritance hazards in dependently-typed algebraic hierarchies<\/a>. ~ Eric Wieser. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-42753-4.pd\">Nominal AC-matching<\/a>. ~ Mauricio Ayala-Rinc\u00f3n et als.f#page=65 #ITP #PVS<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-031-42753-4_16\">CoProver: A recommender system for proof construction<\/a>. ~ Eric Yeh, Briland Hitaj, Sam Owre, Maena Quemener, Natarajan Shankar. #ITP #PVS<\/li>\n<li><a href=\"https:\/\/youtube.com\/playlist?list=PLy5PZQDDJeY3pGUeIo2rVQJH4txKDmMZ4&amp;si=gk9Wv3kzhbusUen4\">From foundations to frontiers: Mastering Haskell programming<\/a>. ~ Byte Sorcery. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/docs.google.com\/document\/d\/1kD7H4E28656ua8jOGZ934nbH2HcBLyxcRgFDduH5iQ0\">AI for Math resources<\/a>. ~ Talia Ringer et als. #AI #Math<\/li>\n<li><a href=\"https:\/\/substack.com\/inbox\/post\/143505428\">Reimagining middle school education: The synergy of AI and Montessori principles (Next-level AI curriculum development)<\/a>. ~ Nick Potkalitsky, Sam Bobo. #AI #Education<\/li>\n<li><a href=\"https:\/\/www.tcs.ifi.lmu.de\/lehre\/ss-2024\/itp_de.html\">Course: Interactive theorem proving<\/a>. ~ Jasmin Blanchette et als. #ITP #Lean4<\/li>\n<li><a href=\"https:\/\/seasawher.github.io\/mathlib4-tactics\/\">Mathlib4 tactics<\/a>. ~ Kitamado. #ITP #Lean4 #Mathlib<\/li>\n<li><a href=\"https:\/\/essay.utwente.nl\/98665\/1\/Veen_van_der_MA_EEMCS.pdf\">A formal proof for the correctness of tangle learning<\/a>. ~ Suzanne Ellen van der Veen. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.cambridge.org\/core\/journals\/journal-of-functional-programming\/article\/knuthmorrispratt-illustrated\/8EFA77D663D585B68630E372BCE1EBA4\">Knuth\u2013Morris\u2013Pratt illustrated<\/a>. ~ Cameron Moy. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.cambridge.org\/core\/journals\/journal-of-functional-programming\/article\/asymptotic-speedup-via-effect-handlers\/296879DE2FD96FB6CF388F27978C76E4\">Asymptotic speedup via effect handlers<\/a>. ~ Daniel Hillerstr\u00f6m, Sam Lindley, John Longley. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.06405\">Wu&#8217;s method can boost symbolic AI to rival silver medalists and AlphaGeometry to outperform gold medalists at IMO geometry<\/a>. ~ Shiven Sinha et als. #AI #ATP #IMO #Math<\/li>\n<li><a href=\"https:\/\/charlesaverill.github.io\/ctpe\/\">Coq tactics in plain english<\/a>. ~ Charles Averill. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/charlesaverill.github.io\/teaching\/fpv_cyberfest23.pdf\">Formal program verification (Rigorous proof of program correctness and security)<\/a>. ~ Charles Averill. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.unwoundstack.com\/blog\/ob-coq.html\">Ann: ob-coq (A package for Coq developments in Org Mode)<\/a>. ~ Michael Herstine (@unwoundstack). #ITP #Coq #Emacs #OrgMode<\/li>\n<li><a href=\"https:\/\/youtu.be\/oG4qVQpCeDQ\">Dyadic Decomposition using Functional lenses<\/a>. ~ Eduardo Lemos. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/abhinavsarkar.net\/posts\/compiling-aoc23-aplenty\/\">Solving Advent of Code \u201923 \u201cAplenty\u201d by Compiling<\/a>. ~ Abhinav Sarkar (@abnv@fantastic.earth). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/tspace.library.utoronto.ca\/bitstream\/1807\/138077\/1\/Wu_Yuhuai_202403_PhD_thesis.pdf\">Neural networks for mathematical reasoning: Evaluations, capabilities, and techniques<\/a>. ~ Yuhuai Tony Wu. #NeuralNetwork #Reasoning #Math<\/li>\n<li><a href=\"https:\/\/www.semanticscholar.org\/api-gallery\/epsilon\">Epsilon: Scientific research at your fingertips (Epsilon uses AI to answer research questions with academic literature)<\/a>. #AI<\/li>\n<li><a href=\"https:\/\/youtu.be\/5Ml7AcaY8DE\">The mathematics of Prolog<\/a>. ~ David S Warren. #Prolog #LogicProgramming #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.06477\">Mechanised hypersafety proofs about structured data: extended version<\/a>. ~ Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, Ilya Sergey. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.05458\">Teaching higher-order logic using Isabelle<\/a>. ~ Simon Tobias Lund, J\u00f8rgen Villadsen. #ITP #IsabelleHOL #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.05462\">Interactive formal specification for mathematical problems of engineers<\/a>. ~ Walther Neuper. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Uncertainty_Principle.html\">Uncertainty principle (in Isabelle\/HOL)<\/a>. ~ Alexander Treml. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/aws.amazon.com\/es\/blogs\/opensource\/lean-into-verified-software-development\/\">Lean into verified software development<\/a>. ~ Kesha Hietala, Emina Torlak. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.05459\">A Coq library of sets for teaching denotational semantics<\/a>. ~ Qinxiang Cao, Xiwei Wu, Yalun Liang. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2403.14606\">The elements of differentiable programming<\/a>. ~ Mathieu Blondel, Vincent Roulet. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.05213\">Evaluation of an LLM in identifying logical fallacies: A call for rigor when adopting LLMs in HCI research<\/a>. ~ Gionnieve Lim, Simon T. Perrault. #LLMs #Reasoning #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.04293\">Reason from fallacy: Enhancing large language models&#8217; logical reasoning through logical fallacy understanding<\/a>. ~ Yanda Li et als. #LLMs #Reasoning #Logic<\/li>\n<li><a href=\"https:\/\/tusharhero.codeberg.page\/creating_a_blog.html\">Creating a blog<\/a>. #Emacs #OrgMode #Blog<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-031-57259-3_1\">From mechanized semantics to verified compilation: the Clight semantics of CompCert<\/a>. ~ Sandrine Blazy. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-031-57249-4_11\">A comprehensive specification and verification of the L4 microkernel API<\/a>. ~ Leping Zhang, Yongwang Zhao, Jianxin Li. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.03614v1\">Towards trustworthy automated program verifiers: Formally validating translations into an intermediate verification language<\/a>. ~ Gaurav Parthasarathy et als. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/link.springer.com\/chapter\/10.1007\/978-3-031-57262-3_4\">Program synthesis from graded types<\/a>. ~ Jack Hughes, Dominic Orchard. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/staff.aist.go.jp\/reynald.affeldt\/documents\/cs2024_preprint.pdf\">The Radon-Nikod\u00fdm theorem and the Lebesgue-Stieltjes measure in Coq<\/a>. ~ Yoshihiro Ishiguro, Reynald Affeldt. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.01234\">GFLean: An autoformalisation framework for Lean via GF<\/a>. ~ Shashank Pathak. #Lean #Autoformalization #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/taylor.fausak.me\/2024\/03\/31\/alias-current-module\/\">Alias the current module with Imp<\/a>. ~ Taylor Fausak. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/oleg.fi\/gists\/posts\/2024-04-01-implicit-arguments.html\">Implicit arguments<\/a>. ~ Oleg Grenrus. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.mat.unb.br\/~ayala\/CompactnessAndApplications.pdf\">Combinatorial applications of the compactness theorem<\/a>. ~ Fabi\u00e1n Fernando Serrano Su\u00e1rez, Mauricio Ayala-Rinc\u00f3n, Thaynara Arielly de Lima. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/www.mat.unb.br\/~ayala\/Certified_AC_Unification_Algorithm.pdf\">Certified first-order AC-unification and applications<\/a>. ~ Mauricio Ayala-Rinc\u00f3n et als. #ITP #PVS<\/li>\n<li><a href=\"https:\/\/people.cs.aau.dk\/~andsch\/SAC2024.pdf\">Isabelle-verified correctness of Datalog programs for program analysis<\/a>. ~ Anders Schlichtkrull, Ren\u00e9 Rydhof Hansen, Flemming Nielson. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/github.com\/haruhisa-enomoto\/mathlib4-all-tactics\/blob\/main\/all-tactics.md\">All tactics in mathlib4<\/a>. ~ Haruhisa Enomoto. #ITP #LeanProver #Mathlib<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Broadcast_Psi.html\">Broadcast Psi-calculi (in Isabelle\/HOL)<\/a>. ~ Palle Raabjerg, Johannes \u00c5man Pohjola, Tjark Weber. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2403.12627\">Enhancing formal theorem proving: A comprehensive dataset for training AI models on Coq code<\/a>. ~ Andreas Florath. #ITP #Coq #LLMs<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2303.17513\">Improving the Diproche CNL through autoformalization via Large Language Models<\/a>. ~ Merlin Carl. #ITP #Diproche #LLMs<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2404.01761\">A formal proof of R(4,5)=25<\/a>. ~ Thibault Gauthier, Chad E. Brown. #ITP #HOL4 #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2304.06186\">Using large language models for (de-)formalization and natural argumentation exercises for beginner&#8217;s students<\/a>. ~ Merlin Carl. #LLMs #Autoformalization #Logic<\/li>\n<li><a href=\"https:\/\/terrytao.wordpress.com\/2024\/04\/02\/ai-mathematical-olympiad-progress-prize-competition-now-open\/\">AI Mathematical Olympiad \u2013 Progress Prize Competition now open<\/a>. ~ Terence Tao (@tao@mathstodon.xyz). #AI #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/tHh9zjNazz4\">Generative logic, teaching Prolog in art &amp; design<\/a>. ~ Christian Jendreiko. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/www.philipzucker.com\/resolution1\/\">Resolution proving I<\/a>. ~ Philip Zucker (@sandmouth@types.pl). #Logic #ATP #Python<\/li>\n<li><a href=\"https:\/\/enpc.hal.science\/hal-03315809\/\">Conditional separation as a binary relation<\/a>. A Coq assisted proof. ~ Jean-Philippe Chancelier, Michel de Lara , Benjamin Heymann. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.ams.org\/journals\/bull\/0000-000-00\/S0273-0979-2024-01827-8\/S0273-0979-2024-01827-8.pdf%20Math\">How machines can make mathematics more congressive<\/a>. ~ Eugenia Cheng. #CompSci<\/li>\n<li><a href=\"https:\/\/www.ams.org\/journals\/bull\/0000-000-00\/S0273-0979-2024-01834-5\/S0273-0979-2024-01834-5.pdf\">Some thoughts on automation and mathematical research<\/a>. ~ Akshay Venkatesh. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/www.ams.org\/journals\/bull\/0000-000-00\/S0273-0979-2024-01828-X\/S0273-0979-2024-01828-X.pdf\">Mathematics, word problems, common sense, and artificial intelligence<\/a>. ~ Ernest Davis. #Math #AI #LLMs #GPT<\/li>\n<li><a href=\"https:\/\/www.ams.org\/journals\/bull\/0000-000-00\/S0273-0979-2024-01831-X\/S0273-0979-2024-01831-X.pdf\">Abstraction boundaries and spec driven development in pure mathematics<\/a>. ~ Johan Commelin, Adam Topaz. #Math #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/www.ams.org\/journals\/bull\/0000-000-00\/S0273-0979-2024-01830-8\/S0273-0979-2024-01830-8.pdf\">Strange new universes: Proof assistants and synthetic foundations<\/a>. ~ Michael Shulman. #Math #ITP #LLMs<\/li>\n<li><a href=\"https:\/\/www.ams.org\/journals\/bull\/0000-000-00\/S0273-0979-2024-01833-3\/S0273-0979-2024-01833-3.pdf\">Mathematical reasoning and the computer<\/a>. ~ Kevin Buzzard. #Math #AI #NeuralNetwork #LLMs #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/www.ams.org\/journals\/bull\/0000-000-00\/S0273-0979-2024-01825-4\/S0273-0979-2024-01825-4.pdf\">Automation compels mathematicians to reflect on our values<\/a>. ~ Michael Harris. #Math #AI<\/li>\n<li><a href=\"https:\/\/www.ams.org\/journals\/bull\/0000-000-00\/S0273-0979-2024-01829-1\/S0273-0979-2024-01829-1.pdf\">Is deep learning a useful tool for the pure mathematician?<\/a> ~ Geordie Williamson. #Math #AI #DeepLearning<\/li>\n<li><a href=\"https:\/\/www.ams.org\/journals\/bull\/0000-000-00\/S0273-0979-2024-01832-1\/S0273-0979-2024-01832-1.pdf\">Mathematics and the formal turn<\/a>. ~ Jeremy Avigad. #Math #AI #ITP #MachineLearning<\/li>\n<li><a href=\"https:\/\/www.ams.org\/journals\/bull\/0000-000-00\/S0273-0979-2024-01826-6\/S0273-0979-2024-01826-6.pdf\">Proof in the time of machines<\/a>. ~ Andrew Granville. #Math #ITP<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante abril de 2024, en Mastodon fundamentalmente sobre programaci\u00f3n funcional y demostraci\u00f3n asistida por ordenador. Las lecturas est\u00e1n ordenadas seg\u00fan su fecha de publicaci\u00f3n en Mastodon. 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":"default","_kad_post_title":"default","_kad_post_layout":"default","_kad_post_sidebar_id":"","_kad_post_content_style":"default","_kad_post_vertical_padding":"default","_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":[1],"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\/8184"}],"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=8184"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8184\/revisions"}],"predecessor-version":[{"id":8185,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8184\/revisions\/8185"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8184"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8184"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8184"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}