Resumen de lecturas compartidas (febrero de 2018)
Esta entrada es una recopilación de lecturas compartidas, durante febrero de 2018, en Twitter sobre programación funcional y demostración asistida por ordenador fundamentalmente.
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.
- Exercitium: “Sucesión de Lichtenberg”. #Haskell #I1M2017
- Homotopy type theory, univalent foundation, and binary trees. ~ R. Beauvile #ITP #Coq #HoTT
- DSLsofMath: typing mathematics. ~ Patrik Jansson (@patrikja), Cezar Ionescu #Haskell #Math
- The Elfe system: Verifying mathematical proofs of undergraduate students. ~ Maximilian Doré, Krysia Broda #Math #Elfe
- AI for marketing. ~ Chandrakumar #AI
- Exercitium: “Relación definida por un árbol”. #Haskell #I1M2017
- HOL Light QE. ~ Jacques Carette, William M. Farmer, Patrick Laskowski #ITP #HOL_Light
- Dissecting the State monad with Operational and Free monads. ~ Robbie Langer #Haskell
- El λ–cálculo (sin tipos y con tipos). ~ B.C. Ruiz y P. Guerrero #Matemáticas #Computación
- A tutorial introduction to the lambda calculus. ~ Raul Rojas #Logic #CompSci
- “Speaking” mathematics with “systems that explain themselves”. ~ Walther Neuper #ITP #Math
- RA2017: Deducción natural proposicional con Isabelle/HOL. #IsabelleHOL
- Relational equivalence proofs between imperative and MapReduce algorithms. ~ B. Beckert et als. #ITP #Coq
- The magic “Just do it” type class. ~ J. Breitner (@nomeata) #Haskell
- Numerical computing is fun (A guide to principles of computer science and numerical computing for all ages). ~ Mikko Kotila #CompSci #Python #Jupiter
- Spirals, snowflakes & trees: Recursion in pictures. ~ G. Keller (@gckeller) & M.M.T. Chakravarty (@TacticalGrace) #Haskell #Fractals
- Fractals in Haskell (Escape-time fractals created with Haskell and GD). ~ Greg Heartsfield #Haskell #Fractals
- Drawing trees with Haskell and Cairo. ~ Ilmari Heikkinen #Haskell #Fractals
- Org Beamer reference card. ~ Fabrice Niessen #Emacs #OrgMode #LaTeX
- A verified Lenstra-Lenstra-Lovász basis reduction algorithm in Isabelle/HOL. ~ J. Divasón, S. Joosten, R. Thiemann and A. Yamada #ITP #IsabelleHOL #Math
- Haskelling Bitcoin (The case for Bitcoin development in Haskell). ~ M. Alshiekh (@MAlashiekh) #Haskell #Bitcoin
- Calcul formel et preuves formelles. ~ Assia Mahboubi #ITP #Mizar #ACL2 #IsabelleHOL #HOL_Light #Coq #Agda #Lean
- A monadic framework for relational verification: Applied to information security, program equivalence, and optimizations. ~ N. Grimm et als. #SMT #Fsharp
- Exercitium: “Máxima distancia en árbol”. #Haskell #I1M2017 #I1M2017
- Efficient certification of complexity proofs: formalizing the Perron–Frobenius theorem. ~ J. Divasón et als. #ITP #IsabelleHOL
- Ciencias de la Computación (mejores programas y programadores). ~ Lourdes del Carmen González Huesca #Computación
- Curso: Lógica computacional. ~ Lourdes del Carmen González Huesca #Lógica #Computación #Haskell #Prolog #Coq
- Revisiting ‘Monadic parsing in Haskell’. ~ Vaibhav Sagar #Haskell
- Cellular Christmas Tree. ~ Mistral Contrastin (@madgen_) #Haskell
- Exercitium: “Relaciones arbóreas”. #Haskell #I1M2017
- A Coq formalization of normalization by evaluation for Martin-Löf type theory. ~ P. Wieczorek, D. Biernacki #ITP #Coq
- Logic lectures: Gödel’s basic logic course at Notre Dame. #Logic
- The wizard monoid. ~ G. González #Haskell
- Exercitium: “Recorrido del robot”. #Haskell #I1M2017
- A Lean formalization of Matiyasevič’s theorem. ~ Mario Carneiro #ITP #Lean
- 9 desafíos en 9 lenguajes de programación (#Clojure, #Erlang, #Fsharp, #Go, #Haskell, #Kotlin, #Rust, #Scala y #Swift). ~ Eduardo Díaz Cortés
- Egyptian fractions. ~ Atabey Kaygun (@Atabey_Kaygun) #CommonLisp #Math
- Free monads for cheap interpreters. ~ James Haydon #Haskell
- Exercitium: “Exponentes de Hamming”. #Haskell #I1M2017
- First-order terms in Isabelle/HOL. ~ Christian Sternagel, René Thiemann #ITP #IsabelleHOL
- Predicting the next US President by simulating the electoral college. ~ B. Kostadinov #Rstats #DataScience #CompSci
- Programs and proofs (Mechanizing Mathematics with dependent types). ~ Ilya Sergey (@ilyasergey) #ITP #Coq #Math
- Exercitium: “Dígitos iniciales”. #Haskell #I1M2017
- Treaps in Isabelle/HOL. ~ Manuel Eberl, Max Haslbeck and Tobias Nipkow #ITP #IsabelleHOL
- RA2017: Deducción natural de primer orden con Isabelle/HOL. #IsabelleHOL
- RA2017: Demostración en Isabelle/HOL de la corrección de un compilador. #IsabelleHOL
- I1M2017: Matrices en Haskell. #Haskell
- I1M2017: Ejercicios sobre vectores y matrices en Haskell. #Haskell
- LMF2017: Presentación del curso de “Lógica matemática y fundamentos”. #Lógica
- LMF2017: Sintaxis y semántica de la lógica proposicional. #Lógica
- The error function in Isabelle/HOL. ~ Manuel Eberl #ITP #IsabelleHOL
- Linus sequence. ~ Atabey Kaygun (@Atabey_Kaygun) #CommonLisp
- Lambda calculus tools and interpreter written in Haskell. #Haskell #LambdaCalculus
- For the love of algorithms. ~ Lance Fortnow (@fortnow)
- An opinionated guide to Haskell in 2018. ~ Alexis King (@lexi_lambda) #Haskell
- Twerk, a twitter archive parser with pipes utilities (in Haskell). ~ Nicolas B. (@BeRewt) #Haskell
- A verified factorization algorithm for integer polynomials with polynomial complexity. ~ Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada #ITP #IsabelleHOL
- Formal verification of spacecraft control programs using a metalanguage for state transformers. ~ A. Mokhov, G. Lukyanov, J. Lechner #Haskell
- When good components go bad: formally secure compilation despite dynamic compromise. ~ G. Fachini et als. #ITP #Coq
- Foundations of functional programming languages. ~ Andrés Sicard Ramírez #FunctionalProgramming #LambdaCalculus
- Una formalización del sistema de los números reales. ~ Jorge O. Acevedo y José L. Echeverri #ITP #Agda #Math
- ¿Qué lenguajes de programación se usan más los fines de semana? ~ Julia Silge (@juliasilge) #DataScience #Haskell via @jeiped12
- What programming languages are used most on weekends? ~ Julia Silge (@juliasilge) #DataScience #Haskell via @jeiped12
- Exercitium: “Celdas interiores de una retícula”. #Haskell #I1M2017
- Verified over-approximation of the diameter of propositionally factored transition systems. ~ M. Abdulaziz, C. Gretton, M. Norrish #ITP #HOL4
- The simply typed lambda calculus (in Agda). ~ Jonathan Prieto-Cubides #ITP #Agda #LambdaCalculus
- Monadic list functions. ~ Donnacha Oisín Kidney (@oisdk) #Haskell
- Sn̊arkl: Somewhat practical, pretty much declarative verifiable computing in Haskell. ~ G. Stewart, S. Merten, L. Leland #Haskell
- Exercitium: “División equitativa”. #Haskell #I1M2017
- Hydra Ludica: Une preuve d’impossibilité de prouver simplement. ~ P. Castéran #ITP #Coq
- Introducing the backprop library. ~ Justin Le (@mstk) #Haskell
- ¿Cómo puede “Blockchain” hacernos más libres? #Blockchain
- Org-noter: A synchronized, Org-mode, document annotator. ~ Gonçalo Santos (@weirdNox) #Emacs
- Corecursion and coinduction: what they are and how they relate to recursion and induction. ~ Mike Gordon
- What I Wish I’d Known When I Started Functional Programming. ~ Tikhon Jelvis (@tikhonjelvis) #FunctionalProgramming
- Coqatoo: Generating natural language versions of Coq proofs. ~ A. Bedford #ITP #Coq
- Exact real arithmetic implemented by fast binary Cauchy sequences. ~ Joe Hermaszewski (@expipiplus1) #Haskell #Math
- LMF2017: Sintaxis y semántica de la lógica proposicional (2). #Lógica
- Exercitium: “Huecos binarios”. #Haskell #I1M2017
- Verifying asymptotic time complexity of imperative programs in Isabelle/HOL. ~ B. Zhan, M.P.L. Haslbeck #ITP #IsabelleHOL
- My attempt to understand the backpropagation algorithm for training neural networks. ~ Mike Gordon
- The higher-order prover Leo-III. ~ A. Steen, C. Benzmüller #ITP
- Exercitium: “Recorrido de árboles en espiral”. #Haskell #I1M2017
- Proof pearl: Magic wand as frame. ~ Q. Cao, S. Wang, A. Hobor, A.W. Appel #ITP #Coq
- Reading for programmers. ~ P. Limanowski (@peel) #Emacs
- Quotes about programming and computer science. ~ A. Thompson (@alfredtwo) #Quote #Programming #CompSci
- Van Eck’s sequence. ~ Atabey Kaygun (@Atabey_Kaygun) #CommonLisp #Math
- Applicative parsing I: building the foundation. ~ James Bowen (@james_OWA) #Haskell
- Exercitium: “Períodos de Fibonacci”. #Haskell #I1M2017
- VST-Floyd: A separation logic tool to verify correctness of C programs. ~ Q. Cao, L. Beringer, S. Gruetter, J. Dodds, A.W. Appel #ITP #Coq
- Mathematical Logic in Computer Science. ~ A. Kfoury #Logic #CompSci
- Do computers really think? ~ R. Colin Johnson #AI
- From gameplay to symbolic reasoning: Learning SAT solver heuristics in the style of Alpha(Go) Zero. ~ F. Wang, T. Rompf #ATP #SAT
- Superposition with datatypes and codatatypes. ~ J.C. Blanchette, N. Peltier, S. Robillard #ATP #Vampire
- Lagrange four-square theorem examples. ~ Ken T Takusagawa #Haskell #Math
- Conventional interfaces in functional programming. ~ Carlos Morera #Haskell
- I believe P=NP. ~ Emanuele Viola #CompSci #Math
- I1M2017: Módulos en Haskell. #Haskell
- I1M2017: Las librerías de vectores y matrices. #Haskell
- I1M2017: Estadística descriptiva (y functores aplicativos). #Haskell
- I1M2017: Ejercicios de estadística descriptiva con las librerías. #Haskell
- LMF2017: Ejercicios de sintaxis y semántica de la lógica proposicional. #Lógica
- Learning a SAT solver from single-bit supervision. ~ D. Selsam et als. #ATP #SAT #NeuralNetwork
- Group theory in Haskell. ~ Spencer Hubbard #Haskell #Math
- Free monoidal functors. ~ Bartosz Milewski (@BartoszMilewski) #Haskell #CategoryTheory
- massiv: Efficient Haskell arrays featuring parallel computation. ~ Alexey Kuleshevich #Haskell
- Exercitium: “Números trimórficos”. #Haskell #I1M2017
- ProofWatch: Watchlist guidance for large theories in E. ~ Z. Goertzel, J. Jakubův, S. Schulz, J. Urban #APT
- Relational algebra in Haskell. ~ Spencer Hubbard #Haskell #Math
- Haskell exercises with automatic tests. ~ Alexey Kuleshevich #Haskell
- Atomic expressions generically. ~ Neil Mitchell #Haskell
- Exercitium: “Menor número divisible por 10^n cuyos dígitos suman n”. #Haskell #I1M2017 #Haskell #I1M2017
- ATPboost: Learning premise selection in binary setting with ATP feedback. ~ B. Piotrowski, J. Urban #ATP #ML
- Simply typed lambda calculus in Haskell. ~ Spencer Hubbard #Haskell #Math
- A verified messaging system. ~ W. Mansky, A.W. Appel, A. Nogin #ITP #Coq
- LMF2017: Consecuencia lógica y demostrabilidad. #Lógica
- Exercitium: “Árboles binarios completos”. #Haskell #I1M2017 #Haskell #I1M2017
- A formal proof of the minor-exclusion property for treewidth-two graphs. ~ C. Doczkal, G. Combette, D. Pous #ITP #Coq
- Free monoidal profunctors. ~ Bartosz Milewski (@BartoszMilewski) #Haskell #CategoryTheory
- Exercitium: “Números que no son cuadrados”. #Haskell #I1M2017 #Haskell #I1M2017
- Higher groups in Homotopy Type Theory. ~ U. Buchholtz, F. van Doorn, E. Rijke #ITP #Lean #Math #HoTT
- Journées francophones des langages applicatifs 2018 (JFLA 2018). ~ S. Boldo, N. Magaud
- Type theory and functional programming. ~ S. Thompson #eBook #FunctionalProgramming #TypeTheory
- Some notes about how I write Haskell. ~ @aisamanra #Haskell
- Constructive mathematics and computer programming. ~ P. Martin-Löf #Math #CompSci
- Automated reasoning and ultra-intuitionism. ~ R.L. Constable #Logic #ATP #ITP
- Educating computer science educators online (A Racket MOOC for elementary math teachers of Finland). ~ T. Partanen, P. Niemelä, L. Mannila, T. Poranen #Racket
- Exercitium: “Vértices de un cuadrado”. #Haskell #I1M2017 #I1M2017
- A Coq formalisation of a core of R. ~ M. Bodin #ITP #Coq #Rstats
- Beauty and the beast (Eta Haskell for JVM). ~ Jarek Ratajski (@jarek000000) #Haskell
- David Hilbert y la defensa del rigor matemático. ~ F. Bombal #Matemáticas
- ASCII fractals in Haskell. ~ Jan Mas Rovira #Haskell
- Logic programming applications: What are the abstractions and implementations? ~ Y.A. Liu #LogicProgramming
- Making agile development processes fit for V-style certification procedures. ~ S. Bezzecchi, P. Crisafulli, C. Pichot, B. Wolff #ITP #IsabelleHOL
- A minimal (<500 LOC) programming language capable of proving theorems about its own terms. #Haskell #Logic
- Un fallo de programación desvió al primer Ariane 5 de 2018 de su trayectoria. ~ @Wicho #Programación
- Let’s not forget the ‘Science’ in ‘Computer Science’. ~ W.S. Saba #CompSci
- Comparing classical and relativistic kinematics in first-order logic. ~ K. Lefever, G. Székely #Logic #Physics
- Modal logic! Propositional logic! Tableaux! ~ R. Zach (@RrrichardZach) #Logic via @OpenLogicProj
- Boxes and diamonds (An open introduction to modal logic). ~ R. Zach (@RrrichardZach) #eBook #Logic
- A multi-language computing environment for literate programming and reproducible research. ~ E. Schulte, D. Davison, T. Dye, C. Dominik #Emacs
- Org-mode and R: An introduction. ~ Erik Iverson #Emacs #OrgMode #Rstats
- The emacs org-mode (Reproducible research and beyond). ~ A. Leha #Emacs #OrgMode #Rstats
- I1M2017: Combinatoria en Haskell. #Haskell #Matemáticas
- I1M2017: Cálculo numérico en Haskell. #Haskell #Matemáticas
- I1M2017: Cálculo simbólico con Maxima. #Maxima #Matemáticas
- LMF2017: Deducción natural proposicional (1). #Lógica
- Verified memoization and dynamic programming. ~ S. Wimmer, S. Hu, T. Nipkow #ITP #IsabelleHOL
- Notes on category theory in the context of (functional) programming. ~ J.W. Buurlage #FunctionalProgramming #Haskell #CategoryTheory
- ASTs with Fix and Free. ~ Chris Penner #Haskell
- Getting started with Org mode. ~ Harry Schwartz #Emacs #OrgMode
- SLC2018: Presentación del “Seminario de Lógica Computacional” (2018).
- Reproducibility and Old Faithful. ~ Dominic Steinitz (@idontgetoutmuch) #Haskell #DataScience
- Exercitium: “Matrices dispersas”. #Haskell #I1M2017 #Haskell #I1M2017
- Abstract completion, formalized. ~ N. Hirokawa, A. Middeldorp, C. Sternagel, S. Winkler #IsabelleHOL
- Using Emacs, Org-mode and R for research writing in social sciences (A toolkit for writing reproducible research papers and monographs). ~ Vikas Rawal #Emacs #OrgMode #Rstats
- Coqatoo: Generates natural language versions of Coq proofs. ~ Andrew Bedford #ITP #Coq
- Liquid Haskell tutorial. ~ Andres Löh #Haskell #LiquidHaskell
- Exercitium: “Representación reducida de matrices dispersas”. #Haskell #I1M2017
- Faithful semantical embedding of a dyadic deontic logic in HOL. ~ C. Benzmüller, A. Farjami, X. Parent #ITP #IsabelleHOL #Logic
- Formal proof: reconciling correctness and understanding. ~ C.S. Calude, C. Müller #ITP #Logic
- A collection of short Org-mode snippets demonstrating the usage of code blocks. ~ Eric Schulte #Emacs #OrgMode
- Why data science is simply the new astrology. ~ Karthik Shashidhar #DataScience
- Exercitium: “Representación ampliada de matrices dispersas”. #Haskell #I1M2017 x pero no por y”]]. #Haskell #I1M2017
- Hoare logics for time bounds. ~ M.P.L. Haslbeck, T. Nipkow #ITP #IsabelleHOL #SLC2018
- Paradigms of artificial intelligence programming: case studies in Common Lisp. ~ Peter Norvig #eBook #AI #CommonLisp
- A categorical manifesto. ~ J.A. Goguen #CategoryTheory #CompSci #Math
- A theory of functional programming. ~ Eric Normand (@ericnormand) #FunctionalProgramming
- Links to some of the most famous articles about mathematics. #Math
- The death of proof. ~ John Horgan #Math
- The immortaility of proof. ~ Steven G. Krantz #Math
- A DARPA perspective on Artificial Intelligence. ~ John Launchbury #AI
- Interpretable machine learning (A guide for making black box models explainable). ~ Christoph Molnar (@ChristophMolnar) #MachineLearning #XAI
- Timeline of artificial intelligence. #AI
- Build large polyglot projects with Bazel … now with Haskell support. ~ M. Boespflug, M. Karpov, M. Kowalczyk #Haskell #Bazel
- El sistema de tipos de Haskell/GHC y sus extensiones. ~ Guillaume Hoffmann (@guion19) #Haskell