Resumen de lecturas compartidas durante marzo de 2020
Esta entrada es una recopilación de lecturas compartidas, durante marzo 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.
- Programming with Miranda. ~ C. Clack, C. Myers, and E. Poon (1995). #eBook #Miranda #FunctionalProgramming
- Church’s thesis and functional programming. ~ David Turner (2006). #Logic #FunctionalProgramming #Miranda
- Some history of functional programming languages. ~ David Turner (2012). #FunctionalProgramming
- Postcondition-preserving fusion of postorder tree transformations. ~ Eleanor Davies, Sara Kalvala. #ITP #Coq
- A modern look at GRIN, an optimizing functional language back end. ~ Csaba Hruska, Péter Dávid Podlovics, Andor Pénzes. #Haskell #FunctionalProgramming
- Course: Approximation theory and proof assistants: certified computations. ~ Nicolas Brisebarre, Damien Pous./#coqsessions #ITP #Coq #Math
- First steps with Coq (for primary and secondary school teachers, APMEP, Grenoble, 2011). ~ Damien Pous. #ITP #Coq
- Optimizing a maze with graph theory, genetic algorithms, and Haskell. ~ Chris Smith (@cdsmithus). #Haskell #FunctionalProgramming #Math
- Seventy-five problems for testing automatic theorem provers. ~ Francis Jeffry Pelletier (1986). #Logic
- How to get a Haskell job. ~ Neil Mitchell (@ndm_haskell). #Haskell #FunctionalProgramming
- Lisp code for the textbook “Paradigms of Artificial Intelligence Programming”. ~ Peter Norvig. #CommonLisp #AI
- Competitive programming in Haskell: modular arithmetic, part 2. ~ Brent Yorgey. #Haskell #FunctionalProgramming #Math
- Practical machine-checked formalization of change impact analysis. ~ Karl Palmskog, Ahmet Celik, Milos Gligoric. #ITP #Coq
- Declarative pearl: Deriving monadic quicksort. ~ Shin-Cheng Mu, Tsung-Ju Chiang. #Haskell #FunctionalProgramming
- Automated derivation of random generators for algebraic data types. ~ Agustín Mista. #Haskell #FunctionalProgramming
- Should your specification language be typed?. ~ Leslie Lamport, Lawrence C. Paulson (1999). #ITP #FunctionalProgramming
- The Prolog debugger and declarative programming. Examples. ~ Włodzimierz Drabent. #Prolog #LogicProgramming
- Scissors congruence (An interactive demonstration of the Wallace–Bolyai–Gerwien theorem). ~ Dima Smirnov, Zivvy Epstein. #Math
- Create blockchain in Haskell (Rolling your own blockchain in Haskell). ~ Michael Burge (2017). #Haskell #Blockchain
- Intuitionistic mathematics and logic. ~ Joan R. Moschovakis, Garyfallia Vafeiadou. #Logic #Math
- Code is engineering, types are science. ~ Juan Raphael Diaz Simões. #Programming #Logic
- Speak math, not code. (Writing algorithms in mathematics rather than code is not only more elegant but also more efficient, says 2013 Turing Award winner Leslie Lamport). #Math #Programming #CompSci
- Building a friendly and safe EDSL with IxState and TypeLits. #Haskell #FunctionalProgramming
- distributed-dataset: A distributed data processing framework in Haskell. ~ Utku Demir. #Haskell #FunctionalProgramming
- GHC Haskell Pats and LPats. ~ Shayne Fletcher. #Haskell #FunctionalProgramming
- Audience role in mathematical proof development. ~ Zoe Ashton. #Logic #Math #ITP
- Writing more modular code with lazy evaluation. ~ Heinrich Apfelmus. #Haskell #FunctionalProgramming
- How does lazy evaluation work in Haskell? ~ Heinrich Apfelmus. #Haskell #FunctionalProgramming via @etorreborre
- Declarative stream runtime verification (hLola). ~ Martı́n Ceresa, Felipe Gorostiaga, César Sánchez. #Haskell #FunctionalProgramming
- Idris 2: Quantitative Type Theory in action. ~ Edwin Brady. #Idris #FunctionalProgramming
- Naive synthesis of sorting networks using Z3Py. ~ Philip Zucker (@SandMouth). #SMT #Z3
- P =? NP. ~ Scott Aaronson (2002). #Logic #CompSci
- El Coronavirus y la leyenda del tablero de ajedrez. ~ Carlos Pena y Juan José Gómez Cadenas. #Matemáticas
- Les algorithmes du programme 2019 de mathématiques de Seconde. ~ Benjamin Clerc. #Math #Programming #Python
- Implémentations du problème du Duc de Toscane dans différents langages. ~ Guillaume Connan. #Math #Caml #Haskell #Scala #Python #Scilab
- Algorithmes de graphes. ~ Guillaume Connan (2019). #Math #SageMath #Pythom
- Au delà des réels: méthodes numériques en informatique. ~ Guillaume Connan (2016). #Math #Python
- Easily making CheatSheets with Org-mode. ~ Musa Al-hassy. #Emacs #OrgMode
- PythonCheatSheet: Quick reference to a tremendously accessible high-level language – executable pseudocode! ~ Musa Al-hassy. #Python #OrgMode
- Formal verification of cyber-physical systems using theorem proving. ~ Adnan Rashid, Umair Siddique, Sofine Tahar. #ITP #HOL4 #HOL_Light #IsabelleHOL #Coq #PVS
- Julia Snail: An Emacs development environment for Julia. #Emacs #JuliaLang
- Holmes: a library for computing constraint-solving problems. ~ Tom Harding. #Haskell #FunctionalProgramming
- Landmark Computer Science proof cascades through Physics and Math. ~ Kevin Hartnett (@KSHartnett). #CompSci #Physics #Math
- Hilbert’s tenth problem in Coq. ~ Dominique Larchey-Wendling, Yannick Forster. #ITP #Coq #Math
- Haskell with UTF-8. ~ Kirill Elagin. #Haskell #FunctionalProgramming
- Proofs, computability, undecidability, complexity, and the lambda calculus (An introduction). ~ Jean Gallier, Jocelyn Quaintance. #eBook #Logic #CompsCi
- Mechanization of a type system for atomicity analysis and its type safety. ~ Beatriz Ferreira et als. #ITP #Coq
- Computational complexity and Brouwer’s continuum. ~ Robert L. Constable. #Logic #Math #ITP #Nuprl
- On proof complexity of resolution over polynomial calculus. ~ Erfan Khaniki. #Logic #Math #CompSci
- El problema aritmético de Sylvester. ~ Juan Arias de Reyna. #Matemáticas
- Ventajas del texto plano. #Emacs #OrgMode
- More natural deduction exercises. ~ Peter Smith. #Logic
- The hardest Math problem. ~ John Baez (@johncarlosbaez). #Math
- LISP comes of age. ~ Steven K. Roberts (1980). #Lisp #Programming #AI
- Todas las revistas Cacumen. #Matemáticas
- Matemáticas recreativas: ponga a prueba su destreza resolviendo enigmas históricos. ~ Fernando Blasco (@fblascoxyz). #Matemáticas
- FindFacts: a search application to find formal theory content of Isabelle and the AFP. ~ Fabian Huch./#about #ITP #IsabelleHOL #AFP
- The ideal mathematician. ~ Phillip J. David & Reuben Hersh (1981). #Math
- QED at large: A survey of engineering of formally verified software. ~ Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock. #ITP #FormalVerification
- The <- pure pattern. ~ Neil Mitchell (@ndm_haskell). #Haskell #FunctionalProgramming
- Verifying typeclasses with refinement types. ~ Yiyun Liu, James Parker, Michael Hicks, Niki Vazou. #Haskell #LiquidHaskell
- Can computers ever replace the classroom? ~ Alex Beard. #IA #Teaching
- seL4 in Australia: From research to real-world trustworthy systems. ~ Gernot Heiser, Gerwin Klein, June Andronick. #ITP #IsabelleHOL
- El Mundo de las Matemáticas de Mathigon. ~ @Alvy. #Matemáticas
- World of Mathematics. #Math
- Need a logic course, fast? ~ Richard Zach (@RrrichardZach). #Logic
- Nix for Coq development. ~ Yann Herklotz (@ymherklotz). #ITP #Coq #Nix
- Gröbner bases and their applications. ~ Mateusz Paprocki. #Math #Python
- Tactic learning and proving for the Coq proof assistant. ~ Lasse Blaauwbroek, Josef Urban, Herman Geuvers. #ITP #Coq #MachineLearning
- Towards formally verified smart contracts with Haskell. ~ Allison Irvin, Nick Waywood. #Haskell #FunctionalProgramming
- “Hello World!” in Isabell/HOL (including a formal framework for reasoning about IO). ~ Cornelius Diekmann and Lars Hupel. #ITP #IsabelleHOL #Monads
- Blaze: Lightweight HTML generation. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming
- Data structure challenge: finding the rightmost empty slot. ~ Brent Yorgey. #Haskell #FunctionalProgramming
- Infinite patterns. ~ Cristóbal Vila. #Maths
- A formalization of SQL with nulls. ~ Wilmer Ricciotti, James Cheney. #ITP #Coq
- Taichi: A brand new programming language, “Frozen” in 99 lines of code. #Programming
- The problem with adding functions to compact regions. ~ Ömer Sinan Ağacan. #Haskell #FunctionalProgramming
- An under-approximate relational logic in Isabelle/HOL. ~ Toby Murray. #ITP #IsabelleHOL
- Furstenberg’s topology and his proof of the infinitude of primes in Isabelle/HOL. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
- Applying the Isabelle Insider framework to airplane security. ~ Florian Kammüller, Manfred Kerber. #ITP #IsabelleHOL
- Building a web app with functional programming – Haskell – part I. ~ Iori Matsuhara (@Matsumonkie). #Haskell #FunctionalProgramming
- Zipping Trees, Part 1. ~ Joseph Morag. #Haskell #FunctionalProgramming
- A trustful monad for axiomatic reasoning with probability and nondeterminism. ~ Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa. #ITP #Coq
- Logic-based technologies for intelligent systems: State of the art and perspectives. ~ Roberta Calegari, Giovanni Ciatto, Enrico Denti, Andrea Omicini. #Logic #AI
- Dual and axiomatic systems for constructive S4, a formally verified equivalence. ~ Lourdes del Carmen González HuescaFavio, E. Miranda-Perea, P. Selene Linares-Arévalo. #ITP #Coq
- A starter template for SWI-Prolog projects. ~ Alex Kelley. #Prolog #LogicProgramming
- Some coding guidelines for Prolog. ~ Michael A. Covington (2002). #Prolog #LogicProgramming
- A repository for writing a Thesis with Org Mode. #Emacs #OrgMode
- Programming algorithms: Synchronization. ~ Vsevolod Dyomkin. #CommonLisp
- Lucid: Another HTML option. ~ James Bowen (@james_OWA). #Haskell #FuncionalProgramming
- Thinking mathematically notes. ~ A. Máté. #Logic #Math