Resumen de lecturas compartidas del 12 al 18 de enero de 2020
Esta entrada es una recopilación de lecturas compartidas, del 12 al 18 de enero, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
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.
1 Programación declarativa
1.1 Programación funcional con Haskell
- Common stanzas. ~ Veronika Romashkina (@vronnie911). #Haskell #Cabal
- Is Haskell a category? ~ B. Fong, B. Milewski, D. Spivak. #FunctionalProgramming #CategoryTheory
- Programming with categories (Draft). ~ B. Fong, B. Milewski, D.I. Spivak. #FunctionalProgramming #Haskell #CategoryTheory
- Static types are dangerously interesting. ~ Alex Nixon (@alexnixon_uk). #Haskell #FunctionalProgramming
- Adjunctions in the wild: foldl. ~ Justin Le (@mstk). #Haskell #FunctionalProgramming
- Digging into Lenses. ~ Josh Kuhn (@deontologician). #Haskell #FunctionalProgramming
- A framework for exploring finite models. ~ Salman Saghafi. #PhD_Thesis #Logic #Haskell
- Using Cabal on its own. ~ James Bowen (@james_OWA). #Haskell #Cabal
- The road to proficient Haskell. ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming
- A tale of two functors (or: how I learned to stop worrying and love Data and Control). ~ Arnaud Spiwack. #Haskell #FunctionalProgramming
1.2 Programación funcional con Lisp
- Programming algorithms: approximation. ~ Vsevolod Dyomkin. #CommonLisp #Algorithms
1.3 Programación lógica con Prolog
2 DAO: Demostración asistida por ordenador
2.1 DAO con Isabelle/HOL
- Automating asymptotics in a theorem prover. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
- On a mathematician’s attempts to formalize his own research in proof assistants. ~ Sébastien Gouëzel. #ITP #IsabelleHOL #LeanProver #Math
- ODEs and the Poincaré-Bendixson theorem in Isabelle/HOL. ~ Fabian Immler, Yong Kiam Tan. #ITP #IsabelleHOL #Math
- Reasoning with non-linear formulas in Isabelle/HOL. ~ Wenda Li. #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
- Computer-supported exploration of a categorical axiomatization of modeloids. ~ L. Tiemens, D.S. Scott, C. Benzmüller, M. Benda. #ITP #IsabelleHOL #Math
- Verified approximation algorithms in Isabelle/HOL. ~ R. Eßmann, T. Nipkow, S. Robillard. #ITP #IsabelleHOL
- Closest pair of points algorithms. ~ M. Rau, T. Nipkow. #ITP #IsabelleHOL
- 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
2.2 DAO con 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
- A mechanized formalization of the WebAssembly specification in Coq. ~ X. Huang. #ITP #Coq
2.3 DAO con Lean
- Formalizing a sophisticated definition. ~ Patrick Massot, Kevin Buzzard, Johan Commelin. #ITP #LeanProver #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
2.4 DAO con PVS
- Automatic generation and verification of test-stable floating-point code. ~ L. Titolo, M. Moscato, C.A. Muñoz. #ITP
- A verified packrat parser interpreter for parsing expression grammars. ~ C. Blaudeau, N. Shankar. #ITP #PVS
2.5 DAO en general
- The space of mathematical software systems. ~ J. Carette, W.M. Farmer, Y. Sharoda. #ATP #ITP #Math #CompSci
3 Lógica
- Randomly generated and self-correcting logic exercises site. ~ Justin Weinberg. #Logic #WorldLogicDay
- History of interactive theorem proving. ~ J. Harrison, J. Urban, F. Wiedijk. #ITP #Logic #CompSci #WorldLogicDay
- The story of Logic. ~ Robert L. Constable. #Logic #CompSci #WorldLogicDay
- Computer Science as the continuation of Logic by other means. ~ Georg Gottlob. #Logic #CompSci #WorldLogicDay
- Computer Science and Logic (a match made in heaven). ~ Luca Aceto. #Logic #CompSci #WorldLogicDay
- Mathematical Logic in Computer Science. ~ Assaf Kfoury. #Logic #CompSci #WorldLogicDay
- Rusty Razor is a tool for constructing finite models for first-order theories. ~ Salman Saghafi. #Logic
- Automated reasoning: From bold dreams to Computer Science methodology. ~ Robert L. Constable. #ATP #CompSci #WorldLogicDay
- TAUT: el software desarrollado por un filósofo del CONICET para enseñar Lógica. #Lógica #WorldLogicDay
- Can the computer really help us to prove theorems? ~ Herman Geuvers. #ITP #Logic #CompSci #WorldLogicDay
- On the unusual effectiveness of Logic in Computer Science. ~ J.Y. Halpern et als. #Logic #CompSci #WorldLogicDay
- Teach yourself Logic 2020: A study guide. ~ Peter Smith. #Logic
- TAUT: A website that contains randomly-generated, self-correcting logic excercises. ~ Ariel Roffé. #Logic