Resumen de lecturas compartidas durante agosto de 2018
Esta entrada es una recopilación de lecturas compartidas, durante agosto de 2018, en Twitter fundamentalmente 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.
Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
- Formalization of the arithmetization of Euclidean plane geometry and applications. ~ P. Boutry, G. Braun, J. Narboux #ITP #Coq #Math
- Formal probabilistic analysis of dynamic fault trees in HOL4. ~ Y. Elderhalli, W. Ahmad, O. Hasan, S. Tahar #ITP #HOL4
- Learning statistics with R (A tutorial for psychology students and other beginners). ~ Danielle Navarro #Statistics #Rstats
- Art vs. science in mathematical discovery. ~ J. Polak #Math
- Making Haskell as fast as C: Imperative programming in Haskell. ~ Henri Verroken #Haskell
- Learn functional Python in 10 minutes. ~ Brandon Skerritt #FunctionalProgramming #Python
- Aggregates tables in Org mode. ~ Thierry Banel #Emacs #OrgMode
- Who needs category theory? ~ A. Blass, Y. Gurevich #CategoryTheory
- Tricks in Coq: Some tips, tricks, and features in Coq that are hard to discover. ~ Tej Chajed #ITP #Coq
- An Answer Set Programming environment for high-level specification and visualization of FCA. ~ L. Bourneuf #ASP #FCA
- Make your code easier to read with Functional Programming. ~ Cristi Salcescu #FunctionalProgramming #JavaScript
- Two years of functional programming in JavaScript: lessons learned. ~ Victor Nakoryakov #FunctionalProgramming #JavaScript
- The science behind functional programming. ~ Rafa Paradela #FunctionalProgramming #CategoryTheory
- Pros and cons of functional programming. ~ Iren Korkishko #FunctionalProgramming
- An introduction to functional programming in JavaScript. ~ Matt Banz #FunctionalProgramming #JavaScript
- A Coq mechanised formal semantics for realistic SQL queries * Formally reconciling SQL and bag relational algebra ~ V. Benzaken, É. Contejean #ITP #Coq
- An introduction to artificial intelligence and law. ~ K. Ashley, T. Gordon. #AI
- Top 10 roles in AI and data science. ~ Cassie Kozyrkov #AI #DataScience
- Summarized Slack from Deepspec Summer School 2017. #DSSS17 #ITP #Coq
- Purely functional games. ~ Gil Mizrahi #FunctionalProgramming #Haskell #Game
- Purely functional games (How I built a game in Haskell – pure functional style). Gil Mizrahi [Slides] #FunctionalProgramming #Haskell #Game
- GHC, one compiler to RULE them all. ~ Alexandre Moine #Haskell
- Introduction to the rank-select bit-string. ~ John Ky #FunctionalProgramming #Haskell
- QuickSpec and the quest for good lemmas. ~ Daniel Selsam #Haskell
- Parametric polymorphism and operational improvement. ~ J. Hackett, G. Hutton. #FunctionalProgramming #Haskell
- The simple essence of automatic differentiation. ~ Conal Elliott #FunctionalProgramming #CategoryTheory #Haskell
- Teaching how to program using automated assessment and functional glossy games (experience report). ~ J. Bacelar Almeida et als. #Teaching #FunctionalProgramming #Haskell
- DAOconCoq T3: Datos estructurados en Coq. #ITP #Coq
- Demostración Asistida por Ordenador (3 primeros capítulos). #DAOconCoq #ITP #Coq
- Compositional soundness proofs of abstract interpreters. ~ S. Keidel, C. Bach Poulsen, S. Erdweg. #Haskell
- Elaborating dependent (co)pattern matching. ~ J. Cockx, A. Abel. #Agda
- Capturing the future by replaying the past (functional pearl). ~ J. Koppel, G. Scherer, A. Solar-Lezama. #FunctionalProgramming #SML
- MoSeL: a general, extensible modal framework for interactive proofs in separation logic. ~ R. Krebbers et als. #ITP #Coq
- What you needa know about Yoneda: profunctor optics and the Yoneda lemma (functional pearl). ~ G. Boisseau, J. Gibbons. #FunctionalProgramming #Haskell #CategoryTheory
- Relational algebra by way of adjunctions. ~ J. Gibbons et als. #FunctionalProgramming #Haskell #CategoryTheory
- Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report). ~ J. Breitner et als. #Haskell #Coq
- A type and scope safe universe of syntaxes with binding: their semantics and proofs. ~ G. Allais et als. #Agda
- DAOconCoq T4: Polimorfismo y funciones de orden superior en Coq. #ITP #Coq
- Demostración Asistida por Ordenador (4 primeros capítulos). #DAOconCoq #ITP #Coq
- Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam. ~ A. Stampoulis, A. Chlipala. #Metaprogramming #Prolog
- Equivalences for free: univalent parametricity for effective transport. ~ N. Tabareau, É. Tanter, M. Sozeau. #Coq #HoTT
- Fault tolerant functional reactive programming (functional pearl). ~ I. Perez #FunctionalProgramming #Haskell #Idris
- Partially-static data as free extension of algebras. ~ J. Yallo et als. #FunctionalProgramming #Haskell
- Boolean constraints in SWI-Prolog: A comprehensive system description. ~ Markus Triska #Prolog #CLP
- Lecture notes on Iris: Higher-order concurrent separation logic. ~ L. Birkedal, A. Bizjak #ITP #Coq #Logic
- A guide to GHC’s extensions. ~ Jannis Limperg #Haskell
- Libro de exámenes de programación funcional con Haskell (versión del 4 de agosto de 2018). #Haskell #I1M2017
- Mathematical olympiad in China (problems and solutions). #Math
- The history and concept of mathematical proof. ~ S. G. Krantz. #Math
- Mathematical proof. ~ Wikipedia #Math
- I1M2017: Libro de ejercicios resueltos de programación funcional en Haskell del curso 2017-18 (versión del 5 de agosto de 2018). #Haskell
- Suggesting valid hole fits for typed-holes (Experience report). ~ Matthías Páll Gissurarson #Haskell
- hgeometry: A simple geometry library in Haskell. ~ Frank Staals #Haskell #Math
- Composing iterator-returning functions. ~ Manuel Vázquez Acosta #Python #Haskell
- Lidl software disaster another example of Germany’s digital failure. ~ F. Kolf, C. Kerkmann #Sofware #Bug
- OpenStax: openly licensed textbooks. #eBooks
- Computing integer sequences: Filtering vs generation (Functional pearl). ~ I. Salvo, A. Pacifico #FunctionalProgramming #Haskell
- Coherent explicit dictionary application for Haskell: Formalisation and coherence proof. ~ T. Winant, D. Devriese #Haskell
- Demostración asistida por ordenador con Isabelle/HOL. #DAO #IsabelleHOL
- An invitation to functional programming (for mathematicians). ~ Sonat Süer #FunctionalProgramming #Haskell
- Haskell ain’t maths. ~ Dan Ghica #Haskell #Maths
- Monoid homomorphisms (Part 1 of 2). ~ Sonat Süer #CategoryTheory #Haskell
- Categorifying cardinal arithmetic. ~ Emily Riehl #Math #CategoryTheory
- Desperately seeking integers (A few twists on Turing’s proof of undecidability of predicate calculus). ~ R.J. Lipton, K.W. Regan #Logic #Math
- Category theory in PL research. ~ N. Krishnaswami #CategoryTheory #CompSci
- Habits of highly mathematical people. ~ Jeremy Kun #Math
- A short guide to hard problems. ~ Kevin Hartnett #Math #CompSci
- Discover “Unpaywall,” a new (and legal) browser extension that lets you read millions of science articles normally locked up behind paywalls.
- Haskell with only one type family. ~ Xia Li-yao #Haskell
- Keeping it clean: Haskell code formatters. ~ James Bowen #Haskell
- Topological models of arithmetic. ~ A. Enayat, J.D. Hamkins, B. Wcisło #Logic #Math
- Semantics of Mizar as an Isabelle object logic. ~ C. Kaliszyk, K. Pąk #ITP IsabelleHOL #Mizar #Logic
- From algebra to abstract machine: a verified generic construction. ~ C.T. Cortiñas, W. Swierstra #FunctionalProgramming #ITP #Agda
- “Concrete semantics” with Coq and CoqHammer. ~ Ł. Czajka, B. Ekici, C. Kaliszyk #ITP #Coq #IsabelleHOL
- Coq version of (part of) the HOL-IMP theories accompanying the book “Concrete Semantics with Isabelle/HOL”. Formalized using CoqHammer. #ITP #Coq
- Enif-Lang: A specialized language for programming network functions on commodity hardware. ~ N. Bonelli, S. Giordano, G. Procissi #Haskell
- Data-parallel rank-select bit-string construction. ~ John Ky #Haskell
- Monoid homomorphisms (Part 2 of 2). ~ Sonat Süer #CategoryTheory #Haskell
- Learning Haskell: Miscellaneous enlightenments. ~ Sandeep C R #Haskell
- Template Haskell tutorial. ~ Mark Karpov #Haskell
- 100 best websites for mathletes. #Math
- Lambda calculus – step by step. ~ Helmut Brandl #LambdaCalculus #Logic #Math
- An outsider’s guide to statically typed functional programming. ~ Brian Marick #FunctionalProgramming #Elm #PureScript
- DAOconCoq T5: Tácticas básicas de Coq. #ITP #Coq
- Demostración Asistida por Ordenador con Coq (5 primeros capítulos). #DAOconCoq #ITP #Coq
- Currying in calculus, PDEs, programming, and categories. ~ J.D. Cook #Math #FunctionalProgramming #Haskell #CategoryTheory
- Breaking the space-time barrier with Haskell: Time-traveling and debugging in CodeWorld. ~ Krystal Maughan #Haskell #CodeWorld
- Improving typeclass relations by being open. ~ G. Martínez, M. Jaskelioff, G. De Luca #Haskell
- Type-safe data versioning in Haskell. ~ Lorenzo Tabacchini #Haskell
- State of Haskell 2018. ~ Aaron Contorer #Haskell
- Paradox at the heart of mathematics makes physics problem unanswerable. ~ Davide Castelvecch #Logic #Math #Physics
- Fast Sudoku solver in Haskell #3: Picking the right data structures. ~ Abhinav Sarkar #Haskell
- A formal proof of the expressiveness of deep learning. ~ A. Bentkamp, J.C. Blanchette, D. Klakow. #ITP #IsabelleHOL #DeepLearning
- Extensible type-directed editing. ~ J. Korkut, D.T. Christiansen #FunctionalProgramming #Idris
- Approximating compiling to categories using type-level Haskell: Take 2. ~ Philip Zucker #FunctionalProgramming #Haskell
- A formally verified proof of the Mason-Stothers theorem in Lean. ~ J. Wagemaker #ITP #Lean #Math
- Ghosts of departed proofs (Functional pearl). ~ Matt Noonan #Haskell
- Type theory as a framework for modelling and programming. ~ C. Ionescu, P. Jansson, N. Botta. #FunctionalProgramming
- Proof theory. ~ Michael Rathjen #Logic
- Mathematical surprises. ~ Dave Richeson #Math
- A verified SAT solver framework with learn, forget, restart, and incrementality. ~ J.C. Blanchette et als. #ITP #IsabelleHOL #SAT
- Newbie’s guide to Deep Learning (Taking baby steps when starting DL). ~ Arkar Min Aung #DeepLearning
- Minsky machines in Isabelle/HOL. ~ Bertram Felgenhauer #ITP #IsabelleHOL
- Some fundamental theorems in Mathematics. ~ Oliver Knill #Math
- Divide and conquer algorithms. ~ Brandon Skerritt #Algorithms
- Typeclass induction and developing a QuickCheck-like library. ~ Marcelo Zabani #FunctionalProgramming #Haskell
- Folds on lists. ~ Jeremy Gibbons #FunctionalProgramming #Haskell
- Cube composer: A puzzle game inspired by functional programming. ~ David Peter #FunctionalProgramming #PureScript #Game
- Proof simplification and automated theorem proving. ~ Michael Kinyon #ATP #Prover9
- The Boyer-Moore waterfall model revisited. ~ P. Papapanagiotou, J. Fleuriot #ITP #HOL_Light
- A very small SAT solver. ~ Maximilian Algehed #FunctionalProgramming #Haskell #Logic #SAT
- From informal to formal proofs in euclidean geometry. ~ S Stojanovic-Ður #ATP #TPTP #Math
- Pearls of Scala functional programming, Part I (1. Smallest free number: array-based solution). ~ Baseer Al-Obaidy #FunctionalProgramming #Scala
- Functional programming in Python (Creating transformation pipelines in Python). ~ Dennis Vriend #FunctionalProgramming #Python
- Introducing computer science to high school students through logic programming. ~ T.T. Yuen, M. Reyes, Y. Zhang. #LogicProgramming #ASP #Teaching
- Using Erlang in research and education in a technical university. ~ I. Petrov, A. Alexeyenko, G. Ivanova. #FunctionalProgramming #Erlang #Teaching
- Lenses for philosophers. ~ Jules Hedges #CategoryTheory
- Categorical data analysis. ~ John D. Cook #CategoryTheory
- How to turn a Dromedary camel into a Bactrian camel. ~ Alexander Klink #FunctionalProgramming #Haskell
- Exercises and notes from the Coursera Machine Learning Course by Andrew Ng. ~ Michael Chavinda #FunctionalProgramming #Haskell #MachineLearning
- ZuriHac 2018: Haskell hackathon in Rapperswil. ~ Ivan Krišto. #FunctionalProgramming #Haskell
- Solving the mystery behind Abstract Algorithm’s magical optimizations. ~ Victor Maia #Haskell
- Abusing the continuation monad. ~ Jules Hedges #FunctionalProgramming #Haskell
- Programs and proofs in the Coq proof assistant. ~ Arthur Azevedo de Amorim and Robert Rand. #ITP #Coq
- QED version 2.0: an interactive text in first-order logic. ~ Terence Tao #Teaching #Logic
- Demystifying functional programming (in a real company). ~ Caio Oliveira #FunctionalProgramming
- Why referential transparency matters? ~ Stéphane Derosiaux #FunctionalProgramming
- Eliminating unstable tests in floating-point programs. ~ L. Titolo, C.A. Muñoz, M.A. Feliú, and M.M. Moscato. #FormalVerification #PVS
- DAOconCoq T6: Lógica en Coq. #DAO #Coq #Lógica
- Demostración Asistida por Ordenador con Coq (6 primeros capítulos). #DAOconCoq #DAO #Coq #ProgramaciónFuncional #Lógica
- SBVPlugin: Formally prove properties of Haskell programs using SBV/SMT. ~ Levent Erkök #Haskell
- A Haskell compiler. ~ David Tereil #Haskell
- Recursion schemes for higher algebras. ~ Bartosz Milewski #FunctionalProgramming #Haskell #CategoryTheory
- Sobre la ética de los asistentes inteligentes. ~ @Alvy #IA
- Towards an ethics of AI assistants: An initial framework. ~ John Danaher #AI
- Excelencia universitaria y elitismo. ~ Francisco R. Villatoro (#Universidad
- From fast exponentiation to square matrices: An adventure in types. ~ Chris Okasaki #FunctionalProgramming #Haskell
- What programming language should a professional mathematician know? #Math #Programming #CompSci
- Esta red neuronal aplica leyes físicas aprendidas de forma automática. #IA #Física
- Discovering physical concepts with neural networks. ~ R. Iten et als. #MachineLearning #Physics
- How to get into Machine Learning for a Haskeller. ~ Dennis Gosnell #Haskell #MachineLearning
- Water jug rewrite with Haskell (Part I). ~ Vignesh Sarma K #Haskell
- A verified simple prover for first-order logic. ~ J. Villadsen, A. Schlichtkrull, A.H. From. #ITP #IsabelleHOL
- Formalisation of a frame stack semantics for a Java-like language. ~ A Schubert, J. Chrząszcz. #ITP #Coq
- The conception, evolution, and application of functional programming languages. ~ Paul Hudak #FunctionalProgramming
- LiquidHaskell: Experience with refinement types in the real world. ~ N. Vazou, E.L. Seidel, R. Jhala #Haskell #LiquidHaskell
- Functional programming for mortals with Scalaz. ~ Sam Halliday #FunctionalProgramming #Scala #Scalaz
- Source and examples to “Functional Programming for Mortals with Scalaz”. ~ Sam Halliday #FunctionalProgramming #Scala #Scalaz
- CoSMed: A confidentiality-verified social media platform. ~ T. Bauereiß et als. #ITP #IsabelleHOL
- Review of: “CoSMed: a confidentiality-verified social media platform”. ~ Simon Thompson #ITP #IsabelleHOL
- Mathematics and programming – the easy languages to learn. ~ A. Egri-Nagy #Math #CompSci
- A new algebraic approach to decision making in a railway interlocking system based on preprocess. A. Hernando, R. Maestre, E. Roanes-Lozano. #Math #CompSci
- Matemáticos y acusmáticos. ~ Lucio Fernando Ruíz #Matemáticas
- The proof: Monad as a monoid in category of endofunctors. ~ Wojtek Pituła #FunctionalProgramming #Scala
- The abstract calculus. ~ Victor Maia #FunctionalProgramming #Haskell
- You should learn functional programming in 2018. ~ Allan MacGregor #FunctionalProgramming
- Using circular programs for higher-order syntax (Functional pearl). ~ E. Axelsson, K. Claessen. #FunctionalProgramming #Haskell
- Writing fast Haskell (Elegance is not an excuse for bad performance). ~ Moritz Kiefer #FunctionalProgramming #Haskell
- Marrying Haskell and Hyper-Threading. ~ Alexander Vershilov #FunctionalProgramming #Haskell
- How functional programming can be awesome: Tail recursion elimination. ~ Luciano Strika #FunctionalProgramming #Python #Haskell
- Bit-manipulation operations for high-performance succinct data-structures and CSV parsing. ~ John Ky #FunctionalProgramming #Haskell
- Exploring folds: A powerful pattern of functional programming. ~ Zaid Ajaj #FunctionalProgramming
- The great power of Newtypes. ~ Hiromi Ishii #FunctionalProgramming #Haskell
- Some lectures on programming languages. ~ Kathleen Fisher #Programming
- Turing goes to Church (What can a computer do?). ~ Steve Poling #CompSci #FunctionalProgramming
- Not-o-matic differentiation. ~ Andrew Knapp #FunctionalProgramming #Haskell
- Examples and results from a BSc-level course on domain specific languages of mathematics ~ P. Jansson et als. #Haskell #Math
- FMS: Functional programming as a modelling language. ~ I. Dasseville, G. Janssens. #ASP
- R para Ciencia de Datos. ~ G. Grolemund, H. Wickham #Rstats #DataScience
- History of Lisp. ~ John McCarthy #Lisp
- Hedwig: a fast, type safe, declarative PureScript library for building web applications. ~ Utkarsh Kukretig#examples #PureScript
- Purely functional solutions to imperative problems (HaskellRank Ep.07). #FunctionalProgramming #Haskell
- Typed transitions, finite state machines and free categories. ~ Marcin Szamotulski #FunctionalProgramming #Haskell
- Towards Mac Lane’s comparison theorem for the (co)Kleisli construction in Coq. ~ Burak Ekici. #ITP #Coq
- Logic as a path to enlightenment (Work in progress report). ~ Wolfgang Schreiner #Logic #CompSci
- Automatic proof-checking of ordinary mathematical texts. ~ S. Frerix, P. Koepke. #ATP #ITP #Math
- IsarMathLib: a formalized mathematics library for Isabelle/ZF. ~ S. Kołodyński. #ITP #IsabelleZF #Math
- Simple high-level code for cryptographic arithmetic (with proofs, without compromises). ~ A. Erbsen, J. Philipoom, J. Gross, R. Sloan, A. Chlipala. #ITP #Coq
- CAP (Categories, Algorithms, and Programming) project. ~ S. Gutsche, S. Posur, M. Barakat, Ø. Skartsæterhagen. #CAS #CategoryTheory
- On the syntax and semantics of CAP (Categories, Algorithms, Programming) project. ~ S. Gutsche, S. Posur, Ø. Skartsæterhagen. #CAS #CategoryTheory
- Automation for proof engineering (Machine-checked proofs at scale). ~ D. Matichuk. #ITP #IsabelleHOL #PhD_Thesis
- Progress in the formalization of Matiyasevich’s theorem in the Mizar system. ~ K. Pąk #ITP #Mizar #Math
- Univalent foundations as a foundation for mathematical practice. ~ H. Crane. #Logic #Math
- A nonlinear guide to Haskell. ~ Daniel Firth #FunctionalProgramming #Haskell
- A road to Common Lisp. ~ Steve Losh #FunctionalProgramming #CommonLisp
- Fun with macros: Gathering. ~ Steve Losh #FunctionalProgramming #CommonLisp
- Fun with macros: If-let and when-let. ~ Steve Losh #FunctionalProgramming #CommonLisp
- The calculus of constructions. ~ T. Coquand, G. Huet #Logic #Math
- [[https://github.com/jaalonso/DAOconCoq/releases/download/v0.6.1/DAOconCoq.pdf][Demostración Asistida por Ordenador con Coq (6 primeros capítulos,
- An incremental simplex algorithm with unsatisfiable core generation in Isabelle/HOL. ~ Filip Marić #ITP #IsabelleHOL
- Learning proof search in proof assistants. ~ Michael Färber #AutomatedTheoremProving #MachineLearning
- A computational sketch of homology. ~ Thomas Sutton #FunctionalProgramming #Haskell #Math
- A simple methodology for computing families of algorithms. ~ D.N. Parikh et als. #Programming #CompSci
- Formalisation of cryptographic proofs in Agda. ~ A.M. Golov. #ITP #Agda
- CoqHammer: Automation for dependent type theory. ~ Ł. Czajka, C. Kaliszyk. #ITP #ATP #Coq
- CoqHammer: An automated reasoning hammer tool for Coq. ~ Łukasz Czajka #ITP #ATP #Coq
- Backprop as functor: A compositional perspective on supervised learning. ~ B. Fong, D.I. Spivak, R. Tuyéras. #Haskell #MachineLearning
- Unique solutions of contractions, CCS, and their HOL formalisation. ~ C. Tian, D. Sangiorgi. #ITP #HOL4
- Verified tail-recursive folds through dissection. ~ C. Tomé Cortiñas. #FunctionalProgramming #ITP #Agda
- Laws! ~ George Wilson #FunctionalProgramming #Haskell
- Is your research software correct? ~ Mike Croucher #Programming
- Software foundations Volume 4: QuickChick: Property-based testing in Coq. ~ L. Lampropoulos, B.C. Pierce. #ITP #Coq
- Owl: A general-purpose numerical library in OCaml. ~ L. Wang. #FunctionalProgramming #OCaml
- Comparison of two theorem provers: Isabelle/HOL and Coq. ~ A. Yushkovskiy, S. Tripakis. #ITP #IsabelleHOL #Coq
- Appetite for dysfunction. ~ Andrew McMiddlin #FunctionalProgramming #Haskell #WordPress
- Awesome emacs config files. #Emacs
- What is Data Science? ~ Lance Fortnow #DataScience
- Foundations of Data Science Boot Camp. #DataScience
- The role of the Mizar Mathematical Library for interactive proof development in Mizar. ~ G. Bancerek et als. #ITP #Mizar #Math
- Proving program correctness using the AG semantics: An example with n-queens. ~ A. Harrison-18. #LogicProgramming #ASP
- SMT-based constraint answer set solver EZSMT+ for non-tight programs. ~ D. Shen, Y. Lierler #LogicProgramming #ConstraintProgramming #ASP #SMT
- Is Julia the next big programming language? MIT thinks so, as version 1.0 lands. #Programming #Julia
- From neural networks to the Category of composable supervised learning algorithms in Scala. ~ P. Voitot #NeuralNetworks #CategoryTheory #Scala