Resumen de lecturas compartidas durante febrero de 2020
Esta entrada es una recopilación de lecturas compartidas, durante febrero 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.
- 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
- 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
- A formal development cycle for security engineering in Isabelle. ~ Florian Kammüller. #ITP #IsabelleHOL
- Automated proof of Bell-LaPadula security properties. ~ Maximiliano Cristiá, Gianfranco Rossi. #ATP #SetLog
- List of open and free logic textbooks. ~ Richard Zach (@RrrichardZach). #Logic
- Intro to Kaleidoscopes: Optics for aggregating data through Applicatives. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming
- Nix: Functional package management! ~ James Bowen (@james_OWA). #Nix
- A comprehensive framework for saturation theorem proving (Technical report). ~ Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette. #ITP #IsabelleHOL #Logic
- jsCoq: A port of Coq to Javascript (Run Coq in your browser). ~ Emilio Jesús Gallego Arias (@ejgallego). #ITP #Coq
- Why monad composes operations sequentially. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming
- Los primos de la conjetura de Collatz. ~ Francisco R. Villatoro (@emulenews). #Matemáticas
- Free and open-source textbooks. ~ Dana C. Ernst. #eBooks #Math
- How I created my website with Org mode. ~ John Borwick (@borwick). #Emacs #OrgMode
- VERONICA: Expressive and precise concurrent information flow security (Extended version with technical appendices). ~ Daniel Schoepe, Toby Murray, Andrei Sabelfeld. #ITP #IsabelleHOL
- A formal system of axiomatic set theory in Coq. ~ Tianyu Sun, Wensheng Yu. #ITP #Coq #Math
- Trakhtenbrot’s theorem in Coq (A constructive approach to finite model theory). ~ Dominik Kirst, Dominique Larchey-Wendling. #ITP #Coq #Logic
- ZZ (drunk octopus) is a modern formally provable dialect of C, inspired by Rust. ~ Arvid E. Picciani. #ZZ #Programming #SMT #FormalVerification
- Java & Haskell: Similarities and differences. ~ Dervis Mansuroglu (@dervis_m). #Java #Haskell
- Proofs, computability, complexity, and the lambda calculus (An introduction). ~ Jean Gallier, Jocelyn Quaintance. #eBook #Logic #CompSci #LambdaCalculus
- An algorithms course with minimal prerequisites. ~ Adam Sheffer. #Algorithms
- Computer-supported analysis of arguments in climate engineering. ~ David Fuenmayor, Christoph Benzmüller. #ITP #IsabelleHOL.
- Implementing and certifying a Web server in Coq. ~ Thomas Letan. #ITP #Coq
- Finkel: Haskell in S-expression. #Haskell #Lisp #Finkel_lang
- Safe memory management in inline-java using linear types. ~ Facundo Dominguez. #Haskell #FunctionalProgramming
- Functional or combinator parsing. ~ Graham Hutton (@haskellhutt). #Haskell #FunctionalProgramming
- Learning algorithmic techniques: dynamic programming. ~ Eric P. Hanson. #Algorithms #Programming #JuliaLang
- Toward a mechanized compendium of gradual typing. ~ Jeremy G. Siek. #ITP #Agda
- Introduction to univalent foundations of mathematics with Agda. ~ Martín Hötzel Escardó. #ITP #Agda #Math
- Formalizing functional analysis structures in dependent type theory. ~ Reynald Affeldt et als. #ITP #Coq #Math
- A formal verification framework for security issues of blockchain smart contracts. ~ Tianyu Sun, Wensheng Yu. #ITP #Coq #Blockchain
- Lorentz: Implementing smart contract eDSL in Haskell. ~ Kostya Ivanov. #Haskell #FunctionalProgramming
- Thinking in types. ~ Pat Brisbin (@patbrisbin). #Haskell #FunctionalProgramming via @lettier
- Functional programming: The simple version. ~ Muhammad Tabaza (@Tabz_98). #Haskell #FunctionalProgramming via @SWTechDev
- Advanced Functional Programming concepts made easy. ~ Tal Joffe (@TalJoffe). #FunctionalProgramming #JavaScript
- Competitive Programming in Haskell: primes and factoring. ~ Brent Yorgey. #Haskell #FunctionalProgramming
- Type classes and filters for mathematical analysis in Isabelle/HOL. ~ Johannes Hölzl, Fabian Immler, Brian Huffman. #ITP #IsabelleHOL #Math
- Lean is better for proper maths than all the other theorem provers. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
- Where is the fashionable mathematics? ~ Kevin Buzzard (@XenaProject). #Math #ITP #LeanProver #Coq #IsabelleHOL
- An experimental study of formula embeddings for automated theorem proving in first-order logic. ~ Ibrahim Abdelaziz et als. #ATP #MachineLearning
- Automated reasoning I. ~ Uwe Waldmann. #eBook #ATP #Logic
- Automated reasoning II. ~ Sophie Tourret, Uwe Waldmann. #eBook #ATP #Logic
- Verificación de estructura de redes neuronales profundas en tiempo de compilación (Proyecto TensorSafe). ~ Leonardo Piñeyro. #Haskell #DeepLearning
- MateFun: Functional Programming and Math with adolescents. ~ Alejandra Carboni et als. #Haskell #FunctionalProgramming #Math
- Mejoras al intérprete MateFun. ~ Nicolás Vázquez. #Haskell #FunctionalProgramming #Math
- Template Haskell tutorial. ~ Mark Karpov (@mrkkrp). #Haskell #FunctionalProgramming
- Imperative Haskell. ~ Vaibhav Sagar. #Haskell #FunctionalProgramming
- Typeable and Data in Haskell. ~ Chris Done (@christopherdone). #Haskell #FunctionalProgramming
- Arithmetic progressions and relative primes. ~ José Manuel Rodríguez Caballero. #ITP #IsabelleHOL #Math
- Tutoriel: types de données, fonctions et preuves en Isabelle. ~ Frédéric Boulanger. #ITP #IsabelleHOL
- Cours: Sémantique des langages. ~ Frédéric Boulanger. #ITP #IsabelleHOL
- How small can we make a useful type theory? ~ Pedro Abreu (@etapedro). #ITP #Coq #Cedille #FunctionalProgramming
- Coquedille: A Coq to Cedille transpiler written in Coq. ~ Pedro Abreu (@etapedro). #ITP #Coq #Cedille #FunctionalProgramming
- How laziness works. #Haskell #FunctionalProgramming
- An introduction to recursion schemes. ~ Patrick Thomson. #Haskell #FunctionalProgramming
- Counterexamples of type classes. ~ Phil Freeman. #Haskell #Purescript #FunctionalProgramming
- Compiling Haskell to JavaScript, not in the way you’d expect. ~ Oleg Grenrus (@phadej). #Haskell #FunctionalProgramming #JavaScript
- Converting Cabal to Nix! ~ James Bowen (@james_OWA). #Haskell #Cabal #Nix
- Liquidate your assets (Reasoning about resource usage in Liquid Haskell). ~ Niki Vazou (@nikivazou). #Haskell
- State will do. ~ Willem Seynaeve, Koen Pauwels and Tom Schrijvers. #Haskell #FunctionalProgramming
- PaSe: An extensible and inspectable DSL for micro-animations. ~ Ruben P. Pieters and Tom Schrijvers. #Haskell #FunctionalProgramming
- Physics, History and Haskell. (Interview with Rinat Stryungis). ~ Denis Oleynikov. #Haskell #FunctionalProgramming
- A DSL for fluorescence microscopy. Birthe van den Berg, Peter Dedecker, Tom Schrijvers. #Haskell #FunctionalProgramming
- A proof assistant based formalisation of core Erlang. ~ Péter Bereczky, Dániel Horpácsi and Simon Thompson. #ITP #Coq #Erlang
- An equational modeling of asynchronous concurrent programming. ~ David Janin. #Haskell #FunctionalProgramming
- BinderAnn: Automated reification of source annotations for monadic EDSLs. ~ Agustín Mista and Alejandro Russo. #Haskell #FunctionalProgramming
- Formalization of cost and utility in Microeconomics. ~ Asad Ahmed, Osman Hasan, Falah Awwad, and Nabil Bastaki. #ITP HOL_Light
- Haskell in production: Riskbook (an interview with Jezen Thomas). ~ Gints Dreimanis. #Haskell #FunctionalProgramming
- Generalized Algebraic Data Types and Data Kinds. ~ Andre Popovitch (@PopovitchAndre). #Haskell #FunctionalProgramming
- Utilización de registros en Emacs. #Emacs
- Generating next step hints for task oriented programs using symbolic execution. ~ Nico Naus and Tim Steenvoorden. #Haskell #FunctionalProgramming
- Mac Lane’s comparison theorem for the Kleisli construction formalized in Coq. ~ Burak Ekici, and Cezary Kaliszyk. #ITP #Coq
- Functional programming in OCaml. ~ Michael R. Clarkson. #eBook #OCaml #FunctionalProgramming
- Practical Common Lisp. ~ Peter Seibel. #eBook #CommonLisp
- Maintainable software architecture in Haskell (with Polysemy). ~ Paweł Szulc (@EncodePanda). #Haskell #FunctionalProgramming
- The Logic course adventure (An active learning textbook for formal logic). ~ Ian Schnee. #eBook #Logic
- Awesome Coq Awesome (A curated list of awesome Coq libraries, plugins, tools, and resources). #ITP #Coq
- Equality of functions in Agda. ~ Mark Armstrong. #ITP #Agda #FunctionalProgramming via @armk_eh
- Equality in mechanized mathematics. ~ Ramkumar Ramachandra. #ITP #Coq #Math
- Porting to Rio. ~ Colin Woodbury (@fosskers). #Haskell #FunctionalProgramming
- Competitive programming in Haskell: modular arithmetic, part 1. ~ Brent Yorgey. #Haskell #FunctionalProgramming #Math
- There and Back Again (TABA). ~ Olivier Danvy, and Mayer Goldberg. #Programming #Algoritms
- Typing TABA (There and Back Again). ~ Donnacha Oisín Kidney (@oisdk). #Haskell #FunctionalProgramming
- Profunctor optics, a categorical update. ~ Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregian, Bartosz Milewski, Emily Pillmore, and Mario Román. #Haskell #FunctionalProgramming
- How to start using Python type annotations with Mypy. ~ Carlos Villavicencio. #Python #Mypy
- Teaching natural deduction as a subversive activity. ~ James Caldwell. #Logic
- Certifications of programs with computational effects. ~ Burak Ekici. #PhD_Thesis #ITP #Coq
- Certification of nonclausal connection tableaux proofs. ~ Michael Färber, and Cezary Kaliszyk. #ITP #HOL_Light
- Flexible coinduction in Agda. ~ Luca Ciccone. #MSc_Thesis #ITP #Agda
- What I wish I knew when learning Haskell (Version 2.5). ~ Stephen Diehl (@smdiehl). #Haskell #FunctionalProgramming
- Categorical combinators for Graphviz in Python. ~ Philip Zucker (@SandMouth). #Python
- How to make mondrian art in Haskell (Unleash your inner functional artist). ~ Marc Fichtel (@mc_razzy). #Haskell #FunctionalProgramming
- 3 tribes of programming. ~ Joseph Gentle (@josephgentle). #Programming
- Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi. ~ Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. #ITP #Coq
- Signatures and induction principles for higher inductive-inductive types. ~ Ambrus Kaposi, and András Kovács. #ITP #Agda #Haskell #FunctionalProgramming
- From Curry to Haskell. ~ Felice Cardone. #Haskell #FunctionalProgramming #Logic
- A Why3 proof of GMP algorithms. ~ Raphaël Rieu-Helft. #Why3 #FormalVerification
- mCoq: Mutation analysis for Coq verification projects. ~ Kush Jain et als. #ITP #Coq
- Most popular programming languages 1965-2019. #Programming
- Programming algorithms: Compression. ~ Vsevolod Dyomkin. #Algorithms #CommonLisp
- On linear types and exceptions. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming
- A Lisp programmer living in Python-land: The Hy programming language. ~ Mark Watson. #eBook #Programing #Lisp #Python #Hy
- Isabelle/HOL and Proof General reference [Isabelle/HOL support wiki]. #ITP #IsabelleHOL
- Agda vs. Coq vs. Idris. #ITP #Agda #Coq #Idris
- Type witnesses in Haskell. ~ Sandeep Chandrika. #Haskell #FunctionalProgramming
- “Papers we love” is a repository of academic computer science papers and a community who loves reading them. @papers_we_love #CompSci
- Papers from the computer science community to read and discuss. #CompSci
- Scheme: An interpreter for extended lambda calculus (1975). ~ Gerald J. Sussman, and Guy L. Steele. #Programming #Scheme #CompSci
- What is a knowledge representation?. ~ Randall Davis, Howard Shrobe, and Peter Szolovits (1993). #KR #AI
- An axiomatic basis for computer programming. ~ C.A.R. Hoare (1969). #CompSci
- Why functional programming matters. ~ John Hughes (1989). #FunctionalProgramming #CompSci
- A tutorial on the universality and expressiveness of fold. ~ Graham Hutton (1999). #FunctionalProgramming #Haskell
- QuickCheck: Α lightweight tool for random testing of Haskell programs. ~ Koen Claessen and John Hughes (2000). #Haskell #FunctionalProgramming
- Computational lambda-calculus and monads. ~ Eugenio Moggi (1988). #CompSci
- Infinite sets that admit fast exhaustive search. ~ Martı́n Escardó (2007). #Haskell #FunctionalProgramming
- Monoids: Theme and variations (Functional Pearl). ~ Brent A. Yorgey (2012). #Haskell #FunctionalProgramming
- QuickCheck testing for fun and profit. ~ John Hughes (2007). #Haskell #FunctionalProgramming
- The mechanical evaluation of expressions. ~ P.J. Landin (1964). #CompSci
- On computable numbers, with an application to the Entscheidungsproblem. ~ A.M. Turing (1937). #CompSci #Math
- Propositions as types. ~ Philip Wadler (2014). #Logic #CompSci
- Recursive functions of symbolic expressions and their computation by machine, Part I. ~ John McCarthy (1960). #CompSci #Lisp
- Fundamental concepts in programming languages. ~ Christopher Strachey (2000). #CompSci
- Graph theory in Coq: Minors, treewidth, and isomorphisms. ~ Christian Doczkal and Damien Pous. #ITP #Coq #Math
- Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq. ~ Christian Doczkal, and Damien Pous. #ITP #Coq #Math
- Pensamientos de Antonio Machado. ~ Guiomar Godoy. #Filosofía
- A selected bibliography on formalised mathematics. ~ Laurent Théry. #ITP #Math
- A machine-checked constructive metatheory of computation tree logic. ~ Christian Doczkal (2016). #PhD_Thesis #ITP #Coq #Logic
- Course: Machine-checked Mathematics. ~ Assia Mahboubi. #ITP #Coq #Math
- On memory addressing. ~ Reto Achermann. #PhD_Thesis #ITP #IsabelleHOL
- Experiences from exporting major proof assistant libraries. ~ Michael Kohlhase, and Florian Rabe. #ITP #Coq #HOL_Light #IsabelleHOL #Mizar #PVS #MMT
- Flexible coinduction in Agda. ~ Luca Ciccone. #MSc_Thesis #ITP #Agda
- Various new theorems in constructive univalent mathematics written in Agda. ~ Martín Escardó. #ITP #Agda #Math
- The Cantor-Schröder-Bernstein Theorem for ∞-groupoids. ~ Martı́n Escardó. #ITP #Agda #Math
- Translation from FOL to LTL+Past and LTL, via separation of LTL+Past. ~ Daniel Oliveira. #Logic #Haskell #FunctionalProgramming
- Linear temporal logic: separation and translation. ~ Daniel Oliveira. #MSc_Thesis #Logic #Haskell #FunctionalProgramming
- Revisiting separation: Algorithms and complexity. ~ Daniel Oliveira, and João Rasga. #Logic #Haskell #FunctionalProgramming
- Sobre listas y atoms. #Emacs #Elisp
- Isabelle/Spartan: A dependent type theory framework for Isabelle. ~ Joshua Chen. #ITP #IsabellleHOL #HoTT
- Implementing the Goodstein function in λ-calculus. ~ Bertram Felgenhauer. #ITP #IsabelleHOL
- Testing higher-order properties with QuickCheck. ~ Li-yao Xia (@lysxia). #Haskell #FunctionalProgramming #QuickCheck
- Another breadth-first traversal. ~ Donnacha Oisín Kidney (@oisdk). #Haskell #FunctionalProgramming
- Lectures on scientific computing with Python. ~ Robert Johansson (2017). #Python
- Machine Learning in Python: Main developments and technology trends in data science, machine learning, and artificial intelligence. ~ Sebastian Raschka, Joshua Patterson, Corey Nolet. #MachineLearning #AI #Python
- Category theory as a tool for thought. ~ Daniel Beskin. #CategoryTheory #FunctionalProgramming #Haskell
- The scientific paper is outdated (For the sake of research, their careers, and their mental health, scientists should spend more time developing software). ~ Ryan Abernathey. #
- A mechanised semantics for HOL with ad-hoc overloading. ~ Johannes Åman Pohjola, Arve Gengelbach. #ITP #HOL4
- A generic framework for verified compilers in Isabelle/HOL. ~ Martin Desharnais. #ITP #IsabelleHOL
- An analysis of programming paradigms in high-level synthesis tools. ~ Pieter Staal. #Haskell #FunctionalProgramming
- Marlowe: implementing and analysing financial contracts on blockchain. ~ Pablo Lamela Seijas et als. #Haskell #ITP #IsabelleHOL #Blockchain #Cardano
- A machine-checked C implementation of Dijkstra’s shortest path algorithm. ~ Anshuman Mohan, Shengyi Wang, and Aquinas Hobor. #ITP #Coq
- Formal verification of hardware components in critical systems. ~ Wilayat Khan et als. #ITP #Coq
- MMT: The Meta Meta Tool (system description). ~ Florian Rabe. #ITP #MMT
- Type-based formal verification. ~ Alejandro Serrano (@trupill). #Haskell #Verification
- Probabilistic programming with monad‑bayes, Part 3: A bayesian neural network. ~ Siddharth Bhat, Simeon Carstens, Matthias Meschede. #Haskell #FunctionalProgramming
- Short proof of Menger’s theorem in Coq (Proof Pearl). ~ Christian Doczka. #ITP #Coq #Math
- Proof-reconstruction in type theory for propositional logic. ~ Jonathan Prieto-Cubides, Andrés Sicard-Ramírez. #ITP #Agda #Metis #Logic
- Athena: a tool that translates Metis ATP proofs to the Agda programming language to check their correctness. ~ Jonathan Prieto-Cubides. #Haskell #ITP #Agda #Metis #Logic
- agda-prop: A library for classical propositional logic in Agda. ~ Jonathan Prieto-Cubides. #ITP #Agda #Logic
- agda-metis: Metis prover reasoning for propositional logic in Agda. ~ Jonathan Prieto-Cubides. #ITP #Agda #Metis
- The natural deduction pack. ~ Alastair Carr. #Logic
- Highly automated formal proofs over memory usage of assembly code. ~ Freek Verbeek et als. #ITP #IsabelleHOL
- Math is your insurance policy. ~ Bartosz Milewski (@BartoszMilewski). #Programming
- Automating the generation of high school geometry proofs using Prolog in an educational context. ~ Ludovic Font et als. #Prolog #LogicProgramming #Math
- A mobile application for self-guided study of formal reasoning. ~ David M. Cerna, Rafael P.D. Kiesel, Alexandra Dzhiganskaya. #Logic #Teaching #Android
- Tools in term rewriting for education. ~ Sarah Winkler, Aart Middeldorp. #Logic #Teaching
- Teaching a formalized logical calculus. ~ Asta Halkjær From et als. #Logic #Teaching #ITP #IsabelleHOL
- Structure and interpretation of computer programs — JavaScript adaptation. #eBook #JavaScript #SICP
- Mathematical structures. ~ Contributors of math.chapman.edu. #Math
- Reductions and jokes. ~ R.J. Lipton & K.W. Regan. #CompSci #Math
- Mathematical humor. ~ Andrej and Elena Cherkaev. #Math