Resumen de lecturas compartidas del 1 al 8 de febrero de 2020
Esta entrada es una recopilación de lecturas compartidas, del 1 al 8 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
- Introduction to univalent foundations of mathematics with Agda. ~ Martín Hötzel Escardó. #ITP #Agda #Math
- Toward a mechanized compendium of gradual typing. ~ Jeremy G. Siek. #ITP #Agda
1.2 DAO con Coq
- Computational type theory and interactive theorem proving with Coq (Version of August 2, 2019). ~ Gert Smolka. #eBook #ITP #Coq #Logic
- jsCoq: A port of Coq to Javascript (Run Coq in your browser). ~ Emilio Jesús Gallego Arias. #ITP #Coq
- A formal system of axiomatic set theory in Coq. ~ Tianyu Sun, Wensheng Yu. #ITP #Coq #Math
- A formal verification framework for security issues of blockchain smart contracts. ~ Tianyu Sun, Wensheng Yu. #ITP #Coq #Blockchain
- Implementing and certifying a Web server in Coq. ~ Thomas Letan. #ITP #Coq
- Formalizing functional analysis structures in dependent type theory. ~ Reynald Affeldt et als. #ITP #Coq #Math
- Hilbert’s tenth problem in Coq. ~ Dominique Larchey-Wendling, Yannick Forster. #ITP #Coq #Math
- Completeness theorems for first-order logic analysed in constructive type theory. ~ Yannick Forster, Dominik Kirst, Dominik Wehr. #ITP #Coq #Logic
- Verified programming of Turing machines in Coq. ~ Yannick Forster, Fabian Kunze, Maximilian Wuttke. #ITP #Coq
- The weak call-by-value λ-calculus is reasonable for both time and space. ~ Yannick Forster, Fabian Kunze, Marc Roth. #ITP #Coq
- A certifying extraction with time bounds from Coq to call-by-value λ-calculus. ~ Yannick Forster, Fabian Kunze. #ITP #Coq
- Trakhtenbrot’s theorem in Coq (A constructive approach to finite model theory). ~ Dominik Kirst, Dominique Larchey-Wendling. #ITP #Coq #Logic
1.3 DAO con Isabelle/HOL
- A comprehensive framework for saturation theorem proving (Technical report). ~ Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette. #ITP #IsabelleHOL #Logic
- A formal development cycle for security engineering in Isabelle. ~ Florian Kammüller. #ITP #IsabelleHOL
- VERONICA: Expressive and precise concurrent information flow security (Extended version with technical appendices). ~ Daniel Schoepe, Toby Murray, Andrei Sabelfeld. #ITP #IsabelleHOL
- Formal specification, monitoring, and verification of autonomous vehicles in Isabelle/HOL. ~ Albert Rizaldi. #PhD_Thesis #ITP #IsabelleHOL
- A hierarchy of algebras for boolean subsets. ~ Walter Guttmann, Bernhard Möller. #ITP #IsabelleHOL #Math
- Computer-supported analysis of arguments in climate engineering. ~ David Fuenmayor, Christoph Benzmüller. #ITP #IsabelleHOL.
- Towards a readable formalisation of category theory. ~ Greg O’Keefe. #ITP #IsabelleHOL #CategoryTheory
1.4 DAO con Lean
- Beyond notations: Hygienic macro expansion for theorem proving languages. ~ Sebastian Ullrich, Leonardo de Moura. #ITP #LeanProver
1.5 DAO y DAT en general
- Automated proof of Bell-LaPadula security properties. ~ Maximiliano Cristiá, Gianfranco Rossi. #ATP #SetLog
- MOIN: A nested sequent theorem prover for intuitionistic modal logics (system description). ~ Marianna Girlando, Lutz Straßburger. #ATP #Prolog #Logic
- ZZ (drunk octopus) is a modern formally provable dialect of C, inspired by Rust. ~ Arvid E. Picciani. #ZZ #Programming #SMT #FormalVerification
2 Programación declarativa
2.1 Programación funcional con Haskell
- Ulam spirals. ~ Ken T Takusagawa. #Haskell #FunctionalProgramming
- Competitive Programming in Haskell: primes and factoring. ~ Brent Yorgey. #Haskell #FunctionalProgramming
- Intro to Kaleidoscopes: Optics for aggregating data through Applicatives. ~ Chris Penner. #Haskell #FunctionalProgramming
- Finkel: Haskell in S-expression. #Haskell #Lisp #Finkel_lang
- Functional programming: The simple version. ~ Muhammad Tabaza. #Haskell #FunctionalProgramming
- Why monad composes operations sequentially. ~ Riccardo Odone. #Haskell #FunctionalProgramming
- Lorentz: Implementing smart contract eDSL in Haskell. ~ Kostya Ivanov. #Haskell #FunctionalProgramming
- Java & Haskell: Similarities and differences. ~ Dervis Mansuroglu. #Java #Haskell
- Thinking in types. ~ Pat Brisbin. #Haskell #FunctionalProgramming
- Safe memory management in inline-java using linear types. ~ Facundo Dominguez. #Haskell #FunctionalProgramming
- Functional or combinator parsing. ~ Graham Hutton. #Haskell #FunctionalProgramming
2.2 Programación lógica con Prolog
- MOIN: A nested sequent theorem prover for intuitionistic modal logics (system description). ~ Marianna Girlando, Lutz Straßburger. #ATP #Prolog #Logic
3 Lógica
- Proofs, computability, complexity, and the lambda calculus (An introduction). ~ Jean Gallier, Jocelyn Quaintance. #eBook #Logic #CompSci #LambdaCalculus