Resumen de lecturas compartidas del 25 al 31 de enero de 2020
Esta entrada es una recopilación de lecturas compartidas, del 25 al 31 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 DAO: Demostración asistida por ordenador
1.1 DAO con Agda
- Combining predicate transformer semantics for effects: a case study in parsing regular languages. ~ Tim Baanen, Wouter Swierstra. #Agda #FunctionalProgramming
- The Cantor-Schröder-Bernstein theorem for ∞-groupoids. ~ Martin Escardo. #ITP #Agda #Math
- Elaborating dependent (co)pattern matching: No pattern left behind. ~ Jesper Cockx, Andreas Abel. #ITP #Agda
1.2 DAO con Coq
- First steps with Coq. ~ Assia Mahboubi. #ITP #Coq
- Introduction to Coq. ~ Assia Mahboubi. #ITP
- Programming with dependent types in Coq: inductive families and dependent patter-matching. ~ Matthieu Sozeau. #ITP #Coq
- Homotopy Type Theory. ~ Nicolas Tabareau. #ITP #Coq #HoTT
- A certificate-based approach to formally verified approximations. ~ Florent Bréhard, Assia Mahboubi, Damien Pous. #ITP #Coq #Math
- TEpla: A certified type enforcement access-control policy language. ~ Amir Eaman. #PhD_Thesis #ITP #Coq
- Formally verified code obfuscation in the Coq Proof Assistant. ~ Weiyun Lu. #PhD_Thesis #ITP #Coq
- Show that a monic (injective) and epic (surjective) function has an inverse in Coq. ~ Arthur Azevedo De Amorim. #ITP #Coq #Math
- A formalised polynomial-time reduction from 3SAT to Clique. ~ Lennard Gäher. #ITP #Coq
1.3 DAO con HOL Light
- FASiM: A framework for automatic formal analysis of simulink models of linear analog circuits. ~ Adnan Rashid, Ayesha Gauhar and Osman Hasan. #ITP #HOL_Light
1.4 DAO con Idris
- Formalizing the Curry-Howard correspondence. ~ Juan Ferrer Meleiro, Hugo Luiz Mariano. #ITP #Idris #Logic
1.5 DAO con Isabelle/HOL
- Smart induction for Isabelle/HOL (System description). ~ Yutaka Nagashima. #ITP #IsabelleHOL
- Searching the space of representations: reasoning through transformations for mathematical problem solving. ~ Daniel Raggi. #PhD_Thesis #ITP #IsabelleHOL
- Formalization of forcing in Isabelle/ZF. ~ Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf. #ITP #IsabelleZF #Logic
1.6 DAO con Lean
- Coherence via wellfoundedness. ~ Nicolai Kraus, Jakob von Raumer. #ITP #LeanProver #Math
1.7 DAO en general
- HolPy: Interactive theorem proving in Python. ~ Bohua Zhan. #ITP #HolPy #Logic #Python
- Mechanized proofs for PL: Past, present, and future. ~ Talia Ringer. #ITP
- Introduction and formalization of Boolean algebra. ~ Boro Sitnikovski (@BSitnikovski). #ITP #Metamath #Math
2 Programación declarativa
2.1 Programación funcional con Haskell
- vmap in Haskell. ~ Edward Z. Yang (@ezyang). #Haskell #FunctionalProgramming
- Case study: migrating from lens to optics. ~ Oleg Grenrus (@phadej). #FunctionalProgramming
- Profunctor optics, a categorical update. ~ Bryce Clarke et als. #Haskell #FunctionalProgramming
- A Pythonista’s Review of Haskell. ~ Ying Wang. #Haskell #Python
- Property testing in depth: The size parameter. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming
- Terminating tricky traversals. ~ Donnacha Oisín Kidney (@oisdk). #Haskell #Agda #FunctionalProgramming
- Profunctor optics: The categorical view. ~ Emily Pillmore and Mario Román. #Haskell #FunctionalProgramming #CategoryTheory
- Developing GHC for a Living: Interview with Vladislav Zavialov. ~ Denis Oleynikov. #Haskell #FunctionalProgramming
- Haskell in production: CentralApp. ~ Ashesh Ambasta (@AsheshAmbasta), Gints Dreimanis. #Haskell #FunctionalProgramming
- Transformations on applicative concurrent computations. ~ Román González. #Haskell #FunctionalProgramming
- Multiple address spaces in a distributed capability system. ~ Nora Hossle. #MsC_Thesis #Haskell #FunctionalProgramming
- Locating performance bottlenecks in large Haskell codebases. ~ Juan Raphael Diaz Simões. #Haskell #FunctionalProgramming
3 Lógica
- Set Theory vs. Type Theory. Alexandre Miquel. #Logic #CompSci
- Realizabilidad clásica y efectos colaterales: Extendiendo la correspondencia de Curry-Howard. ~ Étienne Miquey. #Logic #CompSci
- Curry-Howard: unveiling the computational content of proofs. ~ Étienne Miquey. #CompSci
- The benefits of sequent calculus. ~ Étienne Miquey. #Logic #CompSci