{"id":7589,"date":"2020-10-01T19:00:36","date_gmt":"2020-10-01T17:00:36","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7589"},"modified":"2021-08-30T19:02:03","modified_gmt":"2021-08-30T17:02:03","slug":"resumen-de-lecturas-compartidas-durante-septiembre-de-2020","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-septiembre-de-2020\/","title":{"rendered":"Resumen de lecturas compartidas durante septiembre de 2020"},"content":{"rendered":"<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\/2009.13762\">Iteration in ACL2<\/a>. ~ Matt Kaufmann, J Strother Moore. #ITP #ACL2 #CommonLisp<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.13761\">Formal verification of arithmetic RTL: Translating Verilog to C++ to ACL2<\/a>. ~ David M. Russinoff. #ITP #ACL2<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/13063\/pdf\/lipics-vol175-types2019-complete.pd\">Coherence for monoidal groupoids in HoTT<\/a>. ~ Stefano Piceghello.f#page=199 #ITP #Coq #HoTT<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/13063\/pdf\/lipics-vol175-types2019-complete.pd\">Is impredicativity implicitly implicit? Stefan Monnier, Nathaniel Bos<\/a>.f#page=219 #ITP #Coq<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/13063\/pdf\/lipics-vol175-types2019-complete.pd\">Higher inductive type eliminators without paths<\/a>. ~ Nils Anders Danielsson.f#page=239 #ITP #Agda #HoTT<\/li>\n<li><a href=\"https:\/\/youtu.be\/jKCQsndqEGQ\">\u00bfQu\u00e9 es una red neuronal? | Aprendizaje profundo. Cap\u00edtulo 1<\/a>. #AI #AprendizajeAutom\u00e1tico<\/li>\n<li><a href=\"https:\/\/youtu.be\/mwHiaTrQOiI\">Descenso de gradiente. C\u00f3mo aprenden las redes neuronales | Aprendizaje profundo. Cap\u00edtulo 2<\/a>. #AI #AprendizajeAutom\u00e1tico<\/li>\n<li><a href=\"https:\/\/writings.stephenwolfram.com\/2020\/09\/the-empirical-metamathematics-of-euclid-and-beyond\/\">The empirical metamathematics of Euclid and beyond<\/a>. ~ Stephen Wolfram. #Logic #Math #ITP #LeanProver #Metamath<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/13063\/pdf\/lipics-vol175-types2019-complete.pd\">Making Isabelle content accessible in knowledge representation formats<\/a>. ~ Michael Kohlhase, Florian Rabe, Makarius Wenzel.f#page=11 #ITP #IsabelleHOL #MKM<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/13063\/pdf\/lipics-vol175-types2019-complete.pd\">Type theory unchained: Extending Agda with user-defined rewrite rules<\/a>. ~ Jesper Cockx.f#page=35 #Agda #ITP #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/29yTPSZAw_4\">The Tao of Types<\/a>. ~ Thorsten Altenkirch. #TypeTheory<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/13063\/pdf\/lipics-vol175-types2019-complete.pd\">Big step normalisation for type theory<\/a>. ~ Thorsten Altenkirch, Colin Geniet.f#page=99 #ITP #Agda #TypeTheory<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/13063\/pdf\/lipics-vol175-types2019-complete.pd\">For finitary induction-induction, induction is enough<\/a>. ~ Ambrus Kaposi, Andr\u00e1s Kov\u00e1cs, Ambroise Lafont. f#page=137 #ITP #Agda<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/13063\/pdf\/lipics-vol175-types2019-complete.pd\">Eta-equivalence in core dependent Haskell<\/a>. ~ Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, Stephanie Weirich.f#page=167 #Haskell #FunctionalProgramming #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.12154\">Integration of formal proof into unified assurance cases with Isabelle\/SACM<\/a>. ~ Simon Foster, Yakoub Nemouchi, Mario Gleirscher, Ran Wei, Tim Kelly. #ITP #Isabelle\/SACM<\/li>\n<li><a href=\"https:\/\/youtu.be\/SJ-_zqw5UHk\">Proving excluded middle in Lean (FP lunch 25\/9\/20)<\/a>. ~ Thorsten Altenkirch. #ITP #LeanProver #Logic<\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/mathlib_docs\/field_theory\/primitive_element.html\">Primitive element theorem in Lean<\/a>. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/mathlib_docs\/algebra\/universal_enveloping_algebra.html\">Universal enveloping algebra in Lean<\/a>. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/mathlib_docs\/analysis\/convex\/integral.html\">Jensen&#8217;s inequality for integrals in Lean<\/a>. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/haskell-via-sokoban.nomeata.de\/\">Haskell via Sokoban<\/a>. ~ Joachim Breitner. #Haskell #FunctionalProgramming #CodeWorld<\/li>\n<li><a href=\"https:\/\/blog.adrianistan.eu\/que-es-idris-y-por-que-es-un-lenguaje-de-programacion-tan-interesante\">\u00bfQu\u00e9 es Idris y por qu\u00e9 es un lenguaje de programaci\u00f3n tan interesante?<\/a> ~ Adri\u00e1n Arroyo. #Idris #Programaci\u00f3nFuncional<\/li>\n<li><a href=\"http:\/\/aitp-conference.org\/2020\/slides\/LP.pdf\">Machine learning and the formalisation of mathematics: Research challenges<\/a>. ~ Lawrence C Paulson. #ITP #ML<\/li>\n<li><a href=\"http:\/\/aitp-conference.org\/2020\/slides\/YS.pdf\">Developing a concept-oriented search engine for Isabelle based on natural language: Technical challenges<\/a>. ~ Yiannos Stathopoulos, Angeliki Koutsoukou-Argyraki, Lawrence Paulson. #ITP #IsabelleHOL #MKM #Math<\/li>\n<li><a href=\"http:\/\/aitp-conference.org\/2020\/slides\/YN.pdf\">Automation of proof by induction in Isabelle\/HOL using Domain-Specific Languages (LiFtEr: Logical Feature Extractor, SeLFiE: Semantic Logical Feature Extractor)<\/a>. ~ Yutaka Nagashima. #ITP #IsabelleHOL #ML<\/li>\n<li><a href=\"http:\/\/aitp-conference.org\/2020\/slides\/MW.pdf\">Reinforcement learning for interactive theorem proving in HOL4<\/a>. ~ Minchao Wu, Michael Norrish, Christian Walder, Amir Dezfouli. #ITP #HOL4 #ML<\/li>\n<li><a href=\"http:\/\/aitp-conference.org\/2020\/slides\/LB.pdf\">Relieving user effort for the auto tactic in Coq with machine learning<\/a>. ~ Lasse Blaauwbroek. #ITP #Coq #MachineLearning<\/li>\n<li><a href=\"http:\/\/aitp-conference.org\/2020\/slides\/DS.pdf\">The IMO Grand Challenge<\/a>. ~ Daniel Selsam. #AI #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/aitp-conference.org\/2020\/slides\/NG.pdf\">Classification of finite semigroups and categories using computational methods<\/a>. ~ Najwa Ghannoum et als. #APT #MACE4 #Math<\/li>\n<li><a href=\"http:\/\/aitp-conference.org\/2020\/slides\/MD.pdf\">Formal\/symbolic\/numerical computational methods<\/a>. ~ Michael R. Douglas. #AI #ITP #ML<\/li>\n<li><a href=\"http:\/\/aitp-conference.org\/2020\/slides\/JH.pdf\">Learning cubing heuristics for SAT from DRAT proofs<\/a>. ~ Jesse Michael Han. #ATP #SAT #ML<\/li>\n<li><a href=\"http:\/\/aitp-conference.org\/2020\/slides\/SP.pdf\">Learning theorem proving through self-play<\/a>. ~ Stanis\u0142aw Purga\u0142. #ATP #MachineLearning<\/li>\n<li><a href=\"http:\/\/builds.openlogicproject.org\/open-logic-complete.pdf\">The open logic text (Revision: 2020-09-24)<\/a>. #eBook #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.11403\">CertRL: Formalizing convergence proofs for value and policy iteration in Coq<\/a>. ~ Koundinya Vajjha, Avraham Shinnar, Vasily Pestun, Barry Trager, Nathan Fulton. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/etd.ohiolink.edu\/!etd.send_file?accession=ohiou1594805966855804&amp;disposition=inline\">Formalized generalization bounds for perceptron-like algorithms<\/a>. ~ Robin J. Kelby. #MSc_Thesis #ITP #Coq #Haskell<\/li>\n<li><a href=\"https:\/\/reanimate.github.io\/\">Reanimate: Build declarative animations with SVG and Haskell<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/medium.com\/cantors-paradise\/the-chessboard-puzzle-and-the-mathematics-of-invariants-8283e5b8cdeb\">The chessboard puzzle and the mathematics of invariants<\/a>. ~ Maths and Musings in Cantor\u2019s Paradise. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/www.gaussianos.com\/un-problema-que-llevaba-20-anos-abierto-i-grupos-de-trenzas-y-grupos-de-artin\/\">Un problema que llevaba 20 a\u00f1os abierto (I): Grupos de trenzas y grupos de Artin<\/a>. ~ Mar\u00eda Cumplido. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/chris-martin.org\/2020\/in-the-computer\">In the computer<\/a>. ~ Chris Martin. #Programming<\/li>\n<li><a href=\"http:\/\/composition.al\/blog\/2020\/09\/20\/course-retrospective-smt-solving-and-solver-aided-systems\/\">Course retrospective: SMT solving and solver-aided systems<\/a>. ~ Lindsey Kuper. #SMT #ATP<\/li>\n<li><a href=\"http:\/\/incredible.pm\/\">The Incredible Proof Machine<\/a>. #Logic<\/li>\n<li><a href=\"https:\/\/www.euclidea.xyz\/\">Euclidea: Geometric constructions game with straightedge and compass<\/a>. #Math #Game<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.08174\">Higher-order nonemptiness step by step<\/a>. ~ Pawe\u0142 Parys. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/www.csl.sri.com\/users\/rushby\/papers\/ontargbegs18.pdf\">A mechanically assisted examination of vacuity and question begging in Anselm\u2019s ontological argument<\/a>. ~ John Rushby. #ITP #PVS<\/li>\n<li><a href=\"https:\/\/www.diva-portal.org\/smash\/get\/diva2:1468318\/FULLTEXT01.pdf\">Verifying correctness of contract decompositions<\/a>. ~ Gustav Hedengran. #ITP #HOL4<\/li>\n<li><a href=\"https:\/\/netsec.ethz.ch\/publications\/papers\/Logres2020.pdf\">A formally verified protocol for log replication with byzantine fault tolerance<\/a>. ~ Joel Wanner, Laurent Chuat, Adrian Perrig. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/hal.inria.fr\/inria-00585203\/document\">Similar triangles and orientation in plane elementary geometry for Coq-based proofs<\/a>. ~ Tuan Minh Pham. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/kowainik.github.io\/posts\/deriving\">Strategic deriving<\/a>. ~ Veronika Romashkina, Dmitrii Kovanikov . #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.09541v1\">Foundations: a draft of a chapter on mathematical logic and foundations for an upcoming handbook of computational proof assistants<\/a>. ~ Jeremy Avigad. #Logic #Math #ITP #CompSci<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/at-the-international-mathematical-olympiad-artificial-intelligence-prepares-to-go-for-the-gold-20200921\/\">At the Math Olympiad, computers prepare to go for the gold<\/a>. ~ Kevin Hartnett. #Math #AI #ITP<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.09215\">Faster smarter induction in Isabelle\/HOL with SeLFiE<\/a>. ~ Yutaka Nagashima. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/owenlynch.org\/posts\/2020-09-16-haskells-children\/\">Haskell&#8217;s children<\/a>. ~ Owen Lynch. #Haskell #FunctionalProgramming #Rust #Idris #JuliaLang<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?ICLP2020.6.pdf\">Logic programming and machine ethics<\/a>. ~ Abeer Dyoub, Stefania Costantini, Francesca A. Lisi. #LogicProgramming<\/li>\n<li><a href=\"http:\/\/eptcs.web.cse.unsw.edu.au\/paper.cgi?ICLP2020.18.pdf\">Deriving theorems in implicational linear logic, declaratively<\/a>. ~ Paul Tarau, Valeria de Paiva. #Prolog #LogicProgramming #Logic<\/li>\n<li><a href=\"https:\/\/github.com\/alashworth\/sf-lean\/\">Software Foundations in Lean<\/a>. ~ Andrew Ashworth. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2020\/09\/19\/thoughts-on-the-pythagorean-theorem\/\">Thoughts on the Pythagorean theorem<\/a>. ~ Kevin Buzzard. #Math<\/li>\n<li><a href=\"https:\/\/www.wikiwand.com\/en\/List_of_unsolved_problems_in_mathematics\">List of unsolved problems in mathematics<\/a>. #Math<\/li>\n<li><a href=\"https:\/\/youtu.be\/ip92VMpf_-A\">Finger trees explained anew, and slightly simplified (functional pearl) Haskell<\/a>. ~ Koen Claessen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/people.inf.ethz.ch\/trayteld\/papers\/cade19-incompleteness\/incompleteness.pdf\">A formally verified abstract account of G\u00f6del\u2019s incompleteness theorems<\/a>. ~ Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Goedel_Incompleteness.html\">An abstract formalization of G\u00f6del&#8217;s incompleteness theorems<\/a>. ~ Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Goedel_HFSet_Semantic.html\">From abstract to concrete G\u00f6del&#8217;s incompleteness theorems (Part I)<\/a>. ~ Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Goedel_HFSet_Semanticless.html\">From abstract to concrete G\u00f6del&#8217;s incompleteness theorems (Part II)<\/a>. ~ Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Syntax_Independent_Logic.html\">Syntax-independent logic infrastructure<\/a>. ~ Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Robinson_Arithmetic.html\">Robinson arithmetic<\/a>. ~ Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Extended_Finite_State_Machines.html\">A formal model of extended finite state machines<\/a>. ~ Michael Foster, Achim D. Brucker, Ramsay G. Taylor, John Derrick. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Extended_Finite_State_Machine_Inference.html\">Inference of extended finite state machines<\/a>. ~ Michael Foster, Achim D. Brucker, Ramsay G. Taylor, John Derrick. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/jaspervdj.be\/posts\/2020-09-17-lazysort.html\">Lazy sort: Counting comparisons<\/a>. ~ Jasper Van der Jeugt. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/youtu.be\/gAuvVPw6_CQ\">Lean: The Calculator on Steroids<\/a>. ~ James Arthur. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/vimeo.com\/459020971\">Cubical Agda: A dependently typed programming language with univalence and higher inductive types<\/a>. ~ Anders M\u00f6rtberg. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/bit.ly\/3hI19Ij\">Art and automated reasoning tools in geometry<\/a>. ~ F. Botana, Tom\u00e1s Recio. #Math #CompSci #ATP #GeoGebra<\/li>\n<li><a href=\"http:\/\/www.cril.univ-artois.fr\/~roussel\/satgame\/satgame.php?lang=eng\">The SAT game<\/a>. ~ Olivier Roussel. #Logic #Game #SAT<\/li>\n<li><a href=\"https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0167642320301313\">Which monads Haskell developers use: An exploratory study<\/a>. ~ Ismael Figueroa, Paul Leger, Hiroaki Fukuda. #Haskell #FunctionalProgramming via @FunctorFact<\/li>\n<li><a href=\"https:\/\/pritesh-shrivastava.github.io\/blog\/2020\/09\/13\/fun-with-haskell\">Fun with Haskell<\/a>. ~ Pritesh Shrivastava. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dev.to\/sshine\/aggressive-refactoring-55m2\">Aggressive refactoring<\/a>. ~ Simon Shine. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/aneksteind.github.io\/posts\/2020-08-09.html\">Tensor chain contraction with refolds<\/a>. ~ David Anekstein. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/downloads.hindawi.com\/journals\/mpe\/2020\/3485846.pdf\">An application of knowledge engineering to mathematics curricula organization and formal verification<\/a>. ~ Eugenio Roanes-Lozano, Ang\u00e9lica Mart\u00ednez-Zarzuelo, Mar\u00eda Jos\u00e9 Fern\u00e1ndez-D\u00edaz. #Math #CompSci #FormalVerification #RBES<\/li>\n<li><a href=\"https:\/\/www.rsme.es\/wp-content\/uploads\/2020\/09\/PM-4-Sept-2020.pdf\">Problemas del mes (Septiembre 2020)<\/a>. #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/www.mdpi.com\/2227-7390\/8\/9\/1573\/pdf\">Coinductive natural semantics for compiler verification in Coq<\/a>. ~ Angel Z\u00fa\u00f1iga, Gemma Bel-Enguix. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2005.04722\">Dynamic IFC theorems for free!<\/a> ~ Maximilian Algehed, Jean-Philippe Bernardy, Catalin Hritcu. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/obround.blogspot.com\/2020\/09\/haskell-functors-in-detail-in-depth.html\">Haskell functors in detail: An in-depth tutorial\/reference about functors<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09581-w.pdf\">Formalising \u03a3-protocols and commitment schemes using CryptHOL<\/a>. ~ D. Butler, A. Lochbihler, D. Aspinall, A. Gasc\u00f3n. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/conferences.computer.org\/eurosp\/pdfs\/EuroSPW2020-7k9FlVRX4z43j4uE2SeXU0\/859700a634\/859700a634.pdf\">Towards formal verification of program obfuscation<\/a>. ~ Weiyun Lu, Bahman Sistany, Amy Felty, Philip Scott. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/pdfs.semanticscholar.org\/4136\/15ac7e17e039baaa5a17ec869c96b5e038dc.pdf\">The duality of subtyping<\/a>. ~ Bruno C. d. S. Oliveira, Cuui Shaobo, Baber Rehman. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/computer-scientist-donald-knuth-cant-stop-telling-stories-20200416\/\">The computer scientist who can\u2019t stop telling stories<\/a>. ~ Susan D&#8217;Agostino. #CompSci<\/li>\n<li><a href=\"https:\/\/raw.githubusercontent.com\/maxd13\/logic-soundness\/master\/docs\/paper_final.pdf\">Proving the consistency of Logic in Lean<\/a>. ~ Luiz Carlos R. Viana. #ITP #LeanProver #Logic<\/li>\n<li><a href=\"https:\/\/fmbc.gitlab.io\/2020\/files\/FMBC2020.pd\">Authenticated data structures as functors in Isabelle\/HOL<\/a>. ~ Andreas Lochbihler, Ognjen Mari\u0107.f#page=52 #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/fmbc.gitlab.io\/2020\/files\/FMBC2020.pd\">Inter-blockchain protocols with the Isabelle infrastructure framework<\/a>. ~ Florian Kamm\u00fcller, Uwe Nestmann.f#page=105 #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/fmbc.gitlab.io\/2020\/files\/FMBC2020.pd\">Verifying, testing and running smart contracts in ConCert<\/a>. ~ Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters.f#page=118 #ITP #Coq<\/li>\n<li><a href=\"https:\/\/fmbc.gitlab.io\/2020\/files\/FMBC2020.pd\">Albert, an intermediate smart-contract language for the Tezos blockchain<\/a>. ~ Bruno Bernardo, Rapha\u00ebl Cauderlier, Arvid Jakobsson, Basile Pesin, Julien Tesson.f#page=128 #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.05539\">A general definition of dependent type theories<\/a>. ~ Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine. #TypeTheory #Logic #Math #ITP #Coq<\/li>\n<li><a href=\"http:\/\/tomasp.net\/academic\/papers\/monads\/monads-programming.pdf\">What we talk about when we talk about monads<\/a>. ~ Tomas Petriceka. #Haskell #FunctionalProgramming #CategoryTheory via @impurepics<\/li>\n<li><a href=\"https:\/\/github.com\/rpgcbaptista\/coq\">Some proofs about sequences and series in Coq<\/a>. #ITP #Coq #Math0<\/li>\n<li><a href=\"https:\/\/youtu.be\/zCJV0xNY06o\">Liquid Haskell<\/a>. ~ Andres L\u00f6h. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.cs.ru.nl\/bachelors-theses\/2020\/Rick_Koenders___4576519___Intuitionism_in_Lean.pdf\">Intuitionism in Lean<\/a>. ~ Rick Koenders. #BsC_Thesis #ITP #LeanProver #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.03393\">Generative language modeling for automated theorem proving<\/a>. ~ Stanislas Polu, Ilya Sutskever. #ATP #MachineLearning #DeepLearning<\/li>\n<li><a href=\"https:\/\/softwarefoundations.cis.upenn.edu\/vc-current\/index.html\">Verifiable C (Software foundations, Volume 5)<\/a>. ~ Andrew W. Appel, Qinxiang Cao, #eBook #ITP #Coq<\/li>\n<li><a href=\"https:\/\/youtu.be\/TGLmbl9x7s0\">Theorems for free<\/a>. ~ Lars Hupel. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/obround.blogspot.com\/2020\/09\/understanding-ghcs-error-messages-ghcs.html\">Haskell: Understanding GHC&#8217;s error messages<\/a>. ~ Obro Und. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/sanj.ink\/posts\/2020-06-13-contravariant-functors-are-weird.html\">Contravariant functors are weird<\/a>. ~ Sanjiv Sahayam. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/meeshkan.com\/blog\/purescript-2020\/\">Four reasons that PureScript is your best choice to build a server in 2020<\/a>. ~ Mike Solomon. #PureScript #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/pepeiborra\/hls-tutorial\">Let\u2019s write a Haskell Language Server plugin<\/a>. ~ Pepe Iborra. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dev.to\/samhh\/monoids-and-semigroups-2b94\">Monoids (and semigroups)<\/a>. ~ Sam A. Horvath-Hunt. #Haskell #TypeScript #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/minikanren.org\/workshop\/2020\/minikanren-2020-paper11.pdf\">Certified semantics for disequality<\/a>. ~ Dmitry Rozplokhas, Dmitry Boulytchev. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/github.com\/dboulytchev\/miniKanren-coq\/tree\/disequality\">miniKanren-coq: A certified semantics for relational programming workout<\/a>. ~ Dmitry Boulytchev. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09576-7\">Machine learning guidance for connection tableaux<\/a>. ~ Michael F\u00e4rber, Cezary Kaliszyk, Josef Urban. #Logic #ATP #MachineLearning<\/li>\n<li><a href=\"https:\/\/codygman.dev\/posts\/2020-09-07-Ergonomic_haskell_1_records.html\">Ergonomic Haskell 1: Records<\/a>. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/liamoc\/holbert\">Holbert: A graphical interactive proof assistant designed for education<\/a>. ~ Liam O&#8217;Connor. #ITP #Haskell #Logic<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/~rech\/master\/thesis.pdf\">Mechanising set theory in Coq (The generalised continuum hypothesis and the axiom of choice)<\/a>. ~ Felix Rech. #MsC_Thesis #ITP #Coq #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.cs.princeton.edu\/~appel\/papers\/plcc.pdf\">Program logics for certified compilers<\/a>. ~ Andrew W. Appel et als. #eBook #ITP #Coq<\/li>\n<li><a href=\"https:\/\/youtu.be\/0DTg1sgw58Y\">Language-integrated verification<\/a>. ~ Ranjit Jhala. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.01326\">Check your (students&#8217;) proofs-with holes<\/a>. ~ Dennis Renz, Sibylle Schwarz, Johannes Waldmann. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2008.12716v1\">Practical idiomatic considerations for checkable meta-logic in experimental functional programming<\/a>. ~ Baltasar Tranc\u00f3n y Widemann, Markus Lepper. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/ostina.to\/posts\/2020-08-20-maybe-is-great.html\">Actually, Maybe is great<\/a>. ~ Dave Della Costa. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.well-typed.com\/blog\/2020\/08\/implementing-a-ghc-plugin-for-liquid-haskell\/\">Implementing a GHC plugin for Liquid Haskell<\/a>. ~ Alfredo Di Napoli. #Haskell #FunctionalProgramming #LiquidHaskell<\/li>\n<li><a href=\"https:\/\/free.cofree.io\/2020\/09\/01\/type-errors\/\">Un-obscuring a few GHC type error messages<\/a>. ~ Ziyang Liu. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/oleg.fi\/gists\/posts\/2020-08-28-indexed-fixpoint.html\">Fixed points of indexed functors<\/a>. ~ Oleg Grenrus. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/notxor.nueva-actitud.org\/blog\/2020\/09\/04\/la-calculadora-de-emacs\/\">La calculadora de Emacs<\/a>. #Emacs<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.00416\">Church&#8217;s thesis and related axioms in Coq&#8217;s type theory<\/a>. ~ Yannick Forster. #ITP #Coq #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.labri.fr\/perso\/casteran\/addition-chains.pdf\">Addition chains<\/a>. ~ Pierre Cast\u00e9ran. #ITP #Coq #Math<\/li>\n<li><a href=\"http:\/\/leanprover.github.io\/presentations\/20150123_lean-mode\/lean-mode.pdf\">lean-mode (emacs mode for Lean Theorem Prover)<\/a>. ~ Soonho Kong, Leonardo de Moura. #ITP #LeanProver #Emacs<\/li>\n<li><a href=\"https:\/\/era.ed.ac.uk\/bitstream\/handle\/1842\/37236\/McLaughlin2020.pdf\">Relational reasoning for effects and handlers<\/a>. ~ Craig McLaughlin. #PhDThesis #Haskell #FunctionalProgramming #ITP #Agda<\/li>\n<li><a href=\"http:\/\/formacionib.org\/congreso-entorno-digital\/0018.pdf\">Herramientas de razonamiento autom\u00e1tico en GeoGebra: qu\u00e9 son y para qu\u00e9 sirven<\/a>. ~ Steven Van Vaerenbergh, Tom\u00e1s Recio, Pilar V\u00e9lez. #RA #GeoGebra #Matem\u00e1ticas<\/li>\n<li><a href=\"https:\/\/www.poberezkin.com\/posts\/2020-09-04-dependent-types-to-code-are-what-static-types-to-data.html\">Dependent types to code are what static types to data (Modeling state machines: Part 2)<\/a>. ~ Evgeny Poberezkin. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/free.cofree.io\/2019\/07\/31\/beautiful-bridges\/\">Solving the &#8220;Beautiful bridges&#8221; problem, algebraically<\/a>. ~ Ziyang Liu. #Math #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/research.chalmers.se\/publication\/518742\/file\/518742_Fulltext.pdf\">Practical dependent type checking using twin types<\/a>. ~ V\u00edctor L\u00f3pez Juan, Nils Anders Danielsson. #ITP #Agda #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2008.12751\">A framework for generating diverse Haskell-IO exercise tasks<\/a>. ~ Oliver Westphal. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/lsfa2020.ufba.br\/lsfa2020-preproc.pd\">Formalization of cryptographic algorithms in the Lean Theorem Prover<\/a>. ~ Guilherme Gomes Felix da Silva, Edward Hermann Haeusler, Bruno Lopes.f#page=127 #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Inductive_Inference.html\">Some classical results in inductive inference of recursive functions in Isabelle\/HOL<\/a>. ~ Frank J. Balbach. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/BirdKMP.html\">Putting the &#8216;K&#8217; into Bird&#8217;s derivation of Knuth-Morris-Pratt string matching in Isabelle\/HOL<\/a>. ~ Peter Gammie. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.00416\">Church\u2019s thesis and related axiomsin Coq\u2019s type theory<\/a>. ~ Yannick Forster. #ITP #Coq #Logic #TypeTheory<\/li>\n<li><a href=\"https:\/\/mathscholar.org\/2020\/09\/can-computers-do-mathematical-research\/\">Can computers do mathematical research? ~ David H Bailey<\/a>. #Math #CompSci<\/li>\n<li><a href=\"https:\/\/mathematicswithoutapologies.wordpress.com\/2020\/09\/01\/the-inevitable-questions-about-automated-theorem-proving\/\">The inevitable questions about automated theorem proving<\/a>. ~ Michael Harris. #ATP #ITP #AI #Math<\/li>\n<li><a href=\"https:\/\/cacm.acm.org\/blogs\/blog-cacm\/247125-can-machine-learning-algorithms-replace-exams\/fulltext\">Can machine learning algorithms replace exams? ~ Orit Hazzan, Koby Mike<\/a>. #AI #DataScience<\/li>\n<li><a href=\"https:\/\/ethz.ch\/en\/news-and-events\/eth-news\/news\/2020\/08\/infinite-fun-with-the-infinite-worlds.html\">Infinite fun with infinite worlds<\/a>. ~ Florian Meyer. #Logic #Math<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/PAC_Checker.html?utm_source=dlvr.it&amp;utm_medium=twitter\">Practical algebraic calculus checker in Isabelle\/HOL<\/a>. ~ Mathias Fleury, Daniela Kaufmann. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/raw.githubusercontent.com\/oswald2\/haskell_articles\/master\/HaskellArticles_1_6.pdf\">A list of Haskell articles on good design, good testing<\/a>. ~ William Yao et als. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/profile\/Walter_Carnielli2\/publication\/343838215_Godel's_Incompleteness_Theorems_from_a_Paraconsistent_Perspective\/links\/5f445bde299bf13404ef921e\/Goedels-Incompleteness-Theorems-from-a-Paraconsistent-Perspective.pdf\">G\u00f6del&#8217;s incompleteness theorems from a paraconsistent perspective<\/a>. ~ Walter Carnielli, David Fuenmayor. #ITP #IsabelleHOL #Logic #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2008.13610\">VerifyThis 2019: A program verification competition (Extended report)<\/a>. ~ Claire Dross, Carlo A. Furia, Marieke Huisman, Rosemary Monahan, Peter M\u00fcller. #FormalVerification<\/li>\n<li><a href=\"https:\/\/research.metastate.dev\/a-gentle-introduction-to-dependent-types\/\">A gentle introduction to dependent types<\/a>. ~ A. Samartino. #FunctionalProgramming<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Al final de cada art\u00edculo se encuentran etiquetas relativas a los sistemas que usa o a su contenido. Una recopilaci\u00f3n de todas las lecturas compartidas se encuentra en GitHub.<\/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\/7589"}],"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=7589"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7589\/revisions"}],"predecessor-version":[{"id":7590,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7589\/revisions\/7590"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7589"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7589"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7589"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}