Resumen de lecturas compartidas del 9 al 15 de febrero de 2020
Esta entrada es una recopilación de lecturas compartidas, del 9 al 15 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
- Equality of functions in Agda. ~ Mark Armstrong. #ITP #Agda #FunctionalProgramming via @armk_eh
1.2 DAO con Coq
- A proof assistant based formalisation of core Erlang. ~ Péter Bereczky, Dániel Horpácsi and Simon Thompson. #ITP #Coq #Erlang
- Awesome Coq Awesome (A curated list of awesome Coq libraries, plugins, tools, and resources). #ITP #Coq
- How small can we make a useful type theory? ~ Pedro Abreu (@etapedro). #ITP #Coq #Cedille #FunctionalProgramming
- Coquedille: A Coq to Cedille transpiler written in Coq. ~ Pedro Abreu (@etapedro). #ITP #Coq #Cedille #FunctionalProgramming
- Mac Lane’s comparison theorem for the Kleisli construction formalized in Coq. ~ Burak Ekici, and Cezary Kaliszyk. #ITP #Coq
1.3 DAO con HOL Light
- Formalization of cost and utility in Microeconomics. ~ Asad Ahmed, Osman Hasan, Falah Awwad, and Nabil Bastaki. #ITP HOL_Light
1.4 DAO con Isabelle/HOL
- Cours: Sémantique des langages. ~ Frédéric Boulanger. #ITP #IsabelleHOL
- Tutoriel: types de données, fonctions et preuves en Isabelle. ~ Frédéric Boulanger. #ITP #IsabelleHOL
- Type classes and filters for mathematical analysis in Isabelle/HOL. ~ Johannes Hölzl, Fabian Immler, Brian Huffman. #ITP #IsabelleHOL #Math
- Arithmetic progressions and relative primes. ~ José Manuel Rodríguez Caballero. #ITP #IsabelleHOL #Math
1.5 DAO con Lean
- Lean is better for proper maths than all the other theorem provers. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
- Where is the fashionable mathematics? ~ Kevin Buzzard (@XenaProject). #Math #ITP #LeanProver #Coq #IsabelleHOL
1.6 DAO en general
- Automated reasoning I. ~ Uwe Waldmann. #eBook #ATP #Logic
- Automated reasoning II. ~ Sophie Tourret, Uwe Waldmann. #eBook #ATP #Logic
- An experimental study of formula embeddings for automated theorem proving in first-order logic. ~ Ibrahim Abdelaziz et als. #ATP #MachineLearning
2 Programación declarativa
2.1 Programación funcional con Haskell
- MateFun: Functional Programming and Math with adolescents. ~ Alejandra Carboni et als. #Haskell #FunctionalProgramming #Math
- Compiling Haskell to JavaScript, not in the way you’d expect. ~ Oleg Grenrus (@phadej). #Haskell #FunctionalProgramming #JavaScript
- State will do. ~ Willem Seynaeve, Koen Pauwels and Tom Schrijvers. #Haskell #FunctionalProgramming
- A DSL for fluorescence microscopy. Birthe van den Berg, Peter Dedecker, Tom Schrijvers. #Haskell #FunctionalProgramming
- An equational modeling of asynchronous concurrent programming. ~ David Janin. #Haskell #FunctionalProgramming
- PaSe: An extensible and inspectable DSL for micro-animations. ~ Ruben P. Pieters and Tom Schrijvers. #Haskell #FunctionalProgramming
- Generating next step hints for task oriented programs using symbolic execution. ~ Nico Naus and Tim Steenvoorden. #Haskell #FunctionalProgramming
- BinderAnn: Automated reification of source annotations for monadic EDSLs. ~ Agustín Mista and Alejandro Russo. #Haskell #FunctionalProgramming
- Generalized Algebraic Data Types and Data Kinds. ~ Andre Popovitch (@PopovitchAndre). #Haskell #FunctionalProgramming
- Counterexamples of type classes. ~ Phil Freeman. #Haskell #Purescript #FunctionalProgramming
- An introduction to recursion schemes. ~ Patrick Thomson. #Haskell #FunctionalProgramming
- Typeable and Data in Haskell. ~ Chris Done (@christopherdone). #Haskell #FunctionalProgramming
- Template Haskell tutorial. ~ Mark Karpov (@mrkkrp). #Haskell #FunctionalProgramming
- Converting Cabal to Nix! ~ James Bowen (@james_OWA). #Haskell #Cabal #Nix
- Haskell in production: Riskbook (an interview with Jezen Thomas). ~ Gints Dreimanis. #Haskell #FunctionalProgramming
- Physics, History and Haskell. (Interview with Rinat Stryungis). ~ Denis Oleynikov. #Haskell #FunctionalProgramming
- How laziness works. #Haskell #FunctionalProgramming
- Imperative Haskell. ~ Vaibhav Sagar. #Haskell #FunctionalProgramming
- Verificación de estructura de redes neuronales profundas en tiempo de compilación (Proyecto TensorSafe). ~ Leonardo Piñeyro. #Haskell #DeepLearning
- Mejoras al intérprete MateFun. ~ Nicolás Vázquez. #Haskell #FunctionalProgramming #Math
- Maintainable software architecture in Haskell (with Polysemy). ~ Paweł Szulc (@EncodePanda). #Haskell #FunctionalProgramming
- Liquidate your assets (Reasoning about resource usage in Liquid Haskell). ~ Niki Vazou (@nikivazou). #Haskell
2.2 Programación funcional con Lisp
- Practical Common Lisp. ~ Peter Seibel. #eBook #CommonLisp
2.3 Programación funcional con OCaml
- Functional programming in OCaml. ~ Michael R. Clarkson. #eBook #OCaml #FunctionalProgramming
3 Lógica
- The Logic course adventure (An active learning textbook for formal logic). ~ Ian Schnee. #eBook #Logic