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