Resumen de lecturas compartidas durante mayo de 2019
Esta entrada es una recopilación de lecturas compartidas, durante mayo 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.
- Ordinal notations via simultaneous definitions. ~ F.N. Forsberg, C. Xu. #ITP #Agda #Logic #Math
- A formalization of forcing and the unprovability of the continuum hypothesis. ~ J.M. Han, F. van Doorn. #ITP #LeanProver #Logic #Math
- Code style and moral absolutes. ~ Brent Yorgey. #Haskell
- QKD (Quantum Key Distribution) algorithm in Isabelle: Bayesian calculation. ~ Florian Kammüller. #ITP #IsabelleHOL
- Warshall’s algorithm (survey and applications). ~ Zoltán Kása. #Algorithms
- Backprop as Functor: A compositional perspective on supervised learning. ~ B. Fong, D.I. Spivak, R. Tuyéras. #MachineLearning #CategoryTheory
- MIP: Travelling Salesman. ~ Ole Kröger. #Algorithms #JuliaLang
- MINLP: Travelling Salesman with Neighborhoods. ~ Ole Kröger. #Algorithms #JuliaLang
- Currying and partial application. ~ M. Lopes. #Haskell #Scala
- Formalization of Dubé’s degree bounds for Gröbner bases in Isabelle/HOL. ~ A. Maletzky. #ITP #IsabelleHOL #Math
- Formatting tabular data. ~ Oleg Grenrus. #Haskell
- Good symbolic differentiation requires multidimensional wobbliness. #Haskell #Math
- Formalization of Reynolds’s parametricity theorem in Coq. ~ Li-yao Xia. #ITP #Coq
- How to think about types: Insights from a personal journey. ~ F. Pfenning. #Logic #Programming #CompSci
- Good symbolic differentiation requires multidimensional wobbliness. ~ @Aearnus. #Haskell #Math
- Do we need effects to get abstraction? ~ Eric Torreborre. #Haskell
- Object oriented programming in Haskell. ~ Edsko de Vries. #Haskell
- Catamorphisms and F-Algebras. ~ Alex Avramenko. #Haskell
- Higher kinded option parsing. ~ Chris Penner. #Haskell
- The algebra of algebraic data types, part 1. ~ Chris Taylor #Haskell
- Lens as a divisibility relation: Goofin’ off with the algebra of types. ~ Philip Zucker. #Haskell
- PageRank y el surfista aleatorio. ~ F. Sancho. #Algoritmos #IA
- Making arrays mutable! ~ James Bowen. #Haskell #FunctionalProgramming
- Interaction with formal mathematical documents in Isabelle/PIDE. ~ M. Wenzel. #ITP #IsabelleHOL
- M1F, Imperial undergraduates, and Lean. ~ Kevin Buzzard. #ITP #LeanProver #Math
- Functional programming is on the rise. ~ Roman Elizarov. #FunctionalProgramming
- An interactive network graph showing the connections of programming languages based on their influences relations. ~ Ramiro Gómez. #Programming
- Exámenes de programación funcional con Haskell. Vol. 7 (Curso 2015-16). #Haskell #ProgramaciónFuncional
- Can neural networks learn symbolic rewriting? ~ B. Piotrowski, C Brown, J. Urban, C. Kaliszyk. #ATP #MachineLearning
- Tactic learning for Coq. ~ L. Blaauwbroek. #ITP #Coq #MachineLearnig
- Making set theory great again: The Naproche-SAD project. ~ S. Frerix, P. Koepke. #ITP #Math
- Experiments with connection method provers. ~ W. Bibel, J. Otten. #ATP
- An introduction to categories with Haskell and databases. ~ R. Holbrook. #CategoryTheory #Haskell #Databases
- The power of functional programming. ~ Arvind Kumar GS. #FunctionalProgramming
- Exámenes de programación funcional con Haskell. Vol. 8 (Curso 2016-17). #Haskell #ProgramaciónFuncional
- Complexity-theoretic aspects of interactive proof systems. ~ Lance Jeremy Fortnow. #PhD_Thesis #ITP #ComputationalComplexity
- Neural guidance for SAT solving. ~ S. Jaszczur, M. Łuszczyk, H. Michalewski. #ATP #SAT #MachineLearning
- Using Isabelle/UTP for the verification of sorting algorithms (A case study). ~ J.A. Bockenek, P. Lammich, Y. Nemouchi, B. Wolff. #ITP #IsabelleHOL
- Algebraic type theory and the gluing construction. ~ J. Sterling. #CompSci #TypeTheory
- The subtle art of the mathematical conjecture. ~ R. Dijkgraaf. #Math
- API constraints a’la carte in Haskell & PureScript. ~ R. Andersson. #Haskell #PureScript
- ¿Qué es un coconut? ~ Chema Cortés. #Coconut #FunctionalProgramming #Python
- Coconut – Primeros pasos. ~ Chema Cortés. #Coconut #FunctionalProgramming #Python
- Monadas con coco. ~ Chema Cortés. #Coconut #FunctionalProgramming #Python
- Functional Programming Cheat Sheet. ~ Tony Morris. #FunctionalProgramming #Haskell
- Some tricks for list manipulation. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming
- Transition to Haskell from Python: Iterator slicing. ~ Chris Martin, Julie Moronuki. #Python #Haskell
- Transition to Haskell from Python: Iteration to infinity. ~ Chris Martin, Julie Moronuki. #Python #Haskell
- Inline-JS: Seamless JavaScript/Haskell interop. ~ Shao Cheng. #Haskell #JavaScript
- Exámenes de programación funcional con Haskell. Vol. 9 (Curso 2017-18). #Haskell #ProgramaciónFuncional
- Understanding logic programming. #LogicProgramming #Python
- SMT-based constraint answer set solver EZSMT+. ~ D. Shen, Y. Lierler. #ASP #CASP
- Constructing trees from a distance matrix. ~ Guilherme Kunigami. #Algorithms
- Alan Turing Institute releases ML framework written in Julia. #MachineLearning #JuliaLang
- Exámenes de programación funcional con Haskell. Vol. 10 (Curso 2018-19). #Haskell #ProgramaciónFuncional
- Teoría de la probabilidad: Lo mínimo. ~ F. Sancho. #Matemáticas
- Making elections safe (A new proof that MAJORITY is not in AC⁰). ~ R.J. Lipton. #CompSci
- Java is confusing, Clojure is simple. ~ Yehonathan Sharvit. #Programming #Java #Clojure
- Introduction to functional programming with Python examples. ~ Radoslaw Fabisiak. #FunctionalProgramming #Python
- Timeline of mathematics. #Math
- Category theory and lambda calculus. ~ Mario Román García. #LambdaCalculus #CategoryTheory #Haskell
- Mikrokosmos: a educational λ-calculus interpreter. ~ Mario Román García. #LambdaCalculus #Haskell
- Formalization of asymptotic notations in HOL4. ~ N. Iqbal et als. #ITP #HOL4
- A denotational engineering of programming languages. ~ Andrzej Jacek Blikle. #eBook #Logic #CompSci
- Concatenative programming; the free monoid of programming languages. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming
- Interpreters with non-determinism using a free monad. ~ Casper Bach Poulsen. #Agda #Haskell
- Milestones from the pure lisp theorem prover to ACL2. ~ J Strother Moore. #ITP #ACL2
- I/O logic in HOL. ~ C- Benzmüller, A. Farjami, P. Meder, X. Parent. #ITP #IsabelleHOL #Logic
- Quicksort with Haskell! ~ James Bowen. #Haskell #FunctionalProgramming
- Integrated versus manual shrinking. ~ Edsko de Vries. #Haskell #FunctionalProgramming
- Functor-Of. ~ Vladimir Ciobanu. #Haskell #FunctionalProgramming
- Unifying semantic foundations for automated verification tools in Isabelle/UTP. ~ S. Foster et als. #ITP #IsabelleHOL
- Formalization of generic authenticated data structures in Isabelle/HOL. ~ M. Brun, D. Traytel. #ITP #IsabelleHOL
- Lightweight, efficiently sampleable enumerations in Haskell. ~ Brent Yorgey. #Haskell #FunctionalProgramming
- Implicit corecursive queues. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming
- holpy: Interactive theorem proving in Python. ~ Bohua Zhan. #ITP #Logic #Python
- GHC language extensions. ~ Andrew McMiddlin. #Haskell #FunctionalProgramming
- Laws! ~ George Wilson. #Haskell #FunctionalProgramming
- Appetite for dysfunction. ~ Andrew McMiddlin #Haskell #FunctionalProgramming
- Reflexive art. ~ Sean Chalmers. #Haskell #FunctionalProgramming
- Comma police: The design and implementation of a CSV library. ~ George Wilson. #Haskell #FunctionalProgramming
- State machine testing. ~ Andrew McMiddlin. #Haskell #FunctionalProgramming
- Contravariant functors: The other side of the coin. ~ George Wilson. #Haskell #FunctionalProgramming
- Notions of computation as monoids. ~ E. Rivas, M. Jaskelioff. #Haskell #CategoryTheory
- Graph theory in Coq: Minors, treewidth, and isomorphisms. ~ C. Doczkal, D. Pous. #ITP #Coq #Math
- Cargo culting lenses for fun & profit. ~ Sean Chalmers. #Haskell #FunctionalProgramming
- Your first Haskell app. ~ Andrew McMiddlin. #Haskell #FunctionalProgramming
- Type class: The ultimate ad-hoc. ~ George Wilson. #Haskell #FunctionalProgramming
- A note on the connections between the Foldable methods. ~ Daniel Mlot. #Haskell #FunctionalProgramming
- Data science for fundamental sciences. Atabey Kaygun #DataScience
- An app proof. R.J. Lipton. #Math
- Techniques for embedding postfix languages in Haskell. ~ Chris Okasaki. #Haskell #FunctionalProgramming
- Isabelle technology for the Archive of Formal Proofs. ~ Makarius Wenzel. #ITP #IsabelleHOL
- La Geometría se hizo Arte: las claves secretas de Escher. ~ Antonio Pérez Sanz. #Matemáticas #Escher
- A consistent foundation for Isabelle/HOL. ~ O. Kunčar, A. Popescu. #ITP #IsabelleHOL
- Mechanised assurance cases with integrated formal methods in Isabelle. ~ Y. Nemouchi et als. #ITP #IsabelleHOL
- Guiding theorem proving by recurrent neural networks. ~ B. Piotrowski, J. Urban. #ATP #NeuralNetworks
- Purely functional games (How I built a game in Haskell – pure functional style). ~ Gil Mizrahi. #Haskell #FunctionalProgramming #Game
- For cybersecurity, Computer Science must rely on strongly-typed actors. ~ C. Hewitt. #Logic #CompSci
- Running from enemies! ~ James Bowen. #Haskell #FunctionalProgramming
- A correspondence between deep/shallow embeddings and CPS/first order evaluators. ~ Matthew Chan. #Haskell #FunctionalProgramming
- Thoughts on code style. ~ Matthew Chan. #Haskell #FunctionalProgramming
- Parsing with derivatives in Haskell. ~ Timo Maarse. #Haskell #FunctionalProgramming
- Lessons in functional API development from Haskell’s servant and Http4s. ~ James Santucci. #Haskell #FunctionalProgramming
- Formalization and certification of software for smart cities. ~ E.S. Grilo, B. Lopes. #ITP #Coq
- EduBAI: An educational platform for logic-based reasoning. ~ D. Arampatzis et als. #Teaching #Logic #ASP
- Program design by calculation. ~ J.N. Oliveira. #eBook #Haskell #FunctionalProgramming
- Learning Haskell language eBook. #eBook #Haskell #FunctionalProgramming
- Competitive programming in Haskell: Scanner. ~ Brent Yorgey. #Haskell #FunctionalProgramming
- Profiling in Haskell for a 10x speedup. ~ Jake Zimmerman. #Haskell #FunctionalProgramming
- Maybe catamorphism. ~ Mark Seemann. #Haskell #FunctionalProgramming
- A formalization of forcing and the consistency of the failure of the continuum hypothesis. ~ Jesse Michael Han and Floris van Doorn. #ITP #LeanProver #Logic
- Flypitch: A formal proof of the independence of the continuum hypothesis. ~ Jesse Michael Han and Floris van Doorn. #ITP #LeanProver #Logic
- Learning to prove theorems via interacting with proof assistants. ~ K. Yang, J. Deng. #ITP #Coq #MachineLearning
- CoqGym: A learning environment for theorem proving with the Coq proof assistant. ~ K. Yang, J. Deng. #ITP #Coq #MachineLearning
- ENIGMAWatch: ProofWatch meets ENIGMA. ~ Z. Goertzel, J. Jakubův, J. Urban. #ATP #MachineLearnig
- Faking fundeps with typechecker plugins. #Haskell #FunctionalProgramming
- Applied category theory. ~ John D. Cook. #CategoryTheory
- Equality part 1: definitional equality. ~ Kevin Buzzard. #ITP #LeanProver
- Equality part 2: syntactic equality. ~ Kevin Buzzard. #ITP #LeanProver
- Codata in action, or how to connect Functional Programming and Object Oriented Programming. ~ J. Casas. #Haskell #FunctionalProgramming #CategoryTheory
- Dimensions and Haskell: Introduction. ~ D. Rogozin. #Haskell #FunctionalProgramming #MachineLearnig #Math
- Graph representations for Higher-Order Logic and theorem proving. ~ A. Paliwal et als. #ITP #ATP #MachineLearning
- Pie-hs: an implementation of Pie, the language from “The little typer”, in Haskell. ~ D.T. Christiansen. #Haskell #FunctionalProgramming
- Smarter enemies with BFS! ~ James Bowen. #Haskell #FunctionalProgramming
- A formally verified abstract account of Gödel’s incompleteness theorems. ~ A. Popescu, D. Traytel. #ITP #IsabelleHOL #Logic #Math
- Generic authenticated data structures, formally. ~ M. Brun, D. Traytel. #ITP #IsabelleHOL
- Learning to reason in large theories without imitation. ~ K. Bansal et als. #ATP #MachineLearning
- Toychain: Formally verified blockchain consensus. ~ G. Pîrlea. #ITP #Coq #Blockchain
- Programming with applicative-like expressions. ~ J. Malakhovski, S. Soloviev. #Haskell #FunctionalProgramming
- Deriving a linear-time applicative traversal of a rose tree. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming
- CYP: Checker for “morally correct” induction proofs about Haskell programs. #ITP #Haskell #FunctionalProgramming
- Naïve type theory. ~ T. Altenkirch. #Logic #Math #TypeTheory #HoTT
- La théorie de la complexité algorithmique pour calculer efficacement. ~ G. Lagarde #Algorithmes
- SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver. ~ P.W. Wang et als. #ATP #SAT #MachineLearning
- Towards finding longer proofs. ~ Z. Zombori et als. #ATP #MachineLearning
- Liquidate your assets (Reasoning about resource usage in Liquid Haskell). ~ M.A.T. Handley, N. Vazou, G. Hutton. #Haskell #LiquidHaskell
- String interpolation and overlapping instances. ~ William Yao. #Haskell #FunctionalProgramming
- Sobre cribas y matemáticas. ~ Juan Arias de Reyna. #Matemáticas