Resumen de lecturas compartidas durante septiembre de 2019
Esta entrada es una recopilación de lecturas compartidas, durante septiembre 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.
- Resumen de lecturas compartidas durante el curso 2018-19. #GLC
- A case study in basic algebra. ~ Clemens Ballarin. #ITP #IsabelleHOL #Math
- Functor, applicative, and monad. ~ TypesLogicsCats #FunctionalProgramming #OCaml #Haskell
- Empirical mode decomposition and Hilbert-Huang transform in pure Haskell. ~ Justin Le (@mstk). #Haskell #FunctionalProgramming #Math
- TTK: The Topology ToolKit (Topological data analysis and visualization). ~ Julien Tierny (@JulienTierny) et als. #MachineLearning #DataScience #Python
- A functional reboot for deep learning. ~ Conal Elliott (@conal). #MachineLearning #DeepLearning #FunctionalProgramming #Haskell
- The simple essence of automatic differentiation. ~ Conal Elliott (@conal). #MachineLearning #DeepLearning #FunctionalProgramming #Haskell
- PyF: Haskell quasiquoter for string formatting. ~ Guillaume Bouchard. #Haskell #FunctionalProgramming
- Functional programming with overloading and higher-order polymorphism. ~ Mark P. Jones. #Haskell #FunctionalProgramming
- Announcing the optics library. ~ Adam Gundry. #Haskell #FunctionalProgramming
- Merging IO and Either into one monad. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming
- FunSeqSet: Towards a purely functional data structure for the linearisation case of dynamic trees problem. ~ J.C. Saenz-Carrasco. #Haskell #FunctionalProgramming
- Performance analysis of zippers. ~ Vı́t Šefl. #Haskell #FunctionalProgramming
- A timeline for logic, λ-calculus, and programming language theory. ~ Dana S. Scott #Logic #LambdaCalculus #Programming #ITP #CompSci
- Verifying the DPLL algorithm in Dafny. ~ C.C. Andrici, Ş. Ciobâcă. #Logic #SAT #FormalVerification #Dafny
- (Co)inductive proof systems for compositional proofs in reachability logic. ~ V. Rusu, D. Nowak. #ITP #IsabelleHOL #Coq
- Making a learning model. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming
- High performance Haskell. ~ Harendra Kumar. #Haskell #FunctionalProgramming
- Functors and lifting. ~ Alicja Raszkowska (@mamrotynka). #Haskell #FunctionalProgramming
- From LCF to Isabelle/HOL. ~ L. Paulson, T. Nipkow, M. Wenzel. #ITP #IsabelleHOL
- From type theory to setoids and back. ~ Erik Palmgren. #ITP #Agda
- Relational algebra with fancy types. ~ Philip Zucker (@SandMouth). #Haskell #FunctionalProgramming
- Why Haskell is important. ~ Mark Karpov. #Haskell #FunctionalProgramming
- Introduction to program synthesis. ~ Armando Solar-Lezama.
- Ornaments for proof reuse in Coq. ~ Talia Ringer et als. #ITP #Coq
- IMO (International Mathematical Olympiad) grand challenge. #AI #Math #ITP #LeanProver
- Formal encoding of IMO (International Mathematical Olympiad) problems. ~ Daniel Selsam. #AI #Math #ITP #LeanProver
- Automated reasoning for the working mathematician. ~ Jeremy Avigad. #ITP #ATP #Math
- Automated reasoning for the working mathematician: notes on some experiments with the use of automation in Isabelle. ~ Jeremy Avigad. #ITP #IsabelleHOL
- The great theorem prover showdown. ~ Hillel (@hillelogram). #ITP
- Formalism and proofs for esverify. ~ Christopher Schuster. #ITP #LeanProver
- Formalização de algoritmos de criptografia em um assistente de provas interativo. ~ Guilherme Gomes Felix da Silva. #MSc_Thesis #ITP #LeanProver
- Okay, maybe proofs aren’t dying after all. ~ John Horgan. #Math
- LL(1) parser generator verified in Coq. #ITP #Coq
- QED at large: A survey of engineering of formally verified software. ~ Talia Ringer et als. #ITP #FormalVerification
- The future of mathematics? ~ Kevin Buzzard. #Math #ITP #LeanProver
- Introduction aux mathématiques formalisées. ~ Patrick Massot. #Math #ITP #LeanProver
- 100 theorems for Lean. ~ Floris van Doorn. #ITP #LeanProver #Math
- A Coq formalization of boolean unification. ~ Daniel J. Dougherty. #ITP #Coq
- Porting HOL Light’s multivariate analysis library: Some lessons. ~ Lawrence C. Paulson. #ITP #IsabelleHOL
- Natürliches Schließen in Coq (Ein einführendes Tutorial). ~ Burkhardt Renz. #Logic #ITP #Coq
- Neural networks and the satisfiability problem. ~ Daniel Selsam. #PhD_Thesis #Logic #SAT #NeuralNetworks
- NeuroSAT: Learning a SAT solver from single-bit supervision. ~ Daniel Selsam. #Logic #SAT #NeuralNetworks
- Demystifying MonadBaseControl. ~ Alexis King (@lexi_lambda). #Haskell #FunctionalProgramming
- Logic, algebra, and geometry at the foundation of computer science. ~ T. Hoare, A. Mendes, J.F. Ferreira. #Math #CompSci
- Breve historia de la Inteligencia Artificial. ~ F. Sancho (@sanchocaparrini). #IA #Historia
- CompCertM: CompCert with lightweight modular verification and multi-language linking. ~ Youngju Song et als. #ITP #Coq
- Five ways to compute the cartesian product with Haskell. ~ Andrew Ribeiro (@AndrewJRibeiro). #Haskell #FunctionalProgramming
- Our journey to type checking 4 million lines of Python. ~ Jukka Lehtosalo. #Python
- IA: hombres y máquinas. ~ José Ramón Rodríguez. #IA
- Philosophy of Computer Science. ~ William J. Rapaport. #CompSci #Philosophy
- How to build Artificial Intelligence we can trust. ~ Gary Marcus (@GaryMarcus). #AI
- Running training iterations. | Monday Morning Haskell. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming
- Functor-oriented programming. ~ Russell O’Connor. #Haskell #FunctionalProgramming
- Fun with Typeclasses. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming
- Verification components for hybrid systems in Isabelle/HOL. ~ Jonathan Julian Huerta y Munive. #ITP #IsabelleHOL #Math
- Fourier series in Isabelle/HOL. ~ Lawrence C Paulson. #ITP #IsabelleHOL #Math
- The DPRM theorem in Isabelle. ~ J. Bayer et als. #ITP #IsabelleHOL #Math
- Virtualization of HOL4 in Isabelle. ~ F. Immler, J. Rädle, M. Wenzel. #ITP #IsabelleHOL #HOL4
- Formal proofs of Tarjan’s strongly connected components algorithm in Why3, Coq and Isabelle. ~ R. Chen et als. #ITP #IsabelleHOL #Coq #Why3
- A verified compositional algorithm for AI planning. ~ M. Abdulaziz, C. Gretton, M. Norrish. #ITP #HOL4 #AI
- Proving tree algorithms for succinct data structures. ~ R. Affeldt et als. #ITP #Coq
- Introduction à la programmation fonctionnelle avec Haskell. ~ Yann Esposito (@yogsototh). #Haskell #FunctionalProgramming
- Falacias lógicas explicadas gráficamente. #Lógica
- Pseudomathematics. #Math
- Data types as quotients of polynomial functors. ~ J. Avigad, M. Carneiro, S. Hudon. #ITP #LeanProver
- Primitive Floats in Coq. ~ G. Bertholon, E. Martin-Dorel, P. Roux. #ITP #Coq
- A certificate-based approach to formally verified approximations. ~ F. Bréhard, A. Mahboubi, D. Pous. #ITP #Coq #Math
- Higher-order Tarski Grothendieck as a foundation for formal proof. ~ C.E. Brown, C. Kaliszyk, K. Pak. #ITP #IsabelleHOL
- Generic authenticated data structures, formally. ~ M. Brun, D. Traytel. #ITP #IsabelleHOL
- A verified and compositional translation of LTL to deterministic Rabin automata. ~ J. Brunner, B. Seidl, S. Sickert. #ITP #IsabelleHOL
- Formalizing computability theory via partial recursive functions. ~ M. Carneiro. #ITP #LeanProver
- A smart A* search monad transformer which supports backtracking user-state. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming #AI
- Why types matter. ~ Gabrieλ Volpe (@volpegabriel87).r#/ #Haskell #FunctionalProgramming
- Announcing the refinement types library. ~ Nikita Volkov (@NikitaYVolkov). #Haskell #FunctionalProgramming
- Programming algorithms: Hash-tables. ~ Vsevolod Dyomkin. #Programming #CommonLisp #Algorithms
- Best practices for using functional programming in Python. ~ Amandine Lee (@momandine). #Python #FunctionalProgramming
- Artificial Intelligence: Foundations of computational agents, second edition. ~ David Poole, Alan Mackworth. #eBook #AI
- “Program Verification”: Has it lost its punch? ~ Nikhil Swamy. #FormalVerification
- First-order guarded coinduction in Coq. ~ L. Czajka. #ITP #Coq
- Formalizing the solution to the cap set problem. ~ S.R. Dahmen, J. Hölzl, R.Y. Lewis. #ITP #LeanProver #Math
- Nine chapters of analytic number theory in Isabelle/HOL. ~ M. Eberl. #ITP #IsabelleHOL #Math
- Nine chapters of analytic number theory in Isabelle/HOL (Slides). ~ Manuel Eberl (@pruvisto). #ITP #IsabelleHOL #Math
- A certifying extraction with time bounds from Coq to call-by-value lambda calculus. ~ Y. Forster, F. Kunze. #ITP #Coq
- Formal proof and analysis of an incremental cycle detection algorithm. ~ A. Guéneau et als. #ITP #Coq
- A formalization of forcing and the unprovability of the continuum hypothesis. ~ J.M. Han, F. van Doorn. #ITP #LeanProver
- Refinement with time (Refining the run-time of algorithms in Isabelle/HOL). ~ M.P.L. Haslbeck, P. Lammich. #ITP #IsabelleHOL
- Predicate transformer semantics for hybrid systems: Verification components for Isabelle/HOL. ~ J.J. Huerta y Munive, G. Struth. #ITP #IsabelleHOL
- Structure and interpretation of computer programs (JavaScript adaptation). ~ H. Abelson et als. #eBook #Programming #JavaScript
- Elle: Foundationally verified compilation for Ethereum. ~ M.M. Alvarez. #ITP #IsabelleHOL #Ethereum
- Generating verified LLVM from Isabelle/HOL. ~ P. Lammich. #ITP #IsabelleHOL
- Binary-compatible verification of filesystems with ACL2. ~ M.P. Mehta, W.R. Cook. #ITP #ACL2
- Verifying that a compiler preserves concurrent value-dependent information-flow security. ~ R. Sison, T. Murray. #ITP #IsabelleHOL
- Quantitative continuity and computable analysis in Coq. ~ F. Steinberg, L. Théry, H. Thies. #ITP #Coq
- Deriving proved equality tests in Coq-Elpi: Stronger induction principles for containers in Coq. ~ E. Tassi. #ITP #Coq
- Complete non-orders and fixed points. ~ A. Yamada, J. Dubut. #ITP #IsabelleHOL #Math
- Verified decision procedures for modal logics. ~ M. Wu, R. Goré. #ITP #LeanProver #Logic
- The beauty of functional languages in Deep Learning — Clojure and Haskell. ~ Jun Wu. #Clojure #Haskell #FunctionalProgramming #DeepLearning
- Making Haskell run fast: the many faces of reverse. ~ Li-yao Xia. #Haskell #FunctionalProgramming #ITP #Coq
- Declarative proof translation. ~ C. Kaliszyk, K. Pak. #ITP #IsabelleHOL #Mizar
- Formalization of the domination chain with weighted parameters. ~ D.E. Severín. #ITP #Coq #Math
- From type theory to setoids and back. ~ E. Palmgren. #ITP #Agda
- Verifying randomised social choice. ~ M. Eberl (@pruvisto). #ITP #IsabelleHOL
- A formalization of the mutilated chessboard problem in Lean. ~ Jeremy Avigad. #ITP #LeanProver
- How to build an automated theorem prover. ~ Jens Otten. #Logic #ATP #Prolog
- Building theorem provers using rewriting logic. ~ Carlos Olarte. #Logic #ATP #Maude
- Machine-oriented reasoning. ~ Cláudia Nalon. #Logic #ATP
- Build your own first-order prover. ~ Jens Otten. #Logic #ATP #Prolog
- Stronger higher-order automation: A report on the ongoing Matryoshka project. ~ Jasmin Blanchette et als. #ITP #ATP
- Clausal proofs of mutilated chessboards. ~ M.J.H. Heule, B. Kiesl, A. Biere. #ATP #PR
- Why I prefer functional programming. ~ Mario Morgenthum. #Haskell #FunctionalProgramming
- ¿Qué es un lenguaje de programación? (Parte 1). ~ Alejandro Serrano (@trupill). #Programación
- La Torre de Babel informática de los lenguajes de programación. ~ Alejandro Serrano (@trupill). #Programación
- Overview of automated reasoning and ordering-based strategies. ~ Maria Paola Bonacina. #Logic #ATP
- Computable analysis, exact real arithmetic and analytic functions in Coq. ~ F. Steinberg, H. Thies. #ITP #Coq #Math
- Not a single proof assistant for all, but proof assistants for everyone. ~ Nicolas Tabareau. #ITP #Coq
- Formalisation of probabilistic testing semantics in Coq. ~ Y. Deng, J.F. Monin. #ITP #Coq
- Mars Rover Kata in Haskell. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming
- Building lenses (Implementing basic Haskell lenses in twenty exercises). ~ Mitchell Vitez. #Haskell #FunctionalProgramming
- A cheatsheet to the time library. ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming
- Monday Morning Haskell: Adding random exploration. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming
- Functional programming in Coq. ~ Yuxin Deng. #FunctionalProgramming #ITP #Coq #LambdaCalculus
- G2Q: Haskell constraint solving. ~ W.T. Hallahan, A. Xue, R. Piskac. #Haskell #FunctionalProgramming
- Structural and semantic pattern matching analysis in Haskell. ~ P. Kalvoda, T.S. Kerckhove. #Haskell #FunctionalProgramming
- From type theory to Haskell in 10 minutes. ~ Matt Campbell. #Haskell #LambdaCalculus #TypeTheory
- What is datatype-generic programming? ~ Max Hallinan. #Haskell #FunctionalProgramming
- Seekable parsers in Haskell. ~ Frederik Ramcke. #Haskell #FunctionalProgramming
- J. Donald Monk, Mathematical logic and lectures on set theory. #eBook #Logic #Math
- The existential risk of Math errors. ~ Gwern Branwen. #Math
- Effective problem solving using SAT solvers. ~ Curtis Bright et als. #SAT_solving
- Prolog coding guidelines: Status and tool support. ~ F. Nogatz, P. Körner, S. Krings. #Prolog #LogicProgramming
- On correctness of an n queens program. ~ W. Drabent. #Prolog #LogicProgramming
- Formalization of multiway-join algorithms in Isabelle/HOL. ~ Thibault Dardinier. #ITP #IsabelleHOL
- Slick 1.0 Release – Now with a quick and easy template! ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming
- Prolog fundamentals catchup. ~ James Norman Vladimir Cash (@jamesnvc). #Prolog #LogicProgramming
- Tutorial: Creating Web applications in SWI-Prolog. ~ Anne Ogborn. #Prolog #LogicProgramming
- Functional Prolog: map, filter and reduce. ~ Paul Brown. #Prolog #LogicProgramming
- La deuda de la Inteligencia Artificial con el matemático Gödel. ~ Javier Muñoz de la Cuesta. #Lógica #IA
- A zoo of Haskell newtype wrappers. ~ Sven Heyll. #Haskell #FunctionalProgramming
- Interesting music in four lines of code. ~ Donya Quick. #Haskell #FunctionalProgramming
- An integrated development environment for the Prototype Verification System (PVS). ~ P. Masci, C.A. Muñoz. #ITP #PVS
- A formal semantics of Findel (Financial Derivatives Language) in Coq. ~ A. Arusoaie #ITP #Coq
- Formal verification of upper bounds on translative packing densities. ~ I. Mulder. #MSc_Thesis #ITP #Coq
- Probabilistic programming with Monad‑Bayes. Part 1: first steps. ~ S. Bhat, S. Carstens, M. Meschede. #Haskell #FunctionalProgramming
- Learning Haskell: A resource guide. ~ Denis Oleynikov. #Haskell #FunctionalProgramming
- The power of adjunctions. ~ Bartosz Milewski. #CategoryTheory #Programming
- Optics + Regex: Greater than the sum of their parts. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming
- Sound and reusable components for abstract interpretation. ~ S. Keidel, S. Erdweg. #Haskell #FunctionalProgramming via @Iceland_jack
- Certifying graph-manipulating C programs via localizations within data structures. ~ Shengyi Wang et als. #ITP #Coq
- Leveraging highly automated theorem proving for certification. ~ Deni Raco et als. #ITP #IsabelleHOL
- Verifying concurrent, crash-safe systems with Perennial. ~ Tej Chajed et als. #ITP #Coq
- Lazy stream programming in Prolog. ~ Paul Tarau, Jan Wielemaker, Tom Schrijvers. #Prolog #LogicProgramming
- Linear programming in Isabelle/HOL. ~ Julian Parsert and Cezary Kaliszyk. #ITP #IsabelleHOL #Math
- Linear algebra of types. ~ Philip Zucker (@SandMouth). #Haskell #FunctionalProgramming #Math
- Introducción a la Lógica. ~ F. Sancho (@sanchocaparrini). #Lógica
- Brevísima historia de la Lógica. ~ F. Sancho (@sanchocaparrini). #Lógica
- Monday morning Haskell: Tweaks, fixes, and some results. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming #AI
- Haskell on Raspberry PI 4. ~ Vaclav Svejcar. #Haskell #FunctionalProgramming #Raspberry
- Refactoring the Mars Rover Kata in Haskell. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming
- Emacs – The best Python editor? ~ Kyle Purdon (@PurdonKyle). #Emacs #Python
- A formally verified monitor for metric first-order temporal logic. ~ J. Schneider et als. #ITP #IsabelleHOL
- Adaptive online first-order monitoring. ~ J. Schneider et als #ITP #IsabelLEHOL
- Isabelle for philosophers. ~ Ben Blumson. #ITP #IsabelleHOL #Logic
- Ethereum’s recursive length prefix in ACL2. ~ Alessandro Coglio. #ITP #ACL2 #Ethereum
- Eventful GHC (debugging / profiling Haskell via the GHC eventlog). ~ Alp Mestanogullari (@alpmestan). #Haskell #FunctionalProgramming
- A formal proof of Hensel’s lemma over the p-adic integers. ~ Robert Y. Lewis. #ITP #LeanProver #Math
- Comparison of proof producing systems in SMT solvers. ~ Arjun Viswanathan. #ATP #SMT
- Lógica de primer orden: una introducción informal. F. Sancho (@sanchocaparrini). #Lógica
- Number theorist fears all published Math is wrong. ~ Mordechai Rorvig. #Math #ITP #AI
- Unit testing wai applications. ~ Mark Seemann (@ploeh). #Haskell #FunctionalProgramming
- Efficient stochastic programming in Julia. ~ M. Biel, M. Johansson. #Programming #JuliaLang
- Mikrokosmos: an educational lambda calculus interpreter. ~ M. Román. #LambdaCalculus #Haskell
- Programming algorithms: Trees. ~ Vsevolod Dyomkin. #Programming #CommonLisp #Algorithms
- Where did “differentiable programming” come from? ~ Takeo Imai (@bonotake). #DeepLearning
- Towards Coq-verified Esterel semantics and compiling. ~ G. Berry, L. Rieg. #ITP #Coq
- Quantum computing in Haskell. ~ Christopher Wright. #BSc_Thesis #Haskell #FunctionalProgramming