Resumen de lecturas compartidas (noviembre de 2017)
Esta entrada es una recopilación de lecturas compartidas, durante noviembre de 2017, en Twitter sobre programación funcional y demostración asistida por ordenador.
Las lecturas están ordenadas según su fecha de publicación en Twitter.
Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
- Formal methods and the KRACK vulnerability. ~ Joey Dodds #Cryptography #Formal_methods
- ASP with applications to mazes and levels. ~ Mark J. Nelson & Adam M. Smith @rndmcnlly #ASP #Game
- Notes on Answer Set Programming. ~ Chris Martens #ASP #Logic Programming
- The basics of Answer Set Programming. ~ Olaf Aviss #ASP
- A first look at Answer Set Programming. ~ Hakan Kjellerstrand (@hakankj) #ASP
- Constraint solving and planning with Picat. ~ N.F. Zhou, H. Kjellerstrand, J. Fruhman #eBook #Logic #Programming #Picat
- BioASP: Answer Set Programming for systems biology. #ASP
- Lecturas de teorías de categorías y programación funcional. #Matemáticas #Programación
- Exercitium: Números libres de cuadrados. #Haskell #I1M2017
- Improve SAT-solving with machine learning. ~ Haoze Wu #ATP #SAT #ML
- TypedFlow: a typed, higher-order frontend to TensorFlow and a high-level library for deep-learning. ~ Jean-Philippe Bernardy #Haskell #DeepLearning
- Academic research in the 21st century: maintaining scientific integrity in a climate of perverse incentives and hypercompetition. ~ M.A. Edwards, S. Roy
- RA2017: Ejercicios de programación funcional con Isabelle/HOL. #IsabelleHOL
- RA2017: Razonamiento automático sobre programas en Isabelle/HOL. #IsabelleHOL
- I1M2017: Funciones de orden superior en Haskell. #Haskell
- Understanding HLint rules. ~ Neil Mitchell #Haskell
- Computing with impossible types. ~ @haskell_cat #Haskell
- Sum of heights in a binary tree. ~ Brent Yorgey #Algorithmic
- Aivika: computation-based modeling and simulation in Haskell. ~ David E. Sorokin et als. #eBook #Haskell #Simulation
- Notes and thoughts from reading Milewski “Category theory for programmers” written in Haskell. ~ Robert Peszek #Haskell #Category_theory
- Foundations of implementations for formal argumentation. ~ F. Cerutti et als. #Logic #AI #ASP
- October 2017 1HaskellADay problems and solutions. ~ Douglas M. Auclair (@geophf) | Typed Logic #Haskell #1HaskellADay
- GLC: Lista de lecturas compartidas en octubre de 2017.
- Exercitium: Números completos. #Haskell #I1M2017
- Simplicity: a new language for blockchains. ~ Russell O’Connor #Coq #Blockchain
- Las matemáticas que puede esconder un dónut. ~ Alfonso J. Población #Matemáticas
- Who gets to be called a mathematician? ~ Junaid Mubeen (@fjmubeen) #Math
- A set solver for finite relation algebra. ~ M. Cristiá, G. Rossi #CLP
- Exercitium: Primos equidistantes. #Haskell #I1M2017
- Profunctor Optics. ~ Bartosz Milewski (@BartoszMilewski) #Haskell
- BiGUL: the bidirectional generic update language. #Haskell #Agda
- An axiomatic basis for bidirectional programming. ~ H.S. Ko, Z. Hu #Agda
- An axiomatic basis for bidirectional programming (Agda code). ~ H.S. Ko, Z. Hu #Agda
- A logical relation for monadic encapsulation of state (Proving contextual equivalences in the presence of runST). ~ A. Timany #Haskell
- AutoML, la máquina que crea otras máquinas inteligentes. ~ David Sarabia (@DSRELD) #IA #AA
- AutoML for large scale image classification and object detection. ~ B. Zoph, V. Vasudevan, J. Shlens, Q. Le #AI #ML
- Is mathematics a fine art? ~ Adrian Hindes #Math
- Teaching A.I. systems to behave themselves. ~ Cade Metz #AI #ML
- Mathematicians measure infinities and find they’re equal. ~ Kevin Hartnett (@KSHartnett) #Math via @QuantaMagazine
- Exercitium: Producto cartesiano de una familia de conjuntos. #Haskell #I1M2017
- Refinement reflection: complete verification with SMT. ~ Niki Vazou (@nikivazou) #Haskell #LiquidHaskell #Logic #SMT
- Persistent red black trees in Haskell. ~ Abhiroop Sarkar #Haskell
- Improving Haskell. ~ Martin A.T. Handley & Graham Hutton #Haskell
- Unie: Inequational reasoning assistant for proofs relating to improvement theory. ~ Martin A.T. Handley #Haskell
- I1M2017: Codificación binaria y transmisión de cadenas en Haskell. #Haskell
- I1M2017: Operaciones conjuntistas con listas. #Haskell
- Exercitium: Biparticiones de un número. #Haskell #I1M2017
- Generating good generators for inductive relations. ~ L. Lampropoulos, Z. Paraskevopoulou, B.C. Pierce #Coq #QuickCheck
- Encoding DCC (Dependency Core Calculus) in Haskell. ~ M. Algehed & A. Russo #Haskell
- Cómo calcular áreas contando puntitos. ~ M.A. Morales @gaussianos | El Aleph #Matemáticas
- An introduction to univalent foundations for mathematicians. ~ D.R. Grayson #Math #Logic #HoTT
- Proof theory. ~ J. Avigad #Math #Logic #ATP
- Small resolution proofs for QBF using dependency treewidth. ~ E. Eiben, R. Ganian & S. Ordyniak #Math #Logic #ATP
- Capturing the future by replaying the past (Functional Pearl). ~ J. Koppel & A. Solar #SML
- Exercitium: “Números_libres de cuadrados”. #Haskell #I1M2017 #I1M2017
- I1M2017: Definiciones de tipos en Haskell. #Haskell
- Finite state machines? (Your compiler wants in!) ~ Oskar Wickström (@owickstrom) #Haskell #Idris
- Would aliens understand lambda calculus? ~ Tomas Petricek (@tomaspetricek) #Math #Logic #CompSci
- Verifiable computing in Haskell. ~ Anthony Sheldon #Haskell #Math
- Spatial reasoning about motorway traffic safety with Isabelle/HOL. ~ Sven Linker #IsabelleHOL
- Hybrid multi-lane spatial logic in Isabelle/HOL. ~ Sven Linker #IsabelleHOL
- The digits of pi. ~ Jeremy Gibbons @jer_gib #Haskell #Math
- Haskell theory exploration scripts. ~ Chris Warburton #Haskell
- The Has type class pattern. ~ Jonathan Fischoff #Haskell via @topical_hq
- Formalization of a Conflict-free Replicated Datatype for Internet Message Access Protocol commands in Isabelle/HOL. ~ T. Jungnickel, L. Oldenburg & M. Loibl #IsabelleHOL
- Theory exploration on infinite structures. ~ S.H. Einarsdóttir #IsabelleHOL
- Replicable parallel branch and bound search. ~ B. Archibald, P. Maier, C. McCreesh, R. Stewart & P. Trinder #Haskell
- Purescript for Elm developers. ~ Marco Sampellegrini (@_alpacaaa) #PureScript #Elm
- Answer Set Programming from a logical point of view. ~ P. Cabalar, D. Pearce & A. Valverde #ASP
- Formalisms and formalizations: Glass Bead in conversation with Catarina Dutilh Novaes and Reviel Netz. #Logic #Math via @cdutilhnovaes
- To settle infinity question, a new law of Mathematics. ~ Natalie Wolchover (@nattyover) #Math via @QuantaMagazine
- Scientists in silico? ~ Carl McBride #CompSci
- argmat-clpb: Solve argumentation problems using Constraint Logic Programming over boolean variables. ~ F. Pu, G. Luo & Y. Chen #CLP
- Vigila tus primos. ~ Juan Arias de Reyna #Matemáticas #Computación #RSA
- Cinco claves para entender por qué el Gobierno ha desactivado tu DNI electrónico. ~ David Sarabia (@DSRELD) #RSA
- Millions of high-security crypto keys crippled by newly discovered flaw (Factorization weakness lets attackers impersonate key holders and decrypt their data). ~ Dan Goodin (@dangoodin001) #RSA
- The return of Coppersmith’s attack: Practical factorization of widely used RSA moduli. ~ M. Nemec, M. Sys, P. Svenda, D. Klinec, V. Matyas #Math #CompSci #RSA
- Validating Brouwer’s continuity principle for numbers using named exceptions. ~ V. Rahli & M. Bickford #ITP #Nuprl #Coq
- dblp2bibtex: Generates bibtex files for authors identified in the DBLP database. ~ Rob Stewart (@robstewartUK) #Haskell #TeX
- Exercitium: “Números completos” #Haskell #I1M2017
- Rust as a gateway drug to Haskell. ~ Karol Kuczmarski (@Xion__) #Rust #Haskell via @topical_hq
- MAC (A verified static information-flow control library). ~ M. Vassena & A. Russo #Haskell #Agda
- Exercitium: “Primos consecutivos equidistantes” #Haskell #I1M2017
- In depth overview of Elm and PureScript. Lessons learned porting a game from PureScript to Elm. ~ Marco Sampellegrini (@_alpacaaa) #PureScript #Elm
- Selecting a platform: JavaScript vs Elm vs PureScript vs GHCjs vs Scalajs. ~ Isaac Shapira #JavaScript #Elm #PureScript #GHCjs #Scalajs
- Exercitium: “Producto cartesiano de una familia de conjuntos”. #Haskell #I1M2017
- Is (some) mathematics poetry? ~ J. Henle #Math
- Neural-symbolic learning and reasoning: a survey and interpretation. ~ T.R. Besold et als. #AI
- Exercitium: “Biparticiones de un número”. #Haskell #I1M2017
- Haskell communities and activities report (November 2017). #Haskell
- Por qué deberías aprender programación funcional ya mismo (con una breve introducción a Haskell). ~ A. Marzal #PF #Haskell
- Answer Set Programming and CLASP (A tutorial). ~ S. Hölldobler, L. Schweizer #ASP
- Parallelising your array code. ~ Manuel Chakravarty (@TacticalGrace) #Haskell
- Exercitium: “Pares definidos por su MCD y su MCM”. #Haskell #I1M2017 #Haskell #I1M2017
- Portraits of famous philosophers who were also famous mathematicians. ~ C.S. Keyser #eBook #Math #History
- Recursion schemes (why, how and more). ~ Sergey Vinokurov (@5ergv) #Haskell
- Domain Specific Languages of Mathematics: lecture notes (November 8, 2017). ~ Patrik Jansson (@patrikja), Cezar Ionescu. #Haskell #Math
- Algorithmic resource verification. ~ R Kandhadai Madhavan #PhD_Thesis #ITP #Leon
- Proceedings of the Third Workshop on Bridging the gap between human and automated Reasoning (Is logic and automated reasoning a foundation for human reasoning?) #Logic #AR
- How type errors were fixed and what students did? ~ B. Wu, S. Chen #Haskell
- Learning user friendly type-error messages. ~ B. Wu, J.P. Campora III, S. Chen #Haskell
- I1M2017: Resolución de problemas y el método de Polya. #Haskell
- I1M2017: Programación con Haskell en la Red usando Repl.it. #Haskell
- I1M2017: Ejercicios sobre árboles binarios en Haskell (1). #Haskell
- I1M2017: Libro con las soluciones de las 8 primeras relaciones de ejercicios de programación con Haskell. #Haskell
- Unifying parsing and prettyprinting. ~ Sergey Vinokurov (@5ergv) #Haskell
- Adjunctions in everyday life (What we talk about when we talk about monads). ~ Rúnar Bjarnason (@runarorama) #Haskell
- Jargon from the functional programming world in simple terms! #FuncionalProgramming
- Scala code examples for functional programming jargon. ~ Ikhoon Eom #FuncionalProgramming #Scala
- Mechanizing Principia Logico-Metaphysica in functional type theory. ~ D. Kirchner, C. Benzmüller, E.N. Zalta #IsabelleHOL #RA2017
- Representation and partial automation of the Principia Logico-Metaphysica in Isabelle/HOL. ~ D. Kirchner #Msc_Thesis #IsabelleHOL #RA2017
- Finite-state machines, part 2: Explicit typed state transitions. ~ Oskar Wickström (@owickstrom) #Haskell
- Exercitium: “Números oblongos”. #Haskell #I1M2017
- Let’s play with Regular Expressions. ~ Sergey Vinokurov (@5ergv) #Haskell
- Python implementation and construction of finite abelian groups. ~ P. Bradley, J. Smethurst #Python #Math
- A programming digression: Kaprekar numbers. ~ E. Wallingford (@wallingf) #Programming #Math
- Net puzzle game in Elm. ~ Julian Priestley #Elm #Puzzle
- Verification of PCP-related computational reductions in Coq. ~ Y. Forster, E. Heiter, G. Smolka #Coq
- Rewriting a shallow DSL using a GHC Compiler extension. ~ M. Grebe, D. Young, A. Gill #Haskell
- Exercitium: “Mayor número equidigital”. #Haskell #I1M2017
- A programming digression: Farey sequences. ~ E. Wallingford (@wallingf) #Programming #Math
- Emacs for humans: glossary. #Emacs
- QuickCheck and magic of testing. ~ A. Kuleshevich #Haskell #QuickCheck
- Learn Emacs in one video. ~ Derek Banas (@NewThinkTank) #Emacs #I1M2017
- Type-directed code generation. ~ Sandy Maguire #Haskell
- Anatomy of a Haskell-based application, revisited. ~ Zhouyu Qian (@kccqzy) #Haskell
- LeanCheck: a simple enumerative property-based testing library. ~ Rudy Matela #Haskell
- Exercitium: “Números dígito potenciales”. #Haskell #I1M2017
- A programming digression: Generating excellent numbers. ~ E. Wallingford (@wallingf) #Programming #Math
- Joys & frustrations of putting 34,000 lines of Haskell into production (at Vacation Labs). ~ Saurabh Nanda (@saurabhnanda) #Haskell
- Schur number five. ~ Marijn J.H. Heule #SAT #Logic #AI
- Category theory for programmers. ~ Bartosz Milewski #eBook #CategoryTheory #Haskell #OpenLibra
- Exercitium: “Suma de divisores”. #Haskell #I1M2017 #I1M2017
- Verified functional algorithms. ~ Andrew W. Appel #FuncionalProgramming #ITP #Coq
- Eta Fibers (Towards better concurrency on the JVM). ~ Rahul Muttineni #Haskell
- Resolviendo problemas de satisfacción de restricciones con hormigas. ~ F. Sancho @sanchocaparrini #PSR #IA
- MonadBaseControl in five minutes. ~ Matt Parsons (@mattoflambda) #Haskell
- Dependent types in Haskell. ~ Sasa Bogicevic #Haskell
- RA2017: Razonamiento estructurado sobre programas con Isabelle/HOL. #IsabelleHOL
- A formally proved, complete algorithm for path resolution with symbolic links. ~ R. Chen, M. Clochard, C. Marché #ITP #Coq
- Functional pearl: Nested Datacubes. ~ Tim Philip Williams (@_willtim_) #Haskell
- Exercitium: “Cadenas de sumas de factoriales de los dígitos”. #Haskell #I1M2017
- Spheres and points. ~ Bassel Mabsout #Haskell
- tzimtsum: A Presburger arithmetic proposition decider Haskell library. #Haskell #Logic #Math
- Stochastic matrices and the Perron-Frobenius theorem in Isabelle/HOL. ~ R. Thiemann #IsabelleHOL #Math
- An EDSL for KDB/Q (rationale, techniques and lessons learned). ~ Tim Williams (@_willtim_) #Haskell
- Talk notes: Lazy evaluation in Haskell. ~ Kostiantyn Rybnikov (@ko_bx) #Haskell
- HyperHaskell: a graphical interpreter for the programming language Haskell. ~ Heinrich Apfelmus #Haskell
- Ejercicios sobre árboles binarios en Haskell (2). #I1M2017 #Haskell
- Ejercicios de tipos de datos algebraicos en Haskell (1). #I1M2017 #Haskell
- Programa en Haskell para reconocer tautologías. #I1M2017 #Haskell #Matemáticas #Lógica
- IPS-like proof systems based on binary decision diagrams. ~ A. Knop #Logic #AR #IPS
- Circuit complexity, proof complexity, and polynomial identity testing. ~ J.A. Grochow, T. Pitassi #AR #GröbnerBases
- Type theory in 15min. ~ Niki Vazou (@nikivazou) #Programming
- Una formalización del sistema de los números reales. ~ J.O. Acevedo y J.L. Echeverri #ITP #Agda
- Exference: Haskell tool to generate expressions from types. ~ Lennart Spitzner #Haskell
- Exference: Rubbing the Lamp once more. ~ Lennart Spitzner #Haskell
- Exercitium: “Número de divisores”. #Haskell #I1M2017 #Haskell #I1M2017
- Programación funcional avanzada (2017). ~ Ernesto Hernández-Novich (@iamemhn) #Curso #Haskell
- Can A.I. be taught to explain itself? ~ C. Kuang #XAI
- Teoría de categorías en Scala: Tipos y funciones. ~ A. Alcalde #TeoríaCategorías #Scala
- Carp: A statically typed Lisp, without a GC, for high performance applications. #Haskell #Lisp
- ¿Porqué usar programación funcional? ~ Marco Ordoñez #ProgramacionFuncional vía @nihilipster
- Proving Peano arithmetic partially consistent? ~ R.J. Lipton & K.W. Regan #Logic
- Stochastic matrices and the Perron–Frobenius theorem in Isabelle/HOL. ~ René Thiemann #ITP #IsabelleHOL #Math
- Session types in Cloud Haskell. ~ Ferdinand van Walree #PhD_Thesis #Haskell
- Exercitium: “Punto de inflexión”. #Haskell #I1M2017 todos los dígitos”]]. #Haskell #I1M2017
- Hamiltonian dynamics in Haskell. ~ Justin Le (@mstk) #Haskell #Math #Physic
- My unusual hobby. ~ Stephan Boyer (@stepchowfun) #ITP #Coq
- sparse-linear-algebra: Numerical computation in native Haskell. ~ Marco Zocca #Haskell #Math
- Total Haskell is reasonable Coq. ~ A. Spector-Zabusky, J. Breitner, C. Rizkallah, S. Weirich #Haskell #Coq
- Deciphering Haskell’s applicative and monadic parsers. ~ Eli Bendersky (@elibendersky) #Haskell
- Exercitium: “Sucesión contadora”. #Haskell #I1M2017 #Haskell #I1M2017
- Reseña: “Apología de un matemático” de G. H. Hardy. ~ F.R. Villatoro (@emulenews) #Matemáticas
- Lecturas sobre teoría de categorías y programación funcional. #TeoriaDeCategorias #ProgramacionFuncional #Haskell
- European Union regulations on algorithmic decision-making and a “right to explanation”. ~ B. Goodman, S. Flaxman #MachineLearning
- Haskell-University: Portfolio-based approach to learning Haskell. #Haskell
- Symmetric groups on finite sets in PureScript. #PureScript #Math
- Exercitium: “Mayor producto de las ramas de un árbol”. #Haskell #I1M2017