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