Resumen de lecturas compartidas (diciembre de 2017)
Esta entrada es una recopilación de lecturas compartidas, durante diciembre 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.
- Exercitium: “Sumas de dos cuadrados”. #Haskell #I1M2017 #Haskell #I1M2017
- Teaching the formalization of mathematical theories and algorithms via the automatic checking of finite models. ~ W. Schreiner, A. Brunhuemer, C. Fürst #ITP #Math #RISCAL
- Números piramidales de cuatro dimensiones. ~ Antonio Roldán (@Connumeros) #Matemáticas #Programación
- November 2017 1HaskellADay problems and solutions. ~ Douglas M. Auclair (@geophf) | Typed Logic #Haskell #1HaskellADay
- From logic programming to machine ethics. ~ A. Saptawijaya, L.M. Pereira #LogicProgramming #KRR #AI
- Tierless Web programming in ML. ~ G. Radanne #PhD_Thesis #FunctionalProgramming #OCaml
- A domain specific language for drum beat programming. ~ A.R. Du Bois, R. Ribeiro #Haskell #DSL #Music
- RA2017: Ejercicios de razonamiento detallado sobre programas en Isabelle/HOL. #IsabelleHOL
- RA2017: Razonamiento por casos y por inducción en Isabelle/HOL. #IsabelleHOL
- I1M2017: 2º examen de programación funcional con Haskell. #Haskell
- I1M2017: Evaluación perezosa en Haskell. #Haskell
- A formal proof in Coq of a control function for the inverted pendulum. ~ D. Rouhling #ITP #Coq #Math #Physics
- Writing code like a mathematical proof. ~ Spiro Sideris #Math #Programming
- Haskell for dummies. ~ M. Snoyman (@snoyberg) #Haskell
- CompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler. ~ D. Kästner et als. #ITP #Coq #CompCert
- Reflecting on Haskell in 2017. ~ Stephen Diehl (@smdiehl) #Haskell
- Exercitium: “Conjunto de relaciones binarias entre dos conjuntos”. #Haskell #I1M2017 #I1M2017
- Slides and other materials for functional programming lectures ITMO university. ~ D. Kovanikov, A. Seroka #Haskell
- Point-free or die: tacit programming in Haskell and beyond. ~ Amar Shah #Haskell
- Voting with ties: Strong impossibilities via SAT solving. ~ F. Brandt, C. Saile, C. Stricker #SAT_solving
- Exercitium: “Menor x tal que los x múltiplos de n contienen todos los dígitos”. #Haskell #I1M2017 elementos”]]. #Haskell #I1M2017
- A constructive formalisation of semi-algebraic sets and functions. ~ B. Djalal #ITP #Coq #Math
- Arithmetic coding. ~ Jeremy Gibbons (@jer_gib) #Haskell #Math
- Exercitium: “Reconocimiento de relaciones funcionales entre dos conjuntos”. #Haskell #I1M2017 #I1M2017
- Finding bugs in Haskell code by proving it. ~ J. Breitner (@nomeata) #Haskell
- Using Haskell on the frontend. ~ Vanessa McHale #Haskell
- La inteligencia artificial que caza noticias para Reuters en Twitter. ~ David Sarabia (@DSRELD) #IA
- Reuters Tracer: toward automated news production using large scale social media data. ~ X. Liu et als. #AI #BigData
- learn elm: discover why people are switching to Elm and how you can get started today! #elm
- Un bestiario fractal de curvas para rellenar el espacio (y el cerebro). ~ @Alvy #Fractales
- Brainfilling curves: a fractal bestiary. ~ Jeffrey Ventrella
- A complete taxonomy of plane-filling curves. ~ Jeffrey Ventrella #Fractal
- Analyzing individual proofs as the basis of interoperability between proof systems. ~ G. Dowek #ITP #Coq #IsabelleHOL
- Functional pearl: integer partitions and QuickCheck. ~ Vanessa McHale #Haskell
- Exercitium: “Expresiones equilibradas”. #Haskell #I1M2017 #I1M2017
- Secret link uncovered between pure math and physics. ~ Kevin Hartnett #Math #Physics
- Cómo compartir un secreto usando sistemas de ecuaciones lineales. ~ A. Cano, J.M. LunA, A. Rojas #Matemáticas
- The mind as a computational system. ~ Christoph Adami #AI
- Geometría axiomática. ~ Gerard Romo Garrido #Matemáticas
- Variations on a theme: A set of curated examples meant to show Haskell’s expressiveness. ~ Vanessa McHale #Haskell
- Exercitium: “Conjunto de funciones entre dos conjuntos”. #Haskell #I1M2017
- P = NP: Perhaps I change my mind. (An old result put a new way). ~ R.J. Lipton, K.W. Regan #Math #CompSci
- Mathematicians crack the cursed curve. ~ Kevin Hartnett #Math
- Notes on mathematical writing. ~ Clark Barwick #Math
- Rings: an efficient Java/Scala library for polynomial rings. ~ S. Poslavsky #Scala #Math
- Towards automatic resource bound analysis for OCaml. ~ J. Hoffmann, A. Das, S.C. Weng #OCaml
- The role of theory in Deep Learning. ~ David McAllester #AI #DeepLearning
- Computation in Logic and Logic in Computation. ~ S. Salehi #Logic #CompSci
- Exercitium: “Mayúsculas y minúsculas alternadas”. #Haskell #I1M2017 #I1M2017
- All about strictness analysis (part 1). ~ Sebastian Graf (@sgraf1337) #Haskell
- Introduction to logic programming with Prolog. ~ Mathias Schilling (@MatChilling) #Prolog
- Co finds a pairing. ~ Phil Freeman (@paf31) #Haskell
- Streaming arithmetic coding. ~ Jeremy Gibbons (@jer_gib) #Haskell #Math
- A framework for certified self-stabilization. ~ S. Devismes, P. Corbineau, K. Altisen #ITP #Coq
- Getting things done in Haskell. ~ Jasper Van der Jeugt (@jaspervdj) #Haskell
- Exercitium: “Aplicación de lista de funciones a lista de elementos”. #Haskell #I1M2017 #I1M2017
- Dismal arithmetic. ~ D. Applegate, M. LeBrun, N.J.A. Sloane #Math
- The Haskell pyramid. ~ Patrick Nielsen (@pmylund) #Haskell
- fugacious: An example Haskell Web application. ~ Jasper Van der Jeugt (@jaspervdj) #Haskell
- swMATH: An information service for mathematical software. #Math #CompSci
- Exercitium: “Máximo de las rotaciones restringidas”. #Haskell #I1M2017
- Computational Logic: its origins and applications. ~ L.C Paulson #Logic #ITP #IsabelleHOL
- Monadification of functional programs. ~ M. Erwig, D. Ren #Haskell
- Exercitium: “Caminos minimales en un árbol numérico”. #Haskell #I1M2017
- An interactive introduction to quantum computing (or what do you mean they can be both zero and one at the same time!) ~ D. Kemp #CompSci
- Efficiency is not associative for matrix multiplication. ~ J.D. Cook @JohnDCook #Math #CompSci
- A brief introduction to category theory. ~ D. Hofmann #CategoryTheory
- I1M2017: Ejercicios de evaluación perezosa y listas infinitas en Haskell (1). #Haskell
- Applications of automated reasoning. ~ J. Harrison #AutomatedReasoning
- El Tao de la programación. #Programación
- The Tao of programming. #Programming
- Verified iptables firewall analysis & verification. ~ C. Diekmann, L. Hupel, J. Michaelis, M. Haslbeck, G. Carle #ITP #IsabelleHOL
- A tour of Go in Haskell. ~ Osanai Kazuyoshi #Haskell
- Exercitium: “Ordenación valle”. #Haskell #I1M2017
- Reading simple Haskell. ~ Gil Mizrahi #Haskell
- Continuation passing style Free Monads and direct style Free Monads. ~ Quentin Duval @quduval #Idris
- Folding Christmas fractals. ~ Clarissa Grandi (@c0mplexnumber) #Math
- Online Turing machine simulator. ~ Martín Ugarte #CompSci #Turing
- RA2017: Ejercicios dec uantificadores sobre listas en Isabelle/HOL. #IsabelleHOL
- RA2017: Razonamiento sobre árboles y bosques en Isabelle/HOL. #IsabelleHOL
- I1M2017: Programas interactivos en Haskell. #Haskell
- I1M2017: Definiciones de la lista infinita de factoriales en Haskell. #Haskell #Matemáticas
- A logical relation for monadic encapsulation of state (proving contextual equivalences in the presence of runST). ~ A. Timany et als. #ITP #Coq #Haskell
- What makes Haskell unique. ~ M. Snoyman (@snoyberg) #Haskell
- safe-money: Money in the type system where it belongs. ~ Renzo Carbonara #Haskell
- Emacs: Org mode, programing language code markup. ~ Xah Lee (@xah_lee) #Emacs #Programming #OrgMode
- taskell: A command line task manager written in Haskell. ~ Mark Wales #Haskell
- Logic books of the year? ~ Peter Smith #Logic
- SLS: Songbird + Lemma Synthesis (a separation logic prover which can automatically synthesize inductive lemmas on-the-fly). #ATP #OCaml
- An axiomatic basis for bidirectional programming. ~ H.S. Ko, Z. Hu #ITP #Agda
- Bonsai: synthesis-based reasoning for type systems. ~ K. Chandra, R. Bodik #Racket
- Exercitium: “Número de viajeros en el autobús”. #Haskell #I1M2017
- Collapsing towers of interpreters. ~ N. Amin, T. Rompf #Lisp #Scala
- Debug: Haskell library for debugging. ~ Neil Mitchell #Haskell
- Fast and fearless evolution of server-side Web applications. ~ Oskar Wickström (@owickstrom) #Haskell
- A water-based solution of polynomial equations. ~ Mark Levi #Math
- Safety and conservativity of definitions in HOL and Isabelle/HOL. ~ O. Kunčar, A. Popescu #ITP #IsabelleHOL
- The string search algorithm by Knuth, Morris and Pratt in Isabelle/HOL. ~ F. Hellauer, P. Lammich #IsabelleHOL
- Monadic “do” block, yet again (What should get into your “do” block?) ~ Arvind Devarajan #Haskell
- Exercitium: “Reconocimiento de recorridos correctos”. #Haskell #I1M2017
- Lambda calculus in Clojure (part 1). ~ Sergio Rodrigo Royo #LambdaCalculus #Clojure
- Haskell in production in a startup in 2017? Yup. ~ Frédéric Menou (@ptit_fred), Clément Delafargue (@clementd) #Haskell
- Functional programming with graphs. ~ @futtetennista #Haskell
- Solving satisfiability using inclusion-exclusion. ~ A. Zaleski #Logic #Sat #Maple
- The Haskell performance checklist. ~ Chris Done (@christopherdone) #Haskell
- Exercitium: “Bosque de recorridos del autobús”. #Haskell #I1M2017 #I1M2017
- Benchmarks for numbers: ints, doubles, bignums, rationals, etc. ~ Chris Done (@christopherdone) #Haskell
- Splitting and splicing intervals (part 1). ~ R. Jhala (@RanjitJhala) #Haskell #LiquidHaskell
- De Lutero a Voevodsky, pasando por Brouwer: Reformas en matemáticas. ~ J. Ferreirós #Matemáticas
- Exercitium: “Aplicaciones biyectivas”. #Haskell #I1M2017
- I1M2017: Representación gráfica de funciones en Haskell con GNUplot. #Haskell
- I1M2017: Programación de dibujos por comprensión en CodeWorld/Haskell. #Haskell #CodeWorld
- I1M2017: Programación de dibujos por recursión en CodeWorld/Haskell. #Haskell #CodeWorld
- A library for algorithmic game theory in Ssreflect/Coq. ~ A. Bagnall, S. Merten, G. Stewart #ITP #Coq
- Building Haskell apps with Docker. ~ D. Bertovic #Haskell via @FPComplete
- Exercitium: “Menor con suma de dígitos dada”. #Haskell #I1M2017
- All about reflection: a tutorial. ~ A. Spiwack #Haskell
- A Lisp REPL in your pocket. ~ Kvardek Du #Lisp #Android
- Reasoning about program behavior algebraically. ~ Stephen Diehl (@smdiehl) #Haskell
- Understanding simplicity: implementing a smart contract language in 30 lines of Haskell. ~ Dan Robinson #Haskell
- Evolutionary programming converts darwinism into algorithms. ~ R. Colin Johnson #Programming #AI
- The Mason–Stother’s theorem. ~ Manuel Eberl #ITP #IsabelleHOL
- Some notes about how I write Haskell. ~ Getty Ritter (@aisamanra) #Haskell
- Exercitium: “Cadenas opuestas”. #Haskell #I1M2017
- Zipperposition: An automatic theorem prover in OCaml for typed logic with equality, datatypes and arithmetic. ~ Simon Cruanes #OCaml #ATP #Logic
- Extending superposition with integer arithmetic, structural induction, and beyond. ~ Simon Cruanes #PhD_Thesis #OCaml #ATP #Logic
- Programas artístico-matemáticos en menos de 280 caracteres. ~ @Alvy #Programación #Matemáticas
- Introduction to singletons (Part 1). ~ Justin Le (@mstk) #Haskell
- On possible use of quantifier elimination software in upper secondary mathematics education. ~ Y. Sato, R. Fukasaku #Math #Logic
- The median-of-medians selection algorithm. ~ Manuel Eberl #ITP #IsabelleHOL
- Exercitium: “Vecino en lista circular”. #Haskell #I1M2017 primos”]]. #Haskell #I1M2017
- Integrated simulation and formal verification of a simple autonomous vehicle. ~ A_ Domenici, A. Fagiolini, M. Palmieri #Formal_verification #ITP #PVS
- importify: manage Haskell imports quickly. ~ Dmitry Kovanikov et als. #Haskell
- Exercitium: “Suma de las hojas de mínimo nivel”. #Haskell #I1M2017 #Haskell #I1M2017
- Beginning Computer Science with R. ~ H. White #CompSci #Rstats
- Protolude: A sensible starting Prelude for building custom Preludes. ~ Stephen Diehl (@smdiehl) #Haskell
- Scaling Isabelle proof document processing. ~ M. Wenzel #IsabelleHOL
- Exercitium: “Sumable sin vecinos”. #Haskell #I1M2017.
- Getting used to R, RStudio, and R Markdown. ~ C. Ismay #Rstats
- Tiny art in less than 280 characters. ~ Antonio S. Chinchón (@aschinchon) #Rstats
- Programar (en R) te da alas. ~ Antonio S. Chinchón (@aschinchon) #Rstats
- Formal proof of polynomial-time complexity with quasi-interpretations. ~ H. Férée et als. #ITP #Coq
- Exercitium: “Rotaciones divisibles por 8”. #Haskell #I1M2017
- A library for algorithmic game theory in Ssreflect/Coq. ~ A- Bagnall, S. Merten, G. Stewart #ITP #Coq
- Annotated multisemantics to prove Non-Interference analyses. ~ G. Cabon, A. Schmitt #ITP #Coq