Resumen de lecturas compartidas del 16 al 21 de febrero de 2020
Esta entrada es una recopilación de lecturas compartidas, del 16 al 21 de febrero, 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 DAO: Demostración asistida por ordenador
1.1 DAO con Agda
- Signatures and induction principles for higher inductive-inductive types. ~ Ambrus Kaposi, and András Kovács. #ITP #Agda #Haskell #FunctionalProgramming
- Flexible coinduction in Agda. ~ Luca Ciccone. #MSc_Thesis #ITP #Agda
- Agda vs. Coq vs. Idris. #ITP #Agda #Coq #Idris
1.2 DAO con Coq
- mCoq: Mutation analysis for Coq verification projects. ~ Kush Jain et als. #ITP #Coq
- Equality in mechanized mathematics. ~ Ramkumar Ramachandra. #ITP #Coq #Math
- Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi. ~ Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. #ITP #Coq
- Certifications of programs with computational effects. ~ Burak Ekici. #PhD_Thesis #ITP #Coq
1.3 DAO con HOL Light
- Certification of nonclausal connection tableaux proofs. ~ Michael Färber, and Cezary Kaliszyk. #ITP #HOL_Light
1.4 DAO con Isabelle/HOL
- Isabelle/HOL and Proof General reference [Isabelle/HOL support wiki]. #ITP #IsabelleHOL
2 Programación declarativa
2.1 Programación funcional con Haskell
- Type witnesses in Haskell. ~ Sandeep Chandrika. #Haskell #FunctionalProgramming
- What I wish I knew when learning Haskell (Version 2.5). ~ Stephen Diehl (@smdiehl). #Haskell #FunctionalProgramming
- A tutorial on the universality and expressiveness of fold. ~ Graham Hutton (1999). #FunctionalProgramming #Haskell
- QuickCheck testing for fun and profit. ~ John Hughes (2007). #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
- Competitive programming in Haskell: modular arithmetic, part 1. ~ Brent Yorgey. #Haskell #FunctionalProgramming #Math
- Typing TABA (There and Back Again). ~ Donnacha Oisín Kidney (@oisdk). #Haskell #FunctionalProgramming
- From Curry to Haskell. ~ Felice Cardone. #Haskell #FunctionalProgramming #Logic
- How to make mondrian art in Haskell (Unleash your inner functional artist). ~ Marc Fichtel (@mc_razzy). #Haskell #FunctionalProgramming
- Monoids: Theme and variations (Functional Pearl). ~ Brent A. Yorgey (2012). #Haskell #FunctionalProgramming
- Infinite sets that admit fast exhaustive search. ~ Martı́n Escardó (2007). #Haskell #FunctionalProgramming
- QuickCheck: Α lightweight tool for random testing of Haskell programs. ~ Koen Claessen and John Hughes (2000). #Haskell #FunctionalProgramming
- Porting to Rio. ~ Colin Woodbury (@fosskers). #Haskell #FunctionalProgramming
- On linear types and exceptions. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming
2.2 Programación funcional con Lisp
- Programming algorithms: Compression. ~ Vsevolod Dyomkin. #Algorithms #CommonLisp
3 Lógica
- Teaching natural deduction as a subversive activity. ~ James Caldwell. #Logic