{"id":7607,"date":"2021-07-01T19:35:23","date_gmt":"2021-07-01T17:35:23","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7607"},"modified":"2021-08-30T19:36:26","modified_gmt":"2021-08-30T17:36:26","slug":"resumen-de-lecturas-compartidas-durante-junio-de-2021","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-junio-de-2021\/","title":{"rendered":"Resumen de lecturas compartidas durante junio de 2021"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante junio 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:\/\/www.sciencedirect.com\/science\/article\/pii\/S2352220821000626\">A Perron\u2013Frobenius theorem for deciding matrix growth<\/a>. ~ Ren\u00e9Thiemann. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/yfu.tw\/publication\/cav21-coq-qfbv\/cav21-coq-qfbv.pdf\">CoqQFBV: A scalable certified SMT quantifier-free bit-vector solver<\/a>. ~ Xiaomu Shi et als. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/www.ccas.ru\/ca\/_media\/ca-2021.pd\">On a machine-checked proof for an optimized method to multiply polynomials<\/a>. ~ S.D. Meshveliani.f#page=88 #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/Hester-Breman\/publication\/350607318_Augmenting_the_human_mathematician\/links\/608bc486a6fdccaebdf9063e\/Augmenting-the-human-mathematician.pdf\">Augmenting the human mathematician<\/a>. ~ H.K. S\u00f8rensen, M.W. Johansen, R. Hoekzema, H. Breman. #ITP #ATP #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1905.13100\">Towards finding longer proofs<\/a>. ~ Zsolt Zombori, Adri\u00e1n Csisz\u00e1rik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban. #ATP #MachineLearning<\/li>\n<li><a href=\"https:\/\/cdsmithus.medium.com\/towers-of-hanoi-from-a-random-start-db22d09da027\">Towers of Hanoi from a random start<\/a>. ~ Chris Smith. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/exlean.org\/well-founded-recursion\/\">Well-founded recursion<\/a>. ~ Gihan Marasingha. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/inria-00139131v2\/document\">A modular formalisation of finite group theory<\/a>. ~ Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, LaurentTh\u00e9ry. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/siddhartha-gadgil.github.io\/automating-mathematics\/posts\/sat-prover-lean\/\">SAT solver-prover in Lean 4<\/a>. ~ Siddhartha Gadgil. #ITP #LeanProver #Logic<\/li>\n<li><a href=\"http:\/\/siddhartha-gadgil.github.io\/ProvingGround\/\">ProvingGround: Automated Theorem proving by learning<\/a>. ~ Siddhartha Gadgil. #ITP #LeanProver #MachineLearning<\/li>\n<li><a href=\"http:\/\/siddhartha-gadgil.github.io\/presentations\/KWK-AutoMath.htm\">Automating Mathematics? ~ Siddhartha Gadgil<\/a>.l#\/ #Math #ATP #ITP #AI<\/li>\n<li><a href=\"http:\/\/math.iisc.ac.in\/~gadgil\/SMTGeom.pdf\">Euclidean geometry by high-performance solvers? ~ Siddhartha Gadgil, Anand Tadipatri<\/a>. #Math #ATP #SAT #SMT<\/li>\n<li><a href=\"http:\/\/www.contrib.andrew.cmu.edu\/~avigad\/Students\/serafin_thesis.pdf\">A formally verified proof of the central limit theorem<\/a>. ~ Luke Serafin. #PhD_Thesis #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/www.contrib.andrew.cmu.edu\/~avigad\/Students\/wu_thesis.pdf\">A formally verified proof of Kruskal\u2019s tree theorem in Lean<\/a>. ~ Minchao Wu. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/dodisturb.me\/posts\/2021-06-27-Typed-Programs-Dont-Leak-Data.html\">Typed programs don&#8217;t leak data<\/a>. ~ Mistral Contrastin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/yLw5j-4-aEE\">Historia de desaf\u00edos matem\u00e1ticos<\/a>. C\u00f3mo ganar un mill\u00f3n de d\u00f3lares. ~ Antonio P\u00e9rez. #Matem\u00e1ticas v\u00eda @manuel_de_leon<\/li>\n<li><a href=\"https:\/\/bit.ly\/3AboKvE\">La prova del software (in Italian)<\/a>. ~ Riccardo Brasca et als. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/philpapers.org\/archive\/DETGFA.pdf\">Groundwork for a fallibilist account of Mathematics<\/a>. ~ Silvia De Toffoli. #Math<\/li>\n<li><a href=\"https:\/\/morrowm.github.io\/posts\/2021-06-26-assoc.html\">Associated types in two different ways<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/bit.ly\/3h3jXDD\">Creaci\u00f3n art\u00edstica y creaci\u00f3n matem\u00e1tica<\/a>. ~ Juan Arias de Reyna. #Matem\u00e1ticas #ITP #LeanProver<\/li>\n<li><a href=\"http:\/\/abstract.ups.edu\/index.html\">Abstract algebra: Theory and applications<\/a>. ~ Thomas W. Judson et als. #eBook #Math #Sage<\/li>\n<li><a href=\"http:\/\/antoniobehn.cl\/cursillo2017\/\">Taller de Sage<\/a>. ~ Antonio Behn. #Sage #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/MiniSail.html\">MiniSail: A kernel language for the ISA specification language SAIL in Isabelle\/HOL<\/a>. ~ Mark Wassell. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Public_Announcement_Logic.html\">Public announcement logic (in Isabelle\/HOL)<\/a>. ~ Asta Halkj\u00e6r From. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/people.compute.dtu.dk\/ahfrom\/Formalizing%20Epistemic%20Logic.pdf\">Formalized soundness and completeness of epistemic logic<\/a>. ~ Asta Halkj\u00e6r From et als. #Logic #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/lt2021\/slides\/paula-LeanTogether2021.pdf\">Results in modal and dynamic epistemic logic (A formalization in Lean)<\/a>. ~ Paula Neeley. #Logic #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/www.rsme.es\/2021\/06\/hito-de-las-demostraciones-asistidas-por-ordenador-en-nature\/\">Hito de las demostraciones asistidas por ordenador en Nature<\/a>. ~ Nerea Diez L\u00f3pez. #DAO #LeanProver #Matem\u00e1ticas<\/li>\n<li><a href=\"http:\/\/endlessparentheses.com\/embedding-youtube-videos-with-org-mode-links.html\">Embedding Youtube videos with org-mode links<\/a>. ~ Artur Malabarba. #OrgMode #Emacs<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s42979-020-00417-3.pdf\">Verified model checking for conjunctive positive logic<\/a>. ~ Alex Abuin et als. #ITP #Dafny<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3453483.3454053\">CoStar: a verified ALL (*) parser<\/a>. ~ Sam Lasser et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3453483.3454027\">Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8<\/a>. ~ Kyeongmin Cho et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/elpais.com\/ciencia\/2021-06-24\/las-matematicas-que-estudian-los-limites-de-los-ordenadores.html\">Las matem\u00e1ticas que estudian los l\u00edmites de los ordenadores<\/a>. ~ Daniel Gra\u00e7a, \u00c1gata A. Tim\u00f3n. #Matem\u00e1ticas #Computaci\u00f3n<\/li>\n<li><a href=\"http:\/\/www.contrib.andrew.cmu.edu\/~avigad\/Students\/zipperer_ms_thesis.pdf\">A formalization of elementary group theory in the proof assistant Lean<\/a>. ~ Andrew Zipperer. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2021\/06\/24\/types-versus-sets-in-math-and-programming-languages\/\">Types versus sets in math and programming languages<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/math.andrej.com\/2021\/06\/24\/the-dawn-of-formalized-mathematics\/\">The dawn of formalized mathematics<\/a>. ~ Andrej Bauer. #ITP #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Van_der_Waerden.html\">Van der Waerden&#8217;s theorem in Isabelle\/HOL<\/a>. ~ Katharina Kreuzer, Manuel Eberl. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/blog\/2021-06-23-deconstructing-class\/\">Deconstructing classes<\/a>. ~ Nicholas Clarke. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/13901\/pdf\/LIPIcs-ITP-2021-6.pdf\">A formally verified checker for first-order proofs<\/a>. ~ Seulkee Baek. #ITP #Agda #Logic<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/13924\/pdf\/LIPIcs-ITP-2021-29.pdf\">Reaching for the star: Tale of a monad in Coq<\/a>. ~ Pierre Nigron, Pierre-\u00c9variste Dagand. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/13915\/pdf\/LIPIcs-ITP-2021-20.pdf\">Mechanising complexity theory: The Cook-Levin theorem in Coq<\/a>. ~ Lennard G\u00e4her, Fabian Kunze. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/13920\/pdf\/LIPIcs-ITP-2021-25.pdf\">A mechanized proof of the max-flow min-cut theorem for countable networks<\/a>. ~ Andreas Lochbihler. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/13917\/pdf\/LIPIcs-ITP-2021-22.pdf\">Formalization of basic combinatorics on words<\/a>. ~ \u0160t\u011bp\u00e1n Holub, \u0160t\u011bp\u00e1n Starosta. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/13926\/pdf\/LIPIcs-ITP-2021-31.pdf\">Proof Pearl: Playing with the Tower of Hanoi formally<\/a>. ~ Laurent Th\u00e9ry. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/13896\/pdf\/LIPIcs-ITP-2021-1.pdf\">The CakeML project&#8217;s quest for ever stronger correctness theorems<\/a>. ~ Magnus O. Myreen. #ITP #HOL4<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/13911\/pdf\/LIPIcs-ITP-2021-16.pdf\">A natural formalization of the mutilated checkerboard problem in Naproche<\/a>. ~ Adrian De Lon, Peter Koepke, Anton Lorenzen. #ITP #Naproche<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/13905\/pdf\/LIPIcs-ITP-2021-10.pdf\">Verified progress tracking for timely dataflow<\/a>. ~ M. Brun, S. Decova, A. Lattuada, D. Traytel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/github.com\/leanprover-community\/mathlib\/blob\/master\/src\/geometry\/euclidean\/sphere.lean\">Ptolemy\u2019s Theorem in Lean<\/a>. ~ Manuel Candales, Benjamin Davidson. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/magazines\/2021\/7\/253452-formal-software-verification-measures-up\/fulltext\">Formal software verification measures up<\/a>. ~ Samuel Greengard. #FormalVerification<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/magazines\/2021\/7\/253448-program-verification\/fulltext\">Program verification: Vision and reality<\/a>. ~ Moshe Y. Vardi. #FormalVerification<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2106.10966\">Consequence relations (An introduction to the Tarski-Lindenbaum method)<\/a>. ~ Alex Citkin, Alexey Muravitsky. #eBook #Logic #Math<\/li>\n<li><a href=\"https:\/\/cj-xu.github.io\/abm19\/mainzer.pdf\">From proof theory to proof assistants (Challenges of responsible software and AI)<\/a>. ~ Klaus Mainzer. #ITP #Coq #AI<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/IMP_Compiler.html\">A shorter compiler correctness proof for language IMP<\/a>. ~ Pasquale Noce. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/isabelle.systems\/conventions\/\">Isabelle community conventions<\/a>. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/search.isabelle.in.tum.de\">FindFacts: Experimental search platform for Isabelle and the AFP<\/a>.\/# #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/isabelle.systems\/\">Isabelle quick access links<\/a>. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/cdsmithus.medium.com\/hmock-first-rate-mocks-in-haskell-e59d7c3b066c\">HMock: first rate mocks in Haskell<\/a>. ~ Chris Smith. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/S0HvfXq3454\">A new kind of programming: Tactic metaprogramming in Haskell<\/a>. ~ Sandy Maguire. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/n4IgYrc0pes\">Testing smart contracts with QuickCheck<\/a>. ~ John Hughes. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/wJsXjsCvSPg\">Lift unliftable (and unlift liftable)<\/a>. ~ Veronika Romashkina. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/pdfs\/algebras-for-weighted-search.pdf\">Algebras for weighted search<\/a>. ~ Donnacha Ois\u00edn Kidney, Nicolas Wu. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2021\/06\/19\/competitive-programming-in-haskell-folding-folds\/\">Competitive programming in Haskell: folding folds<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mkdoku.github.io\/posts\/2021-06-19-molecular-dynamics.html%20\">Molecular dynamic simulations in Haskell<\/a>. ~ Sascha Bubeck. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.nature.com\/articles\/d41586-021-01627-2%20\">Mathematicians welcome computer-assisted proof in &#8216;grand unification&#8217; theory<\/a>. ~ Davide Castelvecchi. #ITP #LeanProver #Mat<\/li>\n<li><a href=\"https:\/\/www.research-collection.ethz.ch\/bitstream\/handle\/20.500.11850\/489454\/thesis.pdf?sequence=3\">Formal verification of composable security proofs<\/a>. ~ Seyed Reza Sefidgar. #PhDThesis #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2106.07707v1\">An alternative axiomatic presentation of Nelson algebras<\/a>. ~ Juan Manuel Cornejo, Andr\u00e9s Gallardo, Luiz Monteiro, Ignacio Viglizzo. #ATP #Prover9 #Mace4 #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/ikR4T44PT9w\">La gran familia de los n\u00fameros<\/a>. ~ Ra\u00fal Ib\u00e1\u00f1ez. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/youtu.be\/8LUPWXW_6rc\">Computer says &#8216;I don&#8217;t know&#8217; (The case for Honest AI)<\/a>. ~ Peter Flach. #AI via @hakankj<\/li>\n<li><a href=\"https:\/\/benjaminselfridge.github.io\/haskell\/mathematics\/2021\/06\/13\/finite-algebra-1.html\">Finite abstract algebra in Haskell<\/a>. ~ Ben Selfridge. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/~koch\/bachelor\/incompleteness.pdf\">Undecidability and incompleteness of second-order logic<\/a>. ~ Mark Koch. #ITP #Cog #Logic #Math<\/li>\n<li><a href=\"https:\/\/samuelgruetter.net\/assets\/lightbulb_pldi21.pdf\">Integration verification across software and hardware for a simple embedded system<\/a>. ~ A. Erbsen, S. Gruetter, J. Choi, C. Wood, A. Chlipala. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.cis.upenn.edu\/~sweirich\/papers\/spector-zabusky-thesis.pdf\">Don\u2019t mind the formalization gap: The design and usage of Hs-to-Coq<\/a>. ~ Antal Spector-Zabusky. #PhD_Thesis #ITP #Coq #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2106.05987\">Hybrid systems verification with Isabelle\/HOL: Simpler syntax, better models, faster proofs<\/a>. ~ Simon Foster, Jonathan Juli\u00e1n Huerta y Munive, Mario Gleirscher, Georg Struth. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/micahcantor.xyz\/blog\/median-heap-haskell\">Median heaps in Haskell<\/a>. ~ Micah Cantor. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/bit.ly\/3xiBmyF\">Theorem proving and Artificial Intelligence (A brief introduction)<\/a>. ~ Josef Urban. #ATP #ITP #AI #MachineLearning<\/li>\n<li><a href=\"https:\/\/bit.ly\/3gl4akg\">Towards a human-like reasoning system<\/a>. ~ Mateja Jamnik. #ATP #AI<\/li>\n<li><a href=\"https:\/\/bit.ly\/35hF7IB\">Mathematical reasoning in humans<\/a>. ~ Jay McClelland. #AI #Math<\/li>\n<li><a href=\"https:\/\/bit.ly\/2RT6ANU\">From Hammer to Scalpel: Progress in Automated Theorem Proving<\/a>. ~ Markus Rabe. #ATP #AI<\/li>\n<li><a href=\"https:\/\/bit.ly\/3xlg1EC\">Training a first-order theorem prover from synthetic data<\/a>. ~ Vlad Firoiu et als. #ATP #AI #MachineLearning<\/li>\n<li><a href=\"https:\/\/mathai-iclr.github.io\/papers\/papers\/MATHAI_18_paper.pdf\">Training a first-order theorem prover from synthetic data<\/a>. ~ Vlad Firoiu et als. #ATP #AI #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.06203\">Proof artifact co-training for theorem proving with language models<\/a>. ~ Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, Stanislas Polu. #ITP #LeanProver #MachineLearning<\/li>\n<li><a href=\"https:\/\/bit.ly\/3wm5hG3\">Neural theorem proving in Lean using proof artifact co-training and language models<\/a>. ~ Jesse Michael Han. #ITP #LeanProver #MachineLearning<\/li>\n<li><a href=\"https:\/\/youtube.com\/playlist?list=PLp2qifo30hMuNgmUUhgl82DTK2JTUqK6M\">Video series &#8220;Haskell by Example&#8221;<\/a>. ~ Michael Oswald. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/ensiwiki.ensimag.fr\/images\/2\/20\/Rapport_cousin_marie.pdf\">Formalisation du th\u00e9or\u00e8me de d\u00e9composition de Hahn avec le d\u00e9monstrateur interactif Isabelle<\/a>. ~ Marie Cousin. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2021\/13884\/pdf\/LIPIcs-TYPES-2020-5.pdf\">Synthetic completeness for a terminating Seligman-Style tableau system<\/a>. ~ Asta Halkj\u00e6r From. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/aIObfpWdDbo\">Teaching computers about numbers<\/a>. ~ Kevin Buzzard . #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/www.cse.unsw.edu.au\/~crizkallah\/theses\/harrison-scott-honours-thesis.pdf\">Towards a verified compiler from Cogent to LLVM<\/a>. ~ Harrison Jay Scott. #BsC_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.cse.chalmers.se\/~abela\/agda\/MultiSortedAlgebra.pdf\">Birkhoff&#8217;s completeness theorem for multi-sorted algebras formalized in Agda<\/a>. ~ Andreas Abel. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/www.cs.bham.ac.uk\/~txw467\/lics21.pdf\">Global optimisation with constructive reals<\/a>. ~ Dan R. Ghica, odd Waugh Ambridge. #ITP #Agda #Math<\/li>\n<li><a href=\"https:\/\/tonyday567.github.io\/posts\/avoid\/\">Haskell and the elegant attack<\/a>. ~ Tony Day. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/bwI3MSWQ-po\">Demostraci\u00f3n del teorema de Cantor-Schr\u00f6der-Bernstein<\/a>. ~ Urtzi Buijs. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/rebeccaskinner.net\/posts\/2021-06-09-getting-to-the-fixed-point.html\">The fixed point<\/a>. ~ Rebecca Skinner. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/exlean.org\/blog\/\">What the rec? Types dependent on terms, Lean eliminators, and threshold concepts<\/a>. ~ Gihan Marasingha. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/www.softwarefactory-project.io\/practical-haskell-use-cases.html\">Practical Haskell use cases<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/marcosh.github.io\/post\/2021\/06\/04\/introducing-haskell-in-soisy.html\">Introducing Haskell in Soisy<\/a>. ~ Marco Perone. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2106.05784\">Programming puzzles<\/a>. ~ Tal Schuster, Ashwin Kalyan, Oleksandr Polozov, Adam Tauman Kalai. #Programming #Python<\/li>\n<li><a href=\"https:\/\/github.com\/microsoft\/PythonProgrammingPuzzles\">Python Programming Puzzles (P3)<\/a>. #Programming #Python<\/li>\n<li><a href=\"https:\/\/www.lemonde.fr\/blog\/binaire\/2021\/06\/11\/des-bibliotheques-aux-logiciels-une-histoire-damour\/\">Des biblioth\u00e8ques aux logiciels: une histoire d\u2019amour!<\/a> ~ Sabrina Granger. #Programming<\/li>\n<li><a href=\"https:\/\/youtu.be\/6otIuI89fcU\">Jornada sobre Inteligencia Artificial de los Institutos de Investigaci\u00f3n de la Universidad de Zaragoza<\/a>. #IA<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007%2Fs10817-020-09584-7.pdf\">Certified quantum computation in Isabelle\/HOL<\/a>. ~ Anthony Bordg, Hanna Lachnitt, Yijun He. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/icube-publis.unistra.fr\/docs\/15134\/hal.pdf\">Combining pencil\/paper proofs and formal proofs, a challenge for Artificial Intelligence and mathematics education<\/a>. ~ Julien Narboux, Viviane Durand-Guerrier. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/ilyasergey.net\/assets\/pdf\/papers\/Watanabe-MComp.pdf\">A framework for certified program synthesis<\/a>. ~ Yasunari Watanabe. #PhDThesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2106.03906\">Learning to guide a saturation-based theorem prover<\/a>. ~ Ibrahim Abdelaziz et als. #ATP #MachineLearning<\/li>\n<li><a href=\"https:\/\/coqmath.blogspot.com\/2015\/01\/learning-set-theory-through-coq-part-1.html\">Learning set theory through Coq (part 1)<\/a>. ~ Kyle Stemen. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/coqmath.blogspot.com\/2015\/02\/learning-set-theory-through-coq-part-2.html\">Learning set theory through Coq (part 2)<\/a>. ~ Kyle Stemen. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/coqmath.blogspot.com\/2015\/02\/learning-set-theory-through-coq-part-3.html\">Learning set theory through Coq (part 3)<\/a>. ~ Kyle Stemen. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2106.01184\">Formally verified convergence of policy-rich DBF routing protocols<\/a>. ~ Matthew L. Daggitt, Timothy G. Griffin. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/d1wqtxts1xzle7.cloudfront.net\/66762807\/tphols05.pdf?1619895651=&amp;response-content-disposition=inline%3B+filename%3DTeaching_a_HOL_course_Experience_report.pdf&amp;Expires=1623139510&amp;Signature=FnVfzvP4dk3Wo~3AiYraNZVPRtbII4B6XawBO4iMOhP~nJIzG39oRQfdKJFy8Ts9Pi6NuS5QcnBgdASL0XaM4OlO46wQsWe~y5kt70-UdA-iYGnXcsK-t7iyx~MF6OIKGEspN3AbRas1WKEyRRniSGsJmfmwvXVlH0u202o-GXHehmk5F8agabp9EqSwST3-8IiOwCLDJTWsBdjN22CXs~3YVPUnn0FFjoND5Rmg5hRpfzSpLo1CGmsShzNA3kQLQ~OJ7G3BTfvgY~-OM30x4UOFJ4Sor-waAeerRNJGy-uFoIqJwdhkyoh6-6XfpWZ1KJ8HpvhHOIl-h7Ilt-~9Xg__&amp;Key-Pair-Id=APKAJLOHF5GGSLRBV4ZA\">Teaching a HOL course: experience report<\/a>. ~ Konrad Slind et als. #ITP #HOL4<\/li>\n<li><a href=\"https:\/\/slate.com\/technology\/2021\/05\/artificial-intelligence-moonshots-usually-fail.html\">Why A.I. Moonshots Miss (Ambitious predictions about the future powers of computers keep turning out to be wrong).<\/a> ~ Jeffrey Funk, Gary Smith. #AI<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2104.05207%20Liao%20Zhang,%20Lasse%20Blaauwbroek,%20Bartosz%20Piotrowski,%20Prokop%20%C4%8Cern%C3%BD,%20Cezary%20Kaliszyk,%20Josef%20Urban.\">Online machine learning techniques for Coq: a comparison<\/a>. ~ #ITP #Coq #MachineLearning<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2106.03015\">Learning proofs for the classification of nilpotent semigroups<\/a>. ~ Carlos Simpson. #ATP #MachineLearning #Math<\/li>\n<li><a href=\"https:\/\/bor0.wordpress.com\/2021\/06\/07\/re-inventing-the-monad-wheel\/\">Re-inventing the Monad wheel<\/a>. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/logicaltypes.blogspot.com\/2021\/06\/why-kleisli-arrow-matter.html\">Why Kleisli arrows matter<\/a>. ~ Douglas M. Auclair (geophf). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/williamdemeo\/TypeFunc\">TypeFunc: This repository collects some links and resources for learning about type theory, functional programming, and related subjects<\/a>. ~ Avatar William DeMeo. #ITP #FunctionalProgramming #Agda #Coq #Haskell #Idris #LeanProver #Scala<\/li>\n<li><a href=\"https:\/\/youtu.be\/w11mI67R95I\">Roger Penrose explains Godel&#8217;s incompleteness theorem in 3 minutes<\/a>. #Logic #Math<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2021\/06\/05\/half-a-year-of-the-liquid-tensor-experiment-amazing-developments\/\">Half a year of the Liquid Tensor Experiment: Amazing developments<\/a>. ~ Peter Scholze. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/paulaneeley.com\/wp-content\/uploads\/2021\/05\/draft1.pdf\">A formalization of dynamic epistemic logic<\/a>. ~ Paula Neeley. #ITP #LeanProver #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2105.14183\">Verified quadratic virtual substitution for real arithmetic<\/a>. ~ Matias Scharager, Katherine Cordwell, Stefan Mitsch, Andr\u00e9 Platzer. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/etd.ohiolink.edu\/apexprod\/rws_etd\/send_file\/send?accession=ohiou1618999718015199&amp;disposition=inline\">Verifying value iteration and policy iteration in Coq<\/a>. ~ David M. Masters. #MSc_Thesis #ITP #Coq #MachineLearning<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/~kirst\/downloads\/abstract_CoqWS_21.pdf\">A toolbox for mechanised first-order logic<\/a>. ~ Johannes Hostert, Mark Koch, Dominik Kirst. #ITP #Coq #Logic #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2105.14706v1\">The role of entropy in guiding a connection prover<\/a>. ~ Zsolt Zombori, Josef Urban, Miroslav Ol\u0161\u00e1k. #ATP #MachineLearning<\/li>\n<li><a href=\"https:\/\/blog.monadfix.com\/th-groups\">Declaration groups: where order of declarations suddenly matters in Haskell<\/a>. ~ Artyom Kazak. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.foxhound.systems\/blog\/final-tagless\/\">Final tagless encodings have little to do with typeclasses<\/a>. ~ Ben Levy. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.stackbuilders.com\/tutorials\/haskell\/getting-started-with-haskell-projects-using-scotty\/\">Getting started with Haskell projects using Scotty<\/a>. ~ Juan Pedro Villa Isaza. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/pbrisbin.com\/posts\/phantom-types-and-globbing-bugs\/\">Phantom types and globbing bugs<\/a>. ~ Patrick Brisbin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.haskellforall.com\/2021\/06\/probability-for-slay-spire-fanatics.html\">Probability for Slay the Spire fanatics<\/a>. ~ Gabriel Gonzalez. #Haskell #FunctionalProgramming #Math<\/li>\n<li><a href=\"https:\/\/mathscholar.org\/2021\/06\/bach-as-mathematician\/\">Bach as mathematician<\/a>. ~ David H Bailey. #Math #Music #Bach<\/li>\n<li><a href=\"https:\/\/youtu.be\/IoCcZ5CjuGc\">El Teorema de Cantor-Schr\u00f6der-Bernstein<\/a>. ~ Urtzi Buijs @archimedestub. #L\u00f3gica #Matem\u00e1tica<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/mathematicians-identify-threshold-at-which-shapes-give-way-20210603\/\">Mathematicians identify threshold at which shapes give way<\/a>. ~ Mordechai Rorvig. #Math<\/li>\n<li><a href=\"https:\/\/janmasrovira.gitlab.io\/ascetic-slug\/post\/haskell-proofs\/\">Using dependent types to write proofs in Haskell<\/a>. ~ Jan Mas Rovira. #Haskell #FunctionalProgramming #Logic<\/li>\n<li><a href=\"https:\/\/suzdalnitski.medium.com\/functional-programming-the-true-silver-bullet-fbeb7cf4a17a\">Functional Programming &#8211; the True Silver Bullet<\/a>. ~ Ilya Suzdalnitski. #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/how-a-simple-math-puzzle-can-guide-discovery-20210528\/\">How a simple arithmetic puzzle can guide discovery<\/a>. ~ Pradeep Mutalik. #Math<\/li>\n<li><a href=\"https:\/\/exlean.org\/relations-in-lean\/\">Relations in Lean<\/a>. ~ Gihan Marasingha. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/exlean.org\/decidable-propositions-i\/\">Decidable propositions I<\/a>. ~ Gihan Marasingha. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/exlean.org\/decidable-propositions-ii\/\">Decidable propositions II<\/a>. ~ Gihan Marasingha. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/exlean.org\/decidable-propositions-iii\/\">Decidable propositions III<\/a>. ~ Gihan Marasingha. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/exlean.org\/vectors-and-dependent-function-types\/\">Vectors and dependent function types<\/a>. ~ Gihan Marasingha. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/link.springer.com\/article\/10.1007\/s10516-021-09561-8\">The limits of computation<\/a>. ~ A. Powell. #CompSci #LambdaCalculus #TypeTheory<\/li>\n<li><a href=\"https:\/\/homepages.inf.ed.ac.uk\/slindley\/papers\/nbe-for-edsls-draft-may2021.pdf\">Practical normalization by evaluation for EDSLs<\/a>. ~ N. Valliappan, A. Russo, S. Lindley. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.cs.tufts.edu\/t\/tech_reports\/reports\/2021-01\/report.pdf\">Hook: An embedded domain-specific language for fusing implicit interactions to explicit event handlers<\/a>. ~ Tomoki Shibata, Usamatthew Ahrens, Usarobert J.K. Jacob. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/blanqui.gitlabpages.inria.fr\/papers\/fscd21.pdf\">Some axioms for mathematics<\/a>. ~ Fr\u00e9d\u00e9ric Blanqui et als. #Logic #Math<\/li>\n<li><a href=\"http:\/\/profs.sci.univr.it\/~bonacina\/papers\/JARLWHistoricSurvey.pdf\">Set of support, demodulation, paramodulation: a historical Perspective<\/a>. ~ Maria Paola Bonacina. #ATP #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Lifting_the_Exponent.html\">Lifting the exponent<\/a>. ~ Jakub K\u0105dzio\u0142ka. #ITP #IsabelleHOL #Math<\/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 junio 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\/7607"}],"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=7607"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7607\/revisions"}],"predecessor-version":[{"id":7608,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7607\/revisions\/7608"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7607"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7607"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7607"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}