Resumen de lecturas compartidas durante enero de 2019
Esta entrada es una recopilación de lecturas compartidas, durante enero de 2019, 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.
- Evaluation of Isabelle with a proof of the perfect number theorem. ~ Mark IJbema. #ITP #IsabelleHOL #Math
- Univalent categories (A formalization of category theory in Cubical Agda). ~ F.H. Iversen #Msc_Thesis #ITP #Agda
- Fun with kinds and GADTS. ~ Simon Peyton Jones. #Haskell #FunctionalProgramming
- A combinatorial testing framework for intuitionistic propositional theorem provers. ~ P. Tarau. #ATP #Logic #Prolog
- Haskell Code Explorer: Web application for exploring and understanding Haskell libraries. ~ Alexey Kiryushin. #Haskell
- Haskell with only one type family. ~ Xia Li-yao. #Haskell
- 3D-Rubik’s cube simulator written in Haskell using Gloss. ~ Mark W. Ruszczycky. #Haskell
- A new way of blogging about Prolog. ~ Yehonathan Sharvit. #Prolog #Klipse #Clojure
- Formalization of concurrent revisions in Isabelle/HOL. ~ R. Overbeek. #ITP #IsabelleHOL
- A tale of servant clients. ~ C. Delafargue. #Haskell
- All about strictness analysis (part 2). ~ Sebastian Graf. #Haskell
- Lens into wrapped newtypes. ~ Jappie Klooster. #Haskell
- Parsing infinite streams with attoparsec. ~ Wander Hillen. #Haskell
- Type annotations vs partial type signatures vs visible type applications. ~ Alexey Radkov. #Haskell
- Three chapters of measure theory in Isabelle/HOL. ~ J. Hölzl, A. Heller. #ITP #IsabelleHOL #Math
- Typeable: A long journey to type-safe dynamic type representation. ~ Toan Nguyen. #Haskell
- Formalization of logic in the Isabelle proof assistant. ~ A. Schlichtkrull. #PhD_Thesis #ITP #IsabelleHOL #Logic
- Course: Logical verification (2018-2019). ~ J. Blanchette et als. #ITP #LeanProver
- Liquid Haskell tutorial. ~ Andres Löh. #Haskell #LiquidHaskell
- The QED Manifesto revisited. ~ Freek Wiedijk. #ITP
- The challenge of computer mathematics. ~ H. Barendregt, F. Wiedijk. #ITP
- Zsyntax: Automated theorem prover for a linear logic-based calculus for molecular biology. ~ Filippo Sestini. #ATP #Logic #Haskell
- Zsyntax: A formal language for molecular biology with projected applications in text mining and biological prediction. ~ G. Boniolo, M. D’Agostino, P.P. di Fiore. #ATP #Logic #Haskell
- A formal model of the Document Object Model (DOM) in Isabelle/HOL. ~ A.D. Brucker, M, Herzberg. #ITP #IsabelleHOL
- (The Cartoon Guide to) Lob’s Theorem. ~ Eliezer Yudkowsky. #Logic
- Cantor pairing. #Haskell #FunctionalProgramming #Math
- Why Haskell I: Simple data types! ~ James Bowen. #Haskell #FunctionalProgramming
- Short overview of Haskell concepts. ~ E. Pogrebnyak et als. #Haskell #FunctionalProgramming
- Machine learning leads mathematicians to unsolvable problem. ~ D. Castelvecchi. #AI #Math #MachineLearnig
- Unprovability comes to machine learning. ~ L. Reyzin #AI #Math #MachineLearnig
- Answer Set Programming (A story of default negation, definitions and informal semantics) . ~ M. Truszczynski #ASP #Logic #Programming #KR
- Hakyll + TikZ. ~ Taeer Bar-Yam. #Haskell
- Purely functional GTK+, Part 1: Hello World. ~ Oskar Wickström. #Haskell
- Validating form data via applicative functors. ~ Kostiantyn Rybnikov. #Haskell
- A reduction theorem for store buffers. ~ E. Cohen, N. Schirmer. #ITP #IsabelleHOL
- HaskellQuest: a game for teaching functional programming in Haskell. ~ R. Fu. #Teaching #Haskell
- Teaching to read Haskell. ~ Joachim Breitner. #Haskell
- Haskell for readers. ~ Joachim Breitner. #Haskell
- Types of proof system. ~ Peter Smith. #Logic #ITP
- Nombres premiers, Euclide et Coq. ~ A. Alvarez. #ITP #Coq #Math
- Column addition. ~ Kevin Buzzard. #ITP #LeanProver #Math
- The forgotten history of OOP. ~ Eric Elliott. #Programming #History
- Building the verifiable Web. ~ Kevin Buzzard. #Blockchain
- The compactness theorem and applications. ~ B. Call #Logic
- Handbook of modal logic. ~ P. Blackburn, J. van Benthem, F. Wolter. #Logic
- A comparison of functional and imperative programming techniques for mathematical software development. ~ S. Frame, J.W. Coffey. #Haskell #Cpp #Math
- HaskellRank 11: Treating lists as monads. ~ @tsoding. #Haskell #HaskellRank
- Why Haskell II: Sum types. ~ James Bowen. #Haskell #Java #Python
- Correct by construction programming in Agda. ~ Jesper Cockx. #ITP #Agda
- An algebra for higher-order terms in Isabelle/HOL. ~ Lars Hupel. #ITP #IsabelleHOL
- Haskell, Nix and Vim: Getting started. ~ Tobias Pflug. #Haskell #Nix #Vim
- The history and concept of computability. ~ Robert I. Soare. #CompSci
- Ode on a random urn (Functional pearl). ~ L. Lampropoulos, A. Spector-Zabusky, K. Foner, #Haskell
- Haskell Showroom: How to switch between multiple kubernetes clusters and namespaces. ~ Deni Bertovic #Haskell
- A touch of topological quantum computation in Haskell Pt. II: Automating drudgery. ~ Philip Zucker. #Haskell
- IMP2: Simple program verification in Isabelle/HOL. ~ Peter Lammich and Simon Wimmer. #ITP #IsabelleHOL
- Verifiable certificates for predicate subtyping. ~ F. Gilbert. #ITP #PVS
- Mechanization of separation in generic extensions. ~ E- Gunther, M. Pagano, P.S Terraf. #ITP #IsabelleHOL
- Ltac2: Tactical warfare. ~ P.M. Pédrot. #ITP #Coq
- A materialist dialectica. ~ P.M. Pédrot. #PhD_Thesis #Logic #CompSci
- Löb and möb: strange loops in Haskell. ~ David Luposchainsky. #Haskell
- Ignoring HLint (HLint now has more ways to ignore hints you don’t like). ~ Neil Mitchell. #Haskell
- A binomial urn. ~ Donnacha Oisín Kidney. #Haskell
- Dynamic graphs: A Haskell library for the dynamic connectivity problem. ~ Jasper Van der Jeugt. #Haskell
- Hindsight on Advent of Code 2018. ~ Dimitri Sabadie. #Haskell
- Lean Forward: Usable computer-checked proofs and computations for number theorists. #ITP #LeanProver #Math
- mathlib: Lean mathematical components library. #ITP #LeanProver #Math
- Using Lean with undergraduate mathematicians. ~ Kevin Buzzard. #ITP #LeanProver #Math
- Smooth manifolds and types to sets for linear algebra in Isabelle/HOL. ~ F. Immler, B. Zhan. #ITP #IsabelleHOL #Math
- Las mentes matemáticas mueven el mundo. ~ G. Abril. #Matemáticas
- A new style of mathematical proof. ~ William Farmer. #Logic #Math #ITP
- Resources for teaching with formal methods. ~ Jeremy Avigad. #Logic #Math #CompSci #ITP
- Dynamic class initialization semantics: a Jinja extension. ~ S. Mansky, E.L. Gunter. #ITP #IsabelleHOL
- Discrete Math in Coq. ~ B.C. Pierce et als. #ITP #Coq Math
- Teaching discrete mathematics to early undergraduates with “Software Foundations”. ~ M. Greenberg, J.C. Osborn. #ITP #Coq #Math
- Course: Discrete mathematics and functional programming. ~ M. Greenberg. #ITP #Coq #Math
- Formally verified big step semantics out of x86-64 binaries. ~ I. Roessle, F. Verbeek, B. Ravindran. #ITP #IsabelleHOL
- Pensando en programar. ~ Gonzalo García Braschi. #Programación
- Data-category: a collection of categories, and some categorical constructions on them. ~ Sjoerd Visscher. #Haskell
- Why Haskell III: Parametric types. ~ James Bowen. #Haskell #Java #Cpp #Python
- Farkas’ lemma and Motzkin’s transposition theorem in Isabelle/HOL. ~ R. Bottesch, M.W. Haslbeck, R. Thiemann. #ITP #IsabelleHOL #Math
- A bridge too far: E.W. Dijkstra and logic. ~ Maarten van Emden. #Logic
- Verifying imperative programs using auto2. ~ B. Zhan. #ITP #IsabelleHOL
- Proof editor for natural deduction in first-order logic (The evaluation of an educational aiding tool for students learning logic). ~ E. Björnsson et als. #Logic #Teaching #RA2018
- Tarski’s relevance logic. R. D. Maddux. #Logic
- Towards interactive Data Science in Haskell: Haskell in JupyterLab. ~ Matthias Meschede, Juan Simões. #Haskell
- An in-depth look at quickcheck-state-machine. ~ Edsko de Vries. #Haskell
- Using Jape for “Introduction to formal proof”. ~ Bernard Sufrin. #ITP #Jape #Logic
- Proving pointer programs in higher-order logic. ~ F. Mehta, T. Nipkow. #ITP #IsabelleHOL
- La révolution de l’apprentissage profond. ~ Y. Bengio. #AI
- A beginner’s guide to the ways Haskell helps us avoid errors. ~ Mitchell Vitez. #Haskell
- Solving rings in Aga. ~ Donnacha Oisín Kidney. #ITP #Agda #Math
- Experience implementing a performant category-theory library in Coq. ~ J. Gross, A. Chlipala, D.I. Spivak. #ITP #Coq #CategoryTheory
- Domain modelling with Haskell. ~ Oskar Wickström. #Haskell
- R, Python, Julia … and Polyglot. ~ Steve Miller. #Programming #Rstats #Python #Julia #Jupyter
- Crash course on notation in programming language theory. ~ Jeremy G. Siek. #CompSci
- Haskell and type theory: better together. ~ V. Bragilevsky. #Haskell #TypeTheory #LambdaCalculus
- Finding parallel functional pearls: Automatic parallel recursion scheme detection in Haskell functions via anti-unification. ~ A.D. Barwell, C. Brown, K. Hammond. #Haskell
- Applicative bidirectional programming (Mixing lenses and semantic bidirectionalization). ~ K. Matsuda, M. Wang. #Haskell
- Applicative bidirectional programming and automatic differentiation. ~ Philip Zucker. #Haskell
- Haskell trainings at Google. #Haskell
- Haskell trainings at Google: 101. #Haskell
- Haskell trainings at Google: 102. #Haskell
- El origen de los signos matemáticos. ~ Raúl Ibáñez. #Matemáticas
- Why Haskell IV: Typeclasses vs. inheritance. ~ James Bowen. #Haskell
- On the expressive power of programming languages. ~ M. Felleisen. #FunctionalProgramming
- How technology has changed what it means to think mathematically. ~ K. Devlin. #Math
- A correct compiler from Mini-ML to a big-step machine verified using natural semantics in Coq. ~ A. Zúniga, G. Bel-Enguix. #ITP #Coq
- Defining exceptions in Haskell. ~ Chris Done. #Haskell #FunctionalProgramming
- Combinatory logic: from philosophy and mathematics to computer science. ~ A. Farrugia. #Logic #Math #CompSci #FunctionalProgramming
- Primes and polynomials. ~ R.J. Lipton, K.W. Regan. #Math
- Metaprogramming lecture notes. ~ Nada Amin. #Programming #Scala #Lisp #Prolog
- Fractals and monads in Haskell (Part 1). ~ Derek Wise. #Haskell
- Fractals and monads in Haskell (Part 2). ~ Derek Wise. #Haskell