Resumen de lecturas compartidas durante julio de 2020
Esta entrada es una recopilación de lecturas compartidas, durante julio 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.
- The complex number game, levels 1 to 3. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
- Logic and computation intertwined. ~ Prabhakar Ragde (@plragde). #eBook #Logic #ITP #Agda #Coq
- Teach yourself Racket. ~ Prabhakar Ragde (@plragde). #eBook #Racket #FunctionalProgramming
- Functional data structures. ~ Prabhakar Ragde (@plragde). #eBook #OCaml #FunctionalProgramming #Algorithms
- Certifying the weighted path order. ~ R. Thiemann, J. Schöpf, C. Sternagel, A. Yamada. #ITP #IsabelleHOL
- Notes on “Programming language foundations in Agda”. ~ Prabhakar Ragde (@plragde). #eBook #ITP #Agda
- Dependent types and software verification. ~ Prabhakar Ragde (@plragde). #ITP #Agda
- Proust: A nano proof assistant. ~ Prabhakar Ragde (2016). #Logic #Racket #ITP #Proust
- Functional Pearls: Composable data visualizations. ~ T. Petricek. #FunctionalProgramming #Fsharp
- Total functional programming. ~ D.A. Turner (2004). #FunctionalProgramming
- Higher-order Logic as Lingua franca (Integrating argumentative discourse and deep logical analysis). ~ David Fuenmayor, Christoph Benzmüller. #ITP #IsabelleHOL
- Equality, specifications, and implementations. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math #CompSci
- Modeling state machines with dependent types in Haskell: Part 1. ~ Evgeny Poberezkin (@epoberezkin). #Haskell #FunctionalProgramming
- Abstract algebra cheatsheet: a visual summary of key structures in abstract algebra. ~ Matthias Vallentin. #Math
- Reasoning about algebraic structures with implicit carriers in Isabelle/HOL. ~ W. Guttmann. #ITP #IsabelleHOL #Math
- Binary intersection formalized. ~ Štěpán Holub, Štěpán Starosta. #ITP #IsabelleHOL
- The hydra and the rooster. ~ Pirre Castéran. #ITP #Coq #Math
- Teaching automated theorem proving by example: PyRes 1.2: (System description). ~ S. Schulz, A. Pease. #ATP #Logic #Python
- Unification in Julia. ~ Philip Zucker (@SandMouth). #Logic #JuliaLang
- Some thoughts on building software. ~ Alejandro Serrano (@trupill). #FuncionalProgramming #Haskell
- Sphere eversion. ~ Ricky Reusser. #Math
- Formalizing a Seligman-style tableau system for hybrid logic. ~ Asta Halkjær From, Patrick Blackburn, Jørgen Villadsen. #ITP #IsabelleHOL #Logic
- Prawf: An interactive proof system for program extraction. ~ Ulrich Berger, Olga Petrovska, Hideki Tsuiki. #ITP #Haskell #FunctionalProgramming #Logic
- Formalizing the face lattice of polyhedra. ~ Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub. #ITP #Coq #Math
- The mechanization of Mathematics. ~ Jeremy Avigad (2018). #ITP #Math
- Category theory in the E automated theorem prover. ~ Philip Zucker (@SandMouth). #ATP #CategoryTheory
- Division by zero in type theory: a FAQ. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
- Formal topology in Univalent Foundations. ~ Ayberk Tosun. #MsC_Thesis #ITP #Agda #Math
- Certifying time complexity of Agda programs using complexity signatures. ~ Christian Bach Møllnitz, Johannes Elgaard, Simon Rannes. #Agda #FunctionalProgramming
- Scientific proof-oriented programming (S-pop). ~ Philip Thrift (@philipthrift). #CompSci
- Retrie: Haskell refactoring made easy. #Haskell #FunctionalProgramming
- Lean for the curious mathematician: A virtual workshop on computer-checked mathematics [13–17 July 2020]. #ITP #LeanProver #Math
- Theorems in transcendental number theory. ~ Jujian Zhang. #ITP #LeanProver #Math
- La conjetura de Gilbreath. ~ Juan Arias de Reyna. #Matemáticas
- Introduction to Univalent Foundations of Mathematics with Agda. ~ Martín Hötzel Escardó. #ITP #Agda #Math
- A survey on theorem provers in formal methods. 4 M. Saqib Nawaz, Moin Malik, Yi Li, Meng Sun and M. Ikram Ullah Lali. #ITP #ATP #FormalMethods
- A survey of languages for formalizing mathematics. ~ Cezary Kaliszyk, Florian Rabe. #ITP #Math
- A micro prover for teaching automated reasoning. ~ J. Villadsen. #ITP #IsabelleHOL #Logic
- Textbook mathematics in the Naproche-SAD system. ~ P. Koepke. #ITP #Math
- Formal analysis of unmanned aerial vehicles using higher-order-logic theorem proving. ~ Sa’ed Abed, Adnan Rashid, Osman Hasan. #ITP #HOL_Light
- Animated logic: Correct functional conversion to conjunctive normal form. ~ António Ravara, Mário Pereira, Pedro Barroso. #Logic #Why3
- Testing Mizar user interactivity in a University-level introductory course on foundations of Mathematics. ~ Adam Naumowicz. #ITP #Mizar #Math
- Strong extension-free proof systems. ~ Marijn J H Heule, Benjamin Kiesl, Armin Biere. #SAT
- Online convex optimization with Haskell. ~ Valentin Reis. #Haskell #FunctionalProgramming #Math
- Competitive programming in Haskell: 2D cross product, part 1. ~ Brent Yorgey. #Haskell #FunctionalProgramming
- Type safety in two easy lemmas. ~ Jeremy Siek (@jeremysiek). #ITP #Agda
- Performance of Haskell Array libraries through Canny edge detection. ~ Alexey Kuleshevich. #Haskell #FuncionalProgramming
- Learning selection strategies in Buchberger’s algorithm. ~ Dylan Peifer, Michael Stillman, Daniel Halpern-Leistner. #MachineLearning #Math
- Por qué Matemáticas ha pasado de ser una carrera minoritaria a una de las más codiciadas y de moda. ~ Carlos Prego. #Matemáticas
- Deriving the State monad from first principles. ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming
- Adventures in verifying arithmetic. ~ John Harrison. #ITP #HOL_Light #Math
- The natural number game : an introduction to Lean tactics. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
- The ten (or so) basic tactics. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver
- Infinitude of primes: a Lean theorem prover demo. ~ Scott Morrison. #ITP #LeanProver #Math
- Certifying emptiness of timed Büchi automata. ~ Simon Wimmer, Frédéric Herbreteau, Jaco van de Pol. #ITP #IsabelleHOL
- Development of a tropical algebraic geometry package in the Haskell programming language. ~ Fernando Patricio Zhapa Camacho. #PhD_Thesis #Haskell #FunctionalProgramming #Math
- Optimization of Wu’s algorithm for the elimination of polynomial variables by High-Performance Computing (HPC). ~ José Luis Seraquive Cuenca. #Haskell #FunctionalProgramming #Math
- Record constructors. ~ G. Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming
- Qualified do: rebind your do-notation the right way. ~ Matthías Páll Gissurarson, Facundo Domínguez, Arnaud Spiwack. #Haskell #FunctionalProgramming
- Metaprogramming in Lean. ~ Robert Y. Lewis. #ITP #LeanProver
- A one-line proof of the infinitude of primes. ~ Jason Orendorff. #ITP #LeanProver #Math
- A Lean tactic for normalising ring expressions with exponents. ~ Anne Baanen. #ITP #LeanProver #Math
- Formalization of forcing in Isabelle/ZF. ~ Pedro Sánchez Terraf. #ITP #Isabelle #Math
- The resolution of Keller’s conjecture. ~ Marijn Heule. #ATP #SAT_Solver #Math
- Mathematics in Lean introduction. ~ Patrick Massot. #ITP #LeanProver #Math #LftCM2020
- Logic in Lean. ~ Jeremy Avigad. #ITP #LeanProver #Math #LftCM2020
- Numbers in Lean. ~ Rob Lewis. #ITP #LeanProver #Math #LftCM2020
- Sets in Lean. ~ Jeremy Avigad. #ITP #LeanProver #Math #LftCM2020
- Structures and classes in Lean. ~ Floris van Doorn. #ITP #LeanProver #Math #LftCM2020
- Building an algebraic hierarchy in Lean. ~ Kevin Buzzard. #ITP #LeanProver #Math #LftCM2020
- Lean at Mathcamp 2020. ~ Apurva Nakade, Jalex Stark. #ITP #LeanProver #Math
- Building the topological hierarchy in Lean. ~ Alex Best. #ITP #LeanProver #Math #LftCM2020
- PubSub implementation in Haskell with formal verification in Coq. ~ Boro Sitnikovski, Biljana Stojcevska, Lidija Goracinova-Ilieva, Irena Stojmenovska. #Haskell #FunctionalProgramming #ITP #Coq
- Haskell style guide. ~ Kowainik. #Haskell #FunctionalProgramming
- Forbidden Haskell types. ~ Ashley Yakeley. #Haskell #FunctionalProgramming
- The evolution of a Scheme programmer. ~ Erkin Batu Altunbaş. #Programming #Scheme
- Managing Haskell extensions. ~ Neil Mitchell (@ndm_haskell). #Haskell #FunctionalProgramming
- Optimizing ray tracing in Haskell. ~ Sarfaraz Nawaz. #Haskell #FunctionalProgramming
- Order structures in Lean. ~ Kevin Buzzard. #ITP #LeanProver #Math #LftCM2020
- Groups, rings, and fields in Lean. ~ Johan Commelin. #ITP #LeanProver #Math #LftCM2020
- Lean for the Curious Mathematician 2020. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math #LftCM2020
- Linear algebra in Lean. ~ Anne Baanen.c#ITP #ITP #LeanProver #Math #LftCM2020
- Category theory in Lean. ~ Scott Morrison. #ITP #LeanProver #Math #LftCM2020
- Topology and filters in Lean. ~ Patrick Massot. #ITP #LeanProver #Math #LftCM2020
- Calculus and integration in Lean. ~ Yury Kudryashov. #ITP #LeanProver #Math #LftCM2020
- Simplifying casts and coercions. ~ Robert Y. Lewis, Paul-Nicolas Madelaine. #ITP #LeanProver
- Competitive programming in Haskell: cycle decomposition with mutable arrays. ~ Brent Yorgey. #Haskell #FunctionalProgramming
- Differential geometry in Lean. ~ Sebastien Gouëzel. #ITP #LeanProver #Math #LftCM2020
- Verification of ML systems via reparameterization. ~ Jean-Baptiste Tristan et als. #ITP #LeanProver #MachineLearning
- Modal FRP For All (Functional reactive programming without space leaks in Haskell). ~ Patrick Bahr. #Haskell #FunctionalProgramming #ITP #Coq
- Contributions to a science of contemporary mathematics. ~ Frank Quinn. #Math
- Metamath Zero: Designing a theorem prover prover. ~ Mario Carneiro. #ITP #MethamathZero0
- A promising path towards autoformalization and general Artificial Intelligence. ~ Christian Szegedy. #MKM #AI #ITP #MachineLearning0
- Graphics in Haskell: linear algebra. ~ David Alexander Stuart. #Haskell #FunctionalProgramming #Math
- How to read Haskell Documentation. Step by step guide. ~ Theofanis Despoudis. #Haskell #FunctionalProgramming
- Formalizing graph trail properties in Isabelle/HOL. ~ Laura Kovács, Hanna Lachnitt, Stefan Szeider. #ITP #IsabelleHOL #Math0
- Leveraging the information contained in theory presentations. ~ Jacques Carette, William M. Farmer, Yasmine Sharoda. #ITP #Agda #IsabelleHOL #LeanProver
- A framework for formal dynamic dependability analysis using HOL theorem proving. ~ Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar. #ITP #HOL4
- Maintaining a library of formal mathematics. ~ Floris van Doorn, Gabriel Ebner, Robert Y. Lewis. #ITP #LeanProver #Math
- Formalizing Henkin-Style completeness of an axiomatic system for propositional logic. ~ Asta Halkjær From. #ITP #IsabelleHOL #Logic
- Two types of universe for two types of mathematician. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
- The Tactician (A seamless, interactive tactic learner and prover for Coq). ~ Lasse Blaauwbroek, Josef Urban, Herman Geuvers. #ITP #Coq #MachineLearning
- Computational logic for biomedicine and neurosciences. ~ A. Bahrami, E. de Maria, J. Despeyroux, A. Felty, P. Lió. #ITP #Coq
- Tree neural networks in HOL4. ~ Thibault Gauthier. #ITP #HOL4 #NeuralNetwork
- The stillness of Haskell code. ~ Claes-Magnus Berg. #Haskell #FunctionalProgramming
- A formally verified compiler for programs that deal with cached address translation. ~ J. Andersson. #MsC_Thesis #ITP #IsabelleHOL
- An MIU decision procedure in Lean. ~ Gihan Marasingha. #ITP #LeanProver
- A biased history of equality in type theory]. (Some equations are more equal than others). ~ James Chapman. #TypeTheory #ITP #Coq
- Who verifies the verifiers? A computer-checked implementation of the DPLL algorithm in Dafny. ~ Cezar-Constantin Andrici, Ştefan Ciobâcă. #Dafny #Logic
- Towards verified Artificial Intelligence. ~ Sanjit A. Seshia, Dorsa Sadigh, S. Shankar Sastry. #AI #FormalVerification
- Playing with the tower of Hanoi formally. ~ Laurent Théry. #ITP #Coq
- Towards secure IoT programming in Haskell. ~ N. Valliappan, R. Krook, A. Russo, K. Claessen. #Haskell #FunctionalProgramming
- Setting up Haskell development environment: The basics. #Haskell #FunctionalProgramming
- Strong functional pearl: Harper’s regular-expression matcher in Cedille. ~ Aaron Stump et als. #Haskell #Cedille #FunctionalProgramming
- Approaches to the implementation of generalized complex numbers in the Julia language. ~ M.N. Gevorkyan, A.V. Korolkova, D.S. Kulyabov. #JuliaLang #Math
- Formalizing Nakamoto-style proof of Stake. ~ Søren Eller Thomsen, Bas Spitters. #ITP #Coq
- Relational characterisations of paths. ~ Walter Guttmann, Peter Höfner. #ITP #IsabelleHOL
- Formally verifying proofs for algebraic identities of matrices. ~ Leonard Schmitz, Viktor Levandovskyy. #ITP
- Formally verified constraint solvers. ~ Catherine Dubois, Sourour Elloumi, Arnaud Gotlieb. #ITP #Coq #CSP
- Machine learning in Haskell. ~ @tonyday567 #Haskell #FunctionalProgramming #MachineLearning
- The golden rule of software quality. ~ G. Gonzalez (@GabrielG439). #Programming #Haskell
- Día Mundial de la Lógica 2021. #Lógica
- Expressing disambiguation filters as combinators. ~ José Nuno Macedo, João Saraiva. #Haskell #FunctionalProgramming
- Análisis de coste en programas funcionales Usando CiaoPP. ~ David Munuera Mazarro. #TFG #Haskell #Prolog #Algorítmica
- Golfing language extensions. ~ Taylor Fausak (@taylorfausak). #Haskell #FunctionalProgramming
- Metamath Zero: Designing a theorem prover prover. ~ #ITP
- Maintaining a library of formal Mathematics. ~ Gabriel Ebner. #ITP #LeanProver #Math
- Automated verification of reactive and concurrent programs by calculation. ~ Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock. #ITP #Isabelle
- Certifying a rule-based model transformation engine for proof preservation. ~ Z. Cheng, M. Tisi, J. Hotonnier. #ITP #Coq