Resumen de lecturas compartidas durante junio de 2019
Esta entrada es una recopilación de lecturas compartidas, durante junio 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.
- Sheldon tenía razón: el mejor número es el 73. ~ M.A. Morales. #Matemáticas
- A verified implementation of the Berlekamp–Zassenhaus factorization algorithm. ~ J. Divasón et als. #ITP #IsabelleHOL #Math
- First semester in numerical analysis with Julia. ~ G. Ökten. #eBook #JuliaLang #Math
- Why Haskell – why GitHub use Haskell for their newly released Semantic package. #Haskell #FunctionalProgramming
- Multidimensional binary search trees in Isabelle/HOL. ~ Martin Rau. #ITP #IsabelleHOL
- Towards automated reasoning in Herbrand structures. ~ L. Cohen, R. Rowe, Y. Zohar. #Logic #ATP
- Generating random structurally rich algebraic data type values. ~ A. Mista, A. Russo. #Haskell #FunctionalProgramming
- Monday Morning Haskell: Fighting Back! ~ James Bowen. #Haskell #FunctionalProgramming
- Reference of basic commands to get comfortable with OCaml. ~ Musa Al-hassy. #OCaml
- Translation from problem to code in seven steps. ~ A.D. Hilton, G.M. Lipp, S.H. Rodger. #Teaching #Programming
- Refinement with time (Refining the run-time of algorithms in Isabelle/HOL). ~ M.P.L. Haslbeck, P. Lammich. #ITP #IsabelleHOL
- Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq. ~ Enrico Tassi. #ITP #Coq
- Higher-order Tarski Grothendieck as a foundation for formal proof. ~ C. Brown, C. Kaliszyk, K. Pąk. #ITP #IsabelleHOL #Logic
- A certifying extraction with time bounds from Coq to call-by-value λ-calculus. ~ Y. Forster, F. Kunze. #ITP #Coq
- Formal proof of Tarjan’s strongly connected components algorithm in Why3, Coq, and Isabelle. ~ R. Chen et als. #ITP #Why3 #Coq #IsabelleHOL
- Formalizing computability theory via partial recursive functions. ~ M. Carneiro. #ITP #LeanProver
- Property-based testing in a screencast editor, case study 3: Integration testing. ~ Oskar Wickström. #Haskell #FunctionalProgramming
- Either catamorphism. Mark Seemann. #Haskell #FunctionalProgramming
- Haskell style guide. ~ Johan Tibell. #Haskell #FunctionalProgramming
- Solving programming puzzles without using your brain. ~ Donnacha Oisín Kidney. #Python #Math
- Formalizing the solution to the cap set problem. ~ S. Dahmen, J. Hölzl, R.Y. Lewis. #ITP #LeanProver
- Quantitative continuity and computable analysis in Coq. ~ F. Steinberg, L. Thery, H. Thies. #ITP #Coq #Math
- Hilbert meets Isabelle. (Formalisation of the DPRM theorem in Isabelle/HOL). ~ D. Aryal et als. #ITP #IsabelleHOL #Math
- A certificate-based approach to formally verified approximations. ~ F. Bréhard, A. Mahboubi, D. Pous. #ITP #Coq #Math
- Proving tree algorithms for succinct data structures. ~ R. Affeldt, J. Garrigue, X. Qi, K. Tanaka. #ITP #Coq
- Automatic refactoring for Agda. ~ K. Wibergh. #Msc_Thesis #ITP #Agda
- LP based integration of computing and science education in middle schools. ~ Y. Zhang et als. #Teaching #LogicProgramming
- Functional programming for Web and mobile (A review of the current state of the art). ~ J. Wälter. #FunctionalProgramming
- A role for dependent types in Haskell (Extended version). ~ S. Weirich et als. #Haskell #FunctionalProgramming
- Formalization of the axiom of choice and its equivalent theorems. ~ T. Sun, W. Yu. #ITP #Coq #Logic #Math
- Formalization of axiomatic set theory in Coq. #ITP #Coq #Logic #Math
- Formalization of the axiom of choice and its equivalent theorems in Coq. ~ T. Sun. #ITP #Coq #Logic #Math
- TeIL: a type-safe imperative tensor intermediate language. ~ N.A. Rink, J. Castrillon. #ITP #Coq
- Rapid prototyping formal systems in MMT: 5 case studies. ~ D. Müller, F. Rabe. #ITP #MMT #Logic
- Exploring semantic hierarchies to improve resolution theorem proving on ontologies. ~ S. Small. #ATP #Prover9
- Pure programs: Pure functions aren’t enough. ~ Ryan Newton. #Haskell #FunctionalProgramming
- Spring cleaning: Parameters and saving!. #Haskell #FunctionalProgramming
- Inductive logic programming via differentiable deep neural logic networks. ~ A. Payani, F. Fekri. #ILP #NeuralNetworks #MachineLearning
- Relay: A high-level IR for Deep Learning. ~ J. Roesch et als. #FunctionalProgramming #MachineLearning
- The inverse of a bijection. ~ Kevin Buzzard. #ITP #LeanProver #Math
- A practical introduction to freer monads (Eff). #Haskell #FunctionalProgramming
- Functional programming in OCaml. ~ Michael R. Clarkson. #eBook #FunctionalProgramming #OCaml
- A verified ODE solver and Smale’s 14th problem. ~ F. Immler. #PhD_Thesis #ITP #IsabelleHOL #Math
- An Isabelle/HOL formalisation of Green’s theorem. ~ M. Abdulaziz, L.C. Paulson. #ITP #IsabelleHOL #Math
- Formally verified algorithms for upper-bounding state space diameters. ~ M. Abdulaziz, M. Norrish, C. Gretton. #ITP #HOL4
- A formally verified validator for classical planning problems and solutions. ~ M. Abdulaziz, P. Lammich. #ITP #IsabelleHOL
- A tutorial introduction to structured Isar proofs. ~ T. Nipkow. #ITP #IsabelleHOL
- Permutations and permutation groups in Common Lisp. ~ Robert Smith. #CommonLisp #Math
- Cultures of programming (Understanding the history of programming through controversies and technical artifacts). ~ T. Petricek, #Programming
- Truth and justification in knowledge representation. ~ A. Rodin, S. Kovalyov. #KR #HoTT
- Binary heaps for IMP2 in Isabelle/HOL. ~ S. Griebel. #ITP #IsabelleHOL
- Exercises on generalizing the induction hypothesis. ~ James Wilcox. #ITP #Coq
- Monoid. ~ Chris Martin, Julie Moronuki. #Haskell #FunctionalProgramming
- Empty and unit types. ~ Ashley Yakeley. #Haskell #FunctionalProgramming #TypeTheory
- Free monads of free monads. ~ Li-yao Xia. #Haskell #FunctionalProgramming
- hsp: Haskell command line text stream processor. #Haskell #FunctionalProgramming
- Proofs are not programs. ~ Kevin Buzzard. #ITP #LeanProver #Math
- CrystalBall: SAT solving, data gathering, and machine learning. ~ Mate Soos. #SAT #MachineLearning
- Teaching the art of functional programming using automated grading (Experience report). ~ A. Hameer, B. Pientka. #Teaching #FunctionalProgramming #OCaml
- Learn-OCaml: A Web application for learning OCaml. #Teaching #FunctionalProgramming #OCaml
- Selective applicative functors. ~ Andrey Mokhov. [Slides] #Haskell #FunctionalProgramming
- Composing monads for a musical performance. ~ N. Rossiter, M. Heather. #Music #CategoryTheory #Haskell
- Higher-order type-level programming in Haskell. ~ C. Kiss et als. #Haskell #FunctionalProgramming
- Developing an intuition for reduce in JavaScript through Haskell: Monoids. ~ @codefornerds #JavaScript #Haskell #FunctionalProgramming
- Parsing typed eDSL. ~ George Agapov. #Haskell #FunctionalProgramming
- Haskell quick syntax reference. ~ S.L. Nita, M. Mihailescu. #eBook #Haskell #FunctionalProgramming
- Effective problem solving using SAT solvers. ~ C. Bright et als. #ATP #SAT
- The Isabelle cookbook (A gentle tutorial for programming Isabelle/ML). ~ C. Urban et als. #ITP #IsabelleHOL
- Gröbner bases and Macaulay matrices in Isabelle/HOL. ~ A. Maletzky. #ITP #IsabelleHOL #Math
- Formalization of Dubé’s degree bounds for Gröbner bases in Isabelle/HOL. ~ A. Maletzky. #ITP #IsabelleHOL #Math
- Gröbner bases, Macaulay matrices and Dubé’s degree bounds in Isabelle/HOL. ~ A. Maletzky. #ITP #IsabelleHOL #Math
- Hilbert’s Nullstellensatz in Isabelle/HOL. ~ A. Maletzky. #ITP #IsabelleHOL
- Formal verification of boolean unification algorithms with Coq. ~ D. Richardson et als. #ITP #Coq
- Introduction to homotopy type theory. ~ E. Rijke. #HoTT #Logic #math #ITP #Agda
- Monte Carlo tableau proof search. ~ M. Färber, C. Kaliszyk, J. Urban. #ATP #Logic #MachineLearning
- Authenticated data structures, generically. #Haskell #FunctionalProgramming
- Loading games and changing colors! ~ James Bowen #Haskell #FunctionalProgramming
- Patterns of functional programming: functional core – imperative shell. ~ J. Casas. #Haskell #FunctionalProgramming
- A taste of functional programming in Kotlin. ~ Baseer Al-Obaidy. #FunctionalProgramming #Kotlin
- The Functor Combinatorpedia. ~ Justin Le. #Haskell #FunctionalProgramming
- The functional programming toolkit. ~ Scott Wlaschin. #FunctionalProgramming
- The power of composition (for beginners in FP). ~ Scott Wlaschin. #FunctionalProgramming #Fsharp
- Functional design patterns. ~ Scott Wlaschin. #FunctionalProgramming #Fsharp
- Implementing recursion with the Y combinator in any language. ~ Michele Riva. #LambdaCalculus #JavaScript #Haskell #Java #Racket #Python #C
- UserLAnd: The easiest way to run a Linux distribution or application on Android. #Linux #Android
- An interactive way to C. ~ Musa Al-hassy. #Programming #C #Emacs #Org_mode
- Presenting the Eshell. ~ Howard Abrams. #Emacs
- String interpolation and overlapping instances. ~ William Yao. #Haskell #FunctionalProgramming
- Count-Min sketch in Haskell. ~ Victor Adossi. #Haskell #FunctionalProgramming
- An opinionated beginner’s guide to Haskell in mid 2019. ~ Varun Gandhi. #Haskell #FunctionalProgramming
- foldr under the hood. ~ Neil Mitchell. #Haskell #FunctionalProgramming
- Transition to Haskell from Python: Zipping. ~ Chris Martin, Julie Moronuki. #Python #Haskell
- Theorema-HOL: Classical Higher-Order Logic in Theorema. ~ A. Maletzky. #ITP #TheoremaHOL
- An introduction to Copilot. ~ F. Dedden et als. #Haskell #FunctionalProgramming
- Neural theorem provers do not learn rules without exploration. ~ M. de Jong, F. Sha. #ATP #MachineLearning
- Linear inequalities in Isabelle/HOL. ~ R. Bottesch, A. Reynaud, R. Thiemann. #ITP #IsabelleHOL #Math
- Verifying fold using Monoids in Coq. ~ Dalton Lundy. #ITP #Coq #FunctionalProgramming
- Lessons learned while writing a Haskell application. ~ G. Volpe. #Haskell #FunctionalProgramming
- An efficient implementation of Galois fields. ~ Stephen Diehl. #Haskell #FunctionalProgramming #Math
- A brief guide to a few algebraic structures. ~ Julie Moronuki. #Math #Haskell #FunctionalProgramming
- Why I (as of June 22 2019) think Haskell is the best general purpose language (as of June 22 2019). ~ Philip Zucker. #Haskell #FunctionalProgramming
- What is a programmable programming language? ~ A. Sanchez. #Programming #Lisp
- Introducción a la programación en Julia. ~ Mauricio M. Tejada. #JuliaLang
- A mathematical proof isn’t just an intellectual exercise. ~ D. Holland. #Math
- En busca de una nueva definición para la inteligencia de las máquinas. ~ Luis Ignacio Hojas Hojas. #IA
- Differential game logic in Isabelle/HOL. ~ André Platzer. #ITP #IsabelleHOL
- Taking a shortcut! ~ James Bowen. #Haskell #FunctionalProgramming
- Python and Emacs Pt. 1. ~ Jonathan Bennett. #Emacs #Python
- LiFtEr: Language to encode induction heuristics for Isabelle/HOL. ~ Y. Nagashima. #ITP #IsabelleHOL
- A framework for specifying and formally verifying application security policies. ~ C. Shao. #Msc_Thesis #ITP #Coq
- On roots of polynomials over F(X)/<p>. ~ C. Schwarzweller. #ITP #Mizar #Math
- AI safety as a PL problem. ~ Swarat Chaudhuri. #AI #FormalVerification #MachineLearning
- Transition to Haskell from Python: Data classes. ~ Chris Martin , Julie Moronuki. #Python #Haskell
- Implement with types, not your brain! #Haskell #FunctionalProgramming
- Evaluación de implementaciones alternativas de colas concurrentes en Haskell. ~ T.A: González. #Haskell
- Call-by-need is clairvoyant call-by-value. ~ J. Hackett, G. Hutton. #FunctionalProgramming
- Elisp reference sheet (Quick reference to the core language of Emacs). ~ Musa Al-hassy. #Programminf #Lisp #Elisp #Emacs
- Gerwin’s style guide for Isabelle/HOL. Part 1: Good proofs. ~ Gerwin Klein. #ITP #IsabelleHOL
- Gerwin’s style guide for Isabelle/HOL. Part 2: Good style. ~ Gerwin Klein. #ITP #IsabelleHOL
- Course: Advanced topics in software verification. ~ Gerwin Klein, June Andronick, Christine Rizkallah, Miki Tanaka. #ITP #IsabelleHOL
- CPP considered harmful. ~ Mathieu Boespflug. #Haskell #FunctionalProgramming
- The tragedy of the Common Lisp: Why large languages explode. ~ Mark Miller. #Programming
- Toward artificial intelligence that learns to write code. ~ K. Martineau. #Programming #AI #DeepLearning
- Learning to infer program sketches. ~ M. Nye et als. #Programming #AI #DeepLearning
- How to specify it! (A guide to writing properties of pure functions). ~ John Hughes. #Haskell #FunctionalProgramming
- Gen: A general-purpose probabilistic programming system with programmable inference. ~ M.F. Cusumano-Towner et als. #AI #JuliaLang
- Priority search trees im Isabelle/HOL. ~ P. Lammich, T. Nipkow. #ITP #IsabelleHOL
- Purely functional, simple, and efficient implementation of Prim and Dijkstra in Isabelle/HOL. ~ P. Lammich, T. Nipkow. #ITP #IsabelleHOL
- Complete non-orders and fixed points in Isabelle/HOL. ~ A. Yamada, and J. Dubut. #ITP #IsabelleHOL
- Mathematical method and proof. ~ Jeremy Avigad. #ITP #IsabelleHOL #Logic #Math
- A Julia set generator. ~ Chris Martin, Julie Moronuki. #Haskell #FunctionalProgramming