Resumen de lecturas compartidas durante enero de 2020
Esta entrada es una recopilación de lecturas compartidas, durante enero de 2020, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
Las lecturas están ordenadas según su fecha de publicación en Twitter.
Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
- Introduction to HOL4 theorem prover. ~ K. Aksoy, S. Tahar, Y. Zeren. #ITP #HOL4
- Design and verification of parity checking circuit using HOL4 theorem proving. ~ E. Deni̇z, K. Aksoy, S. Tahar, Y. Zeren. #ITP #HOL4
- Proof searching in HOL4 with genetic algorithm. ~ M.Z. Nawaz et als #ITP #HOL4
- Defunctionalization: Everybody does it, nobody talks about it. ~ James Koppel. #FunctionalProgramming #Haskell
- Constructive reverse mathematics. ~ Hannes Diener. #Logic #Math
- Formalizing modal logic in HOL. ~ Yiming Xu. #PhD_Thesis #ITP #HOL #Logic
- On correctness of an n queens program. ~ Włodzimierz Drabent. #LogicProgramming #Prolog #Verification
- The simple Haskell initiative. #Haskell #FunctionalProgramming
- A computer made from DNA can compute the square root of 900. #CompSci
- Learn Haskell now! ~ Yann Esposito (@yogsototh). #Haskell #FunctionalProgramming
- Lean versus Coq: The cultural chasm. ~ Ramkumar Ramachandra. #ITP #LeanProver #Coq
- Type-level rewrite rules. ~ Samuel Gélineau. #Haskell #FunctionalProgramming
- Mandelbrot & Lovejoy’s rain fractals. ~ Jasper Van der Jeugt (@jaspervdj). #Haskell #FunctionalProgramming
- Kind inference for datatypes. ~ N. Xie, R.A. Eisenberg, B.C.d.S. Oliveira. #Haskell #FunctionalProgramming
- Organizing our package! ~ James Bowen (@james_OWA). #Haskell #Cabal #FunctionalProgramming
- Resumen de lecturas compartidas durante septiembre de 2019. #FunctionalProgramming #Haskell #ITP #IsabelleHOL #Coq #Agda
- Resumen de lecturas compartidas durante octubre de 2019. #FunctionalProgramming #Haskell #ITP #IsabelleHOL #Coq #Agda
- Resumen de lecturas compartidas durante noviembre de 2019. #FunctionalProgramming #Haskell #ITP #IsabelleHOL #Coq #Agda
- Resumen de lecturas compartidas durante diciembre de 2019. #FunctionalProgramming #Haskell #ITP #IsabelleHOL #Coq #Agda
- Formalizing a Seligman-style tableau system for hybrid logic in Isabelle/HOL. ~ Asta Halkjær. #ITP #IsabelleHOL #Logic
- Different problems, common threads: Computing the difficulty of mathematical problems. ~ Karen Lange. #Math #CompSci
- Estimating the proportion of smooth numbers. ~ John D. Cook (@JohnDCook). #Math #Programming #Python
- Lean 3 for hackers. ~ J Kenneth King. #LeanProver #FunctionalProgramming
- Haskell language extension taxonomy. ~ Doug Beardsley. #Haskell #FunctionalProgramming
- A formal proof of the irrationality of ζ(3). ~ Assia Mahboubi, Thomas Sibut-Pinote. #ITP #Coq #Math
- Proof pearl: Braun trees. ~ T. Nipkow, T. Sewell. #ITP #IsabelleHOL
- Gauss sums and the Pólya–Vinogradov inequality. ~ R. Raya, M. Eberl. #ITP #IsabellleHOL #Math
- Bicategories in Isabelle/HO: ~ Eugene W. Stark. #ITP #IsabelleHOL
- The irrationality of ζ(3) in Isabelle/HOL. ~ Manuel Eberl. #ITP #IsabellleHOL #Math
- Skip lists in Isabelle/HOL. ~ M.W. Haslbeck, M. Eberl. #ITP #IsabelleHOL
- Motivated proofs: what they are, why they matter and how to write them. ~ Rebecca Lea Morris. #Math
- Programming with categories. ~ Peter Smith. #Programming #CategoryTheory
- Generating small binaries in Haskell. ~ Alex Dixon (@dixonary_). #Haskell #FunctionalProgramming
- Collections of papers and books about Haskell, type theory and category theory. ~ Saurabh Kukade. #Haskell #TypeTheory #CategoryTheory
- LF+ in Coq for “fast and loose” reasoning. ~ F. Alessi. #ITP #Coq
- Selective applicative functors & probabilities. ~ Armando Santos (@_bolt12). #MSc_Thesis #Haskell #FunctionalProgramming #Math
- Linear algebra of programming – Algebraic matrices in Haskell. ~ Armando Santos (@_bolt12). #FunctionalProgramming #Math
- Gain confidence with Haskell! ~ Brandon Chinn. #Haskell #FunctionalProgramming
- Programming algorithms: approximation. ~ Vsevolod Dyomkin. #CommonLisp #Algorithms
- The road to proficient Haskell. ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming
- Teach yourself Logic 2020: A study guide. ~ Peter Smith. #Logic
- Rusty Razor is a tool for constructing finite models for first-order theories. ~ Salman Saghafi. #Logic
- A framework for exploring finite models. ~ Salman Saghafi. #PhD_Thesis #Logic #Haskell
- Computer Science as the continuation of Logic by other means. ~ Georg Gottlob. #Logic #CompSci #WorldLogicDay
- Mathematical Logic in Computer Science. ~ Assaf Kfoury. #Logic #CompSci #WorldLogicDay
- On the unusual effectiveness of Logic in Computer Science. ~ J.Y. Halpern et als. #Logic #CompSci #WorldLogicDay
- Computer Science and Logic (a match made in heaven). ~ Luca Aceto. #Logic #CompSci #WorldLogicDay
- The story of Logic. ~ Robert L. Constable. #Logic #CompSci #WorldLogicDay
- History of interactive theorem .proving. ~ J. Harrison, J. Urban, F. Wiedijk. #ITP #Logic #CompSci #WorldLogicDay
- Automated reasoning: From bold dreams to Computer Science methodology. ~ Robert L. Constable. #ATP #CompSci #WorldLogicDay
- Can the computer really help us to prove theorems? ~ Herman Geuvers. #ITP #Logic #CompSci #WorldLogicDay
- TAUT: A website that contains randomly-generated, self-correcting logic excercises. ~ Ariel Roffé. #Logic
- TAUT: el software desarrollado por un filósofo del CONICET para enseñar Lógica. #Lógica #WorldLogicDay
- Randomly generated and self-correcting logic exercises site. ~ Justin Weinberg. #Logic #WorldLogicDay
- Adjunctions in the wild: foldl. ~ Justin Le (@mstk). #Haskell #FunctionalProgramming
- Computer-supported exploration of a categorical axiomatization of modeloids. ~ L. Tiemens, D.S. Scott, C. Benzmüller, M. Benda. #ITP #IsabelleHOL #Math
- Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel’s ontological argument. ~ C. Benzmüller, D. Fuenmayor. #ITP #IsabelleHOL #Logic
- A verified packrat parser interpreter for parsing expression grammars. ~ C. Blaudeau, N. Shankar. #ITP #PVS
- Using Cabal on its own. ~ James Bowen (@james_OWA). #Haskell #Cabal
- Common stanzas. ~ Veronika Romashkina (@vronnie911). #Haskell #Cabal
- Closest pair of points algorithms. ~ M. Rau, T. Nipkow. #ITP #IsabelleHOL
- Automatic generation and verification of test-stable floating-point code. ~ L. Titolo, M. Moscato, C.A. Muñoz. #ITP #PVS
- The space of mathematical software systems. ~ J. Carette, W.M. Farmer, Y. Sharoda. #ATP #ITP #Math #CompSci
- A mechanized formalization of the WebAssembly specification in Coq. ~ X. Huang. #ITP #Coq
- Is Haskell a category? ~ B. Fong, B. Milewski, D. Spivak. #Haskell #FunctionalProgramming #CategoryTheory
- Your students could have invented … the Pythagorean theorem. ~ Chris Smith (@cdsmithus). #Math #Teaching
- Programming with categories (Draft). ~ B. Fong, B. Milewski, D.I. Spivak. #FunctionalProgramming #Haskell #CategoryTheory
- Verified approximation algorithms in Isabelle/HOL. ~ R. Eßmann, T. Nipkow, S. Robillard. #ITP #IsabelleHOL
- La magia del orden (de los datos). ~ Alejandro Serrano (@trupill). #Algoritmos
- A tale of two functors (or: how I learned to stop worrying and love Data and Control). ~ Arnaud Spiwack. #Haskell #FunctionalProgramming
- Talks from the formal methods in Mathematics / Lean together 2020 workshop. #ITP #LeanProver #IsabelleHOL #Coq
- Generating mathematical structure hierarchies using Coq-ELPI. ~ C. Cohen, K. Sakaguchi, E. Tassi. #ITP #Coq #Math
- High level commands to declare a hierarchy based on packed classes. ~ C. Cohen, K. Sakaguchi, E. Tassi. #ITP #Coq #Math
- On a mathematician’s attempts to formalize his own research in proof assistants. ~ Sébastien Gouëzel. #ITP #IsabelleHOL #LeanProver #Math
- Automating asymptotics in a theorem prover. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
- Using Lean for new research. ~ Neil Strickland. #ITP #LeanProver #Math
- Iterated chromatic localisation. ~ Neil Strickland, Nicola Bellumat. #ITP #LeanProver #Math
- Lean code formalising many of the proofs from the paper “Iterated chromatic localisation”. ~ Neil Strickland, Nicola Bellumat. #ITP #LeanProver #Math
- Proof in Lean that there are infinitely many primes. ~ Neil Strickland. #ITP #LeanProver #Math
- Reasoning with non-linear formulas in Isabelle/HOL. ~ Wenda Li. #ITP #IsabelleHOL #Math
- ODEs and the Poincaré-Bendixson theorem in Isabelle/HOL. ~ Fabian Immler, Yong Kiam Tan. #ITP #IsabelleHOL #Math
- Julia programming’s dramatic rise in HPC and elsewhere. ~ John Russell. #JuliaLang
- Complex geometry in Isabelle/HOL. ~ F. Marić, D. Simić. #ITP #IsabelleHOL #Math
- Poincaré disc model in Isabelle/HOL. ~ D. Simić, F. Marić, P. Boutry. #ITP #IsabelleHOL #Math
- Static types are dangerously interesting. ~ Alex Nixon (@alexnixon_uk). #Haskell #FunctionalProgramming
- Digging into Lenses. ~ Josh Kuhn (@deontologician). #Haskell #FunctionalProgramming
- Formalizing a sophisticated definition. ~ Patrick Massot, Kevin Buzzard, Johan Commelin. #ITP #LeanProver #Math
- A Coq formalization of Lebesgue integration of nonnegative functions. ~ Sylvie Boldo et als. #ITP #Coq #Math
- First-order theorem (dis)proving for reachability problems in verification and experimental mathematics. ~ Alexei Lisitsa. #ATP #Prover9 #Mace4 #Math
- SMTCoq: Coq automation and its application to formal mathematics. ~ Chantal Keller. #ITP #Coq #SMT #Math
- Metamath Zero (or: how to verify a verifier). ~ Mario Carneiro. #ITP #MetamathZero
- Lisping at JPL. ~ Ron Garret. #Programming #CommonLisp
- Números primos que son imágenes. ~ @Alvy #Matemáticas
- swMATH: an information service for mathematical software. #Math #CompSci
- The Encyclopedia of Mathematics wiki is an open access resource designed specifically for the mathematics community. #Math
- Theorem prover. ~ Encyclopedia of Mathematics. #ATP #ITP #Math
- NIST digital library of mathematical functions. #Math
- The On-Line Encyclopedia of Integer Sequences (OEIS). #Math
- A modern perspective on type theory: From its origins until today. ~ Fairouz Kamareddine, Twan Laan, and Rob Nederpelt. #eBook #TypeTheory
- The future of Mathematics? ~ Kevin Buzzard. #Math #ITP
- Formal specification of a security framework for smart contracts. ~ M. Mandrykin et als. #ITP #IsabelleHOL
- Tabled typeclass resolution. ~ D. Selsam, S. Ullrich, L. de Moura. #ITP #LeanProver
- Mersenne primes and the Lucas–Lehmer test in Isabelle/HOL. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
- Nicer package organization with Stack! ~ James Bowen (@james_OWA). #Haskell #Stack
- A small matter of programming. ~ Jeremy Gibbons. #AI #Programming
- Adding online exercises with automated grading to any logic course with Carnap. ~ Richard Zach (@RrrichardZach). #Logic #Teaching
- Three equivalent ordinal notation systems in cubical Agda. ~ Fredrick Nordvall Forsberg. #ITP #Agda #Math
- Undecidability of higher-order unification formalised in Coq. ~ Simon Spies. #ITP #Coq
- A functional proof pearl: Inverting the Ackermann heirarchy. ~ Linh Tran. #ITP #Coq
- Euclid’s theorem on the infinitude of primes: a historical survey of its proofs (300 B.C.–2017) and another new proof. ~ Romeo Meštrović. #Math #History
- Crash course on higher-order logic, type theory, etc. ~ Theodore Sider. #Logic via @RrrichardZach
- Verified programming of Turing machines in Coq. ~ Fabian Kunze. #ITP #Coq
- Proof pearl: Braun trees. ~ Tobias Nipkow. #ITP #IsabelleHOL
- Algebraic data types aren’t numbers on steroids. Mark Seemann (@ploeh). #Haskell #FunctionalProgramming
- Differential Hoare logics and refinement calculi for hybrid systems with Isabelle/HOL. ~ Simon Foster, Jonathan Julián Huerta y Munive, and Georg Struth. #ITP #IsabelleHOL
- Formalizing π-calculus in Guarded Cubical Agda. ~ Niccolò Veltri, Andrea Vezzosi. #ITP #Agda
- For beginners. ~ Julie Moronuki (@argumatronic). #Haskell #FunctionalProgramming
- Drawing Prolog search trees: A manual for teachers and students of logic programming. ~ Johan Bos. #Prolog #LogicProgramming
- Towards an Isabelle Theory for distributed, interactive systems-the untimed case. ~ Jens Christoph Bürger et als. #ITP #IsabelleHOL
- Coinductive formalization of SECD machine in Agda. ~ Adam Krupička. #MsC_Thesis #ITP #Agda
- Folding lists. ~ Chris Martin (@chris__martin), Julie Moronuki (@argumatronic). #Haskell #FunctionalProgramming
- Beautiful mutable values. ~ Justin Le (@mstk). #Haskell #FunctionalProgramming
- Haskell problems for a new decade. ~ Stephen Diehl (@smdiehl). #Haskell #FunctionalProgramming
- The Functor family: Profunctor. ~ Vladimir Ciobanu. #Haskell #FunctionalProgramming
- Formally verified code obfuscation in the Coq Proof Assistant. ~ Weiyun Lu. #PhD_Thesis #ITP #Coq
- A formalised polynomial-time reduction from 3SAT to Clique. ~ Lennard Gäher. #ITP #Coq
- Haskell in production: CentralApp. ~ Ashesh Ambasta (@AsheshAmbasta), Gints Dreimanis. #Haskell #FunctionalProgramming
- La conjetura de Merterns y su relación con un número tan raro como extremada y colosalmente grande. ~ @Alvy. #Matemáticas
- The benefits of sequent calculus. ~ Étienne Miquey. #Logic #CompSci
- Curry-Howard: unveiling the computational content of proofs. ~ Étienne Miquey. #Logic #CompSci
- Realizabilidad clásica y efectos colaterales: Extendiendo la correspondencia de Curry-Howard. ~ Étienne Miquey. #Logic #CompSci
- Introduction to Coq. ~ Assia Mahboubi. #ITP #Coq
- First steps with Coq. ~ Assia Mahboubi. #ITP #Coq
- Programming with dependent types in Coq: inductive families and dependent patter-matching. ~ Matthieu Sozeau. #ITP #Coq
- Homotopy Type Theory. ~ Nicolas Tabareau. #ITP #Coq #HoTT
- Set Theory vs. Type Theory. Alexandre Miquel. #Logic #CompSci
- Profunctor optics, a categorical update. ~ Bryce Clarke et als. #Haskell #FunctionalProgramming
- Multiple address spaces in a distributed capability system. ~ Nora Hossle. #MsC_Thesis #Haskell #FunctionalProgramming
- Coherence via wellfoundedness. ~ Nicolai Kraus, Jakob von Raumer. #ITP #LeanProver #Math
- Formalizing the Curry-Howard correspondence. ~ Juan Ferrer Meleiro, Hugo Luiz Mariano. #ITP #Idris #Logic
- A sketch of categorical relation algebra combinators in Z3Py. ~ Philip Zucker (@SandMouth). #Z3 #SMT
- Primeros pasos con Nix: un Linux más funcional. ~ Adrián Arroyo Calle. #Nix #Linux #FunctionalProgramming
- Case study: migrating from lens to optics. ~ Oleg Grenrus (@phadej). #Haskell #FunctionalProgramming
- TEpla: A certified type enforcement access-control policy language. ~ Amir Eaman. #PhD_Thesis #ITP #Coq
- Elaborating dependent (co)pattern matching: No pattern left behind. ~ Jesper Cockx, Andreas Abel. #ITP #Agda
- The Cantor-Schröder-Bernstein theorem for ∞-groupoids. ~ Martin Escardo. #ITP #Agda #Math
- FASiM: A framework for automatic formal analysis of simulink models of linear analog circuits. ~ Adnan Rashid, Ayesha Gauhar and Osman Hasan. #ITP #HOL_Light
- Transformations on applicative concurrent computations. ~ Román González. #Haskell #FunctionalProgramming
- The beauty of abstraction in mathematics. ~ Thomas Lingefjärd, Russell Hatami. #Math
- Formalization of forcing in Isabelle/ZF. ~ Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf. #ITP #IsabelleZF #Logic
- HolPy: Interactive theorem proving in Python. ~ Bohua Zhan. #ITP #HolPy #Logic #Python
- Org-mode features you may not know. ~ Bastien Guerry (@bzg2). #Emacs #OrgMode
- Smart induction for Isabelle/HOL (System description). ~ Yutaka Nagashima. #ITP #IsabelleHOL
- Show that a monic (injective) and epic (surjective) function has an inverse in Coq. ~ Arthur Azevedo De Amorim. #ITP #Coq #Math
- Mechanized proofs for PL: Past, present, and future. ~ Talia Ringer. #ITP
- Profunctor optics: The categorical view. ~ Emily Pillmore and Mario Román. #Haskell #FunctionalProgramming #CategoryTheory
- vmap in Haskell. ~ Edward Z. Yang (@ezyang). #Haskell #FunctionalProgramming
- Developing GHC for a Living: Interview with Vladislav Zavialov. ~ Denis Oleynikov. #Haskell #FunctionalProgramming
- Terminating tricky traversals. ~ Donnacha Oisín Kidney (@oisdk). #Haskell #Agda #FunctionalProgramming
- Locating performance bottlenecks in large Haskell codebases. ~ Juan Raphael Diaz Simões. #Haskell #FunctionalProgramming
- A certificate-based approach to formally verified approximations. ~ Florent Bréhard, Assia Mahboubi, Damien Pous. #ITP #Coq #Math
- Combining predicate transformer semantics for effects: a case study in parsing regular languages. ~ Tim Baanen, Wouter Swierstra. #Agda #FunctionalProgramming
- Searching the space of representations: reasoning through transformations for mathematical problem solving. ~ Daniel Raggi. #PhD_Thesis #ITP #IsabelleHOL
- Introduction and formalization of Boolean algebra. ~ Boro Sitnikovski (@BSitnikovski). #ITP #Metamath #Math
- Property testing in depth: The size parameter. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming
- A Pythonista’s Review of Haskell. ~ Ying Wang. #Haskell #Python