Lecturas del Grupo de Lógica Computacional
Este repositorio es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional. La recopilación está ordenada por la fecha de su publicación en la lista. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.
Contenido
Lecturas del año 2020
Febrero de 2020
02-Feb-20
- Completeness theorems for first-order logic analysed in constructive type theory. ~ Yannick Forster, Dominik Kirst, Dominik Wehr. #ITP #Coq #Logic
- Hilbert’s tenth problem in Coq. ~ Dominique Larchey-Wendling, Yannick Forster. #ITP #Coq #Math
- Beyond notations: Hygienic macro expansion for theorem proving languages. ~ Sebastian Ullrich, Leonardo de Moura. #ITP #LeanProver
- MOIN: A nested sequent theorem prover for intuitionistic modal logics (system description). ~ Marianna Girlando, Lutz Straßburger. #ATP #Prolog #Logic
01-Feb-20
- A certifying extraction with time bounds from Coq to call-by-value λ-calculus. ~ Yannick Forster, Fabian Kunze. #ITP #Coq
- The weak call-by-value λ-calculus is reasonable for both time and space. ~ Yannick Forster, Fabian Kunze, Marc Roth. #ITP #Coq
- Verified programming of Turing machines in Coq. ~ Yannick Forster, Fabian Kunze, Maximilian Wuttke. #ITP #Coq
- Computational type theory and interactive theorem proving with Coq (Version of August 2, 2019). ~ Gert Smolka. #eBook #ITP #Coq #Logic
- Towards a readable formalisation of category theory. ~ Greg O’Keefe. #ITP #IsabelleHOL #CategoryTheory
- A hierarchy of algebras for boolean subsets. ~ Walter Guttmann, Bernhard Möller. #ITP #IsabelleHOL #Math
- Formal specification, monitoring, and verification of autonomous vehicles in Isabelle/HOL. ~ Albert Rizaldi. #PhD_Thesis #ITP #IsabelleHOL
- Ulam spirals. ~ Ken T Takusagawa. #Haskell #FunctionalProgramming
- Karp’s 21 NP-complete problems. #CompSci
- NP-completeness, part I. ~ Kevin Buchin. #CompSci
- NP-completeness, part II. ~ Kevin Buchin. #CompSci
Enero de 2020
31-Ene-20
- 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
30-Ene-20
- 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
28-Ene-20
- 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
27-Ene-20
- 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
26-Ene-20
- 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
25-Ene-20
- 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
24-Ene-20
- 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
23-Ene-20
- For beginners. ~ Julie Moronuki (@argumatronic). #Haskell #FunctionalProgramming
- Drawing Prolog search trees: A manual for teachers and students of logic programming. ~ Johan Bos. #Prolog #LogicProgramming
22-Ene-20
- 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
21-Ene-20
- 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
20-Ene-20
- 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
19-Ene-20
- 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
18-Ene-20
- 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
17-Ene-20
- 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
16-Ene-20
- 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
15-Ene-20
- 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
14-Ene-20
- 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
13-Ene-20
- 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
12-Ene-20
- 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
11-Ene-20
- 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
10-Ene-20
- 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
09-Ene-20
- 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 #Isabelle
08-Ene-20
- Haskell language extension taxonomy. ~ Doug Beardsley. #Haskell #FunctionalProgramming
07-Ene-20
- 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
06-Ene-20
- Organizing our package! ~ James Bowen (@james_OWA). #Haskell #Cabal #FunctionalProgramming
05-Ene-20
- 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
04-Ene-20
- Lean versus Coq: The cultural chasm. ~ Ramkumar Ramachandra. #ITP #LeanProver #Coq
03-Ene-20
- 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
02-Ene-20
- 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
01-Ene-20
- 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