Resumen de lecturas compartidas durante diciembre de 2018
Esta entrada es una recopilación de lecturas compartidas, durante diciembre 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.
- |{Math, Philosophy, Programming, Writing}| = 1. ~ Attila Egri-Nagy. #Math #Philosophy #Programming
- Certifying the true error: Machine learning in Coq with verified generalization guarantees. ~ A. Bagnall, G. Stewart. #ITP #Cop #MachineLearnig
- Verification of Casper in the Coq proof assistant. ~ K. Palmskog et als. #ITP #Coq #Blockchain
- Sharing a library between proof assistants: reaching out to the HOL family. ~ F. Thiré. #ITP #Dedukti #Coq #Matita #OpenTheory #LeanProver #PVS
- Interoperability between arithmetic proofs using Dedukti. ~ F. Thiré #ITP #Dedukti #Coq #Matita #OpenTheory #LeanProver #PVS
- Logipedia: an arithmetic library that is shared between several proof systems. ~ F. Thiré. #ITP #Dedukti #Coq #Matita #OpenTheory #LeanProver #PVS
- Three Euler’s sieves and a fast prime generator (Functional pearl). ~ I. Salvo, A. Pacifico. #Haskell #FunctionalProgramming #Math
- QuickCheck (a lightweight tool for random testing of Haskell programs). ~ K. Claessen, J. Hughes. #Haskell #QuickCheck
- Tools and techniques for the verification of modular stateful code. ~ M.J. Parreira. #ITP #Why3
- Programming language foundations in Agda. ~ Philip Wadler. #ITP #Agda
- Histoire des mathématiques dans l’humanité. ~ Cedric Villani. #Math
- Programming language foundations in Agda. ~ Philip Wadler, Wen Kokke. #ITP #Agda
- Adventures in formalisation: Financial contracts, modules, and two-level type theory. ~ Danil Annenkov. #PhD_Thesis #ITP #Coq #Agda #Lean
- Introduction to Haskell. ~ Ray Toal #Haskell #FunctionalProgramming
- Course: Programming languages. ~ Ray Toal #Programming
- guanxi: An exploration of relational programming in Haskell. ~ Edward Kmett #Haskell #FunctionalProgramming
- An integrative framework for artificial intelligence education. ~ P. Langley. #Teaching #AI
- Programming with Lenses in Haskell and OCaml. #Haskell #OCaml #FunctionalProgramming
- Laziness Quiz. ~ Matt Parsons. #Haskell #FunctionalProgramming
- Pycategories: Python library implementing ideas from category theory. ~ Daniel Hones. #Python #Haskell #CategoryTheory
- Alchemical groups: Advent of code with free groups and group homomorphisms. ~ Justin Le. #Haskell #FunctionalProgramming
- Fixin’ your automata. ~ François Pottier. #OCaml #FunctionalProgramming
- Dependently typed lambda calculus in Haskell. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming
- Why Clojure? I’ll tell you why … ~ Ertuğrul Çetin. #Clojure #FunctionalProgramming
- A behind the scenes look at Map, Filter, and Reduce in Swift. ~ Boudhayan Biswas. #Swift #FunctionalProgramming
- Functional programming principles in Javascript. ~ @leandrotk_ #FunctionalProgramming #JavaScript
- Verified analysis of random binary tree structures. ~ M. Eberl, M.W. Haslbeck, T. Nipkow. #ITP #IsabelleHOL
- Automated theorem proving in a chat environment. ~ R. Zhumagambetov, M. Sterling. #ITP #Coq
- Automating the diagram method to prove correctness of program transformations. ~ D. Sabel. #Haskell #FunctionalProgramming
- A simple functional presentation and an inductive correctness proof of the Horn algorithm. ~ A. Ravara. #Logic #SAT
- Implementing a proof assistant using focusing and logic programming. ~ T. Libal. #ITP #LogicProgramming #Prolog
- Shaving with Occam’s razor: deriving minimalist theorem provers for minimal logic. ~ P. Tarau. #Logic #ATP #Prolog #LogicProgramming
- Rating of geometric automated theorem provers. ~ N. Baeta, P. Quaresma. #ATP #Geometry
- Introduction to state machine testing: part 3. ~ Andrew McMiddlin. #Haskell #FunctionalProgramming
- Lens by example: Writing traversals. ~ Chris Penner. #Haskell #FunctionalProgramming
- Haskell to Perl 6: nutshell (Learning Perl 6 from Haskell, in a nutshell). #Haskell #Perl
- Certified ACKBO. ~ A. Lochmann, C. Sternagel. #ITP #IsabelleHOL
- Towards intuitive reasoning in axiomatic geometry. ~ M. Doré, K. Broda. #ITP #ELFE #Haskell #Math
- Binding to a C++ CORBA interface in Haskell. ~ Michael Oswald. #Haskell #Cpp
- Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL. ~ J.C. Blanchette. #ITP #IsabelleHOL #Logic #ATP
- IsaFoL: Isabelle Formalization of Logic. #ITP #IsabelleHOL #Logic
- Competitive proving for fun. ~ M.P.L. Haslbeck, S. Wimmer. #ITP #IsabelleHOL
- Towards an encyclopaedia of proof systems. #Logic
- A verified compiler for a linear imperative/functional intermediate language. ~ S. Schneider. #PhD_Thesis #ITP #Coq
- Techniques behind SMT solvers. ~ T. Ehrencron. #SMT #LiquidHaskell #ATP
- 15 of the most important algorithms that helped define Mathematics, Computing, and Physics. ~ C. McFadden. #Algorithms #Math #CompSci #Physics
- 2018 in review: 10 AI failures. #AI
- Formalization of metatheory of the Quipper quantum programming language in a linear logic. ~ M.Y. Mahmoud, A.P. Felty. #ITP #Coq
- Intuitionistic dual tableaux in HOL. ~ Jeremy E. Dawson. #ITP #HOL #Logic
- United monoids. ~ A. Mokhov. #Haskell #FunctionalProgramming #Math
- Shifting the stars: Advent of code with galilean optimization. ~ Justin Le. #Haskell #FunctionalProgramming
- DIY benchmark history with Criterion and Shiny. ~ Théophane Hufschmitt. #Haskell #FunctionalProgramming
- Why not both? (Build Haskell projects with either cabal or stack). ~ Sam Halliday. #Haskell
- A webcam server in 35 lines of Haskell. #Haskell
- Computational mathematics with SageMath. ~ Paul Zimmermann et als. #eBook #SageMath
- A verified implementation of algebraic numbers in Isabelle/HOL. ~ S.J.C. Joosten, R. Thiemann, A. Yamada. #ITP #IsabelleHOL #Haskell #Math
- Applications of foundational proof certificates in theorem proving. ~ M. Roberto. #PhD_Thesis #FPC #ATP
- Tools and techniques for the verification of modular stateful code. ~ M.J. Pereira. #PhD_Thesis #ITP #Why3
- Will machine learning replace mathematicians? ~ Chris Budd. #Math #AI #ITP
- Thinking with types: Type-level programming in Haskell. ~ Sandy Maguire. #Haskell #FunctionalProgramming
- Formalizing probability concepts in a type theory. ~ F. Kachapova. #ITP #Coq #Math
- Can one design a geometry engine? On the (un)decidability of affine Euclidean geometries. ~ J.A. Makowsky. #Logic #Math #ATP
- A verified Timsort C implementation in Isabelle/HOL. ~ Y. Zhang, Y. Zhao, D. Sanan. #ITP #IsabelleHOL #Algorithms
- In praise of sequence (co-)algebra and its implementation in Haskell. ~ K. Clenaghan. #Haskell #FunctionalProgramming #Math
- The Yoda of Silicon Valley. ~ S. Roberts. #CompSci
- Why dependent Haskell is the future of software development. ~ V. Zavialov. #Haskell #FunctionalProgramming
- A Coq mechanised formal semantics for realistic SQL queries (Formally reconciling SQL and bag relational algebra). ~ V. Benzaken, É. Contejean. #ITP #Coq
- Formalizing the semantics of concurrent revisions. ~ R. Overbeek. #Msc_Thesis #ITP #IsabelleHOL
- Properties of orderings and lattices. ~ G. Struth. #ITP #IsabelleHOL #Math
- Constructive cryptography in HOL. ~ A. Lochbihler, S.R. Sefidgar. #ITP #IsabelleHOL
- Constructive and non-constructive proofs in Agda (Part 1): Logical background. ~ Danya Rogozin #ITP #Agda #Logic
- Constructive and non-constructive proofs in Agda (Part 2): Agda in a nutshell. ~ Danya Rogozin. #ITP #Agda #Logic
- Constructive and non-constructive proofs in Agda (Part 3): Playing with negation. ~ Danya Rogozin #ITP #Agda #Logic
- Prime sieves in Agda. ~ Donnacha Oisín Kidney. #ITP #Agda
- Signal processing in Haskell. ~ Rinat Stryungis. #Haskell #FunctionalProgramming
- Pure & lazy breadth-first traversals of graphs in Haskell. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming
- Purescript II: Typeclasses and Monads. ~ James Bowen. #Purescript #Haskell #FunctionalProgramming
- Purescript III: Making a Web Page with Purescript and React! ~ James Bowen. #Purescript #Haskell #FunctionalProgramming
- Purescript IV: Routing and navigation! ~ James Bowen. #Purescript #Haskell #FunctionalProgramming
- Proof pearl: A mechanized proof of GHC’s mergesort. ~ C. Sternagel. #ITP #IsabelleHOL #Haskell #Algorithms
- Classical logic in Haskell. ~ Vladimir Ciobanu. #Haskell #FunctionalProgramming #Logic
- Formally verified quantum programming. ~ R. Rand. #PhD_Thesis #ITP #Coq
- Balancing scans. ~ Donnacha Oisín Kidney. #Haskell #Agda
- Open season on hylomorphisms. ~ B. Milewski. #Haskell #FunctionalProgramming
- Metaprob: A language for probabilistic programming and metaprogramming, embedded in Clojure. #Clojure #FunctionalProgramming
- Clojure & functional programming. ~ @leandrotk_ #Clojure #FunctionalProgramming
- El yin-yang y el número áureo. ~ M.A. Morales. #Matemáticas
- Higher kinded parametricity. ~ Brian McKenna. #Haskell #FunctionalProgramming
- Verified solving and asymptotics of linear recurrences. ~ M. Eberl. #ITP #IsabelleHOL #Math #Algorithmic
- Verifying a security hypervisor model by infinite symbolic execution and invariant strengthening. ~ V. Rusu, G. Grimaud, M. Hauspie. #ITP #Coq
- Décomposer et itérer pour résoudre un problème. ~ G. Legendre, J. Salomon. #Algorithms #Math
- Solving planning problems with Fast Downward and Haskell. ~ @acid2 #Haskell #FunctionalProgramming
- Graphs are to categories as lists are to monoids. ~ Musa Al-hassy. #CategoryTheory #Agda #Haskell
- A listing of common theorems in elementary category theory. ~ Musa Al-hassy. #CategoryTheory #Agda
- Reference sheet for the Coq language. ~ Musa Al-hassy. #ITP #Coq
- Literate Agda with Org-mode. ~ Musa Al-hassy. #ITP #Agda #Emacs #OrgMode
- A verified efficient implementation of the LLL basis reduction algorithm. ~ R. Bottesch, M.W. Haslbeck, R. Thiemann. #ITP #IsabelleHOL
- Compiling to categories 3: A bit cuter. ~ Philip Zucker. #Haskell #FunctionalProgramming
- Essential logic for computer science. ~ R. Page, R. Gamboa. #Logic #ITP #ACL2
- The essence of Datalog. #Haskell #FunctionalProgramming #LogicProgramming
- Functional programming and mathematical objects. ~ J. Karczmarczuk. #Haskell #FunctionalProgramming #Math
- Proving Cantor’s theorem in Clojure using LaTTe. ~ Andrea Amantini. #ITP #LaTTe #Clojure
- How to learn Math and Physics. ~ John Carlos Baez. #Math #Physics
- Gröbner bases and Macaulay matrices in Isabelle/HOL. ~ A. Maletzky. #ITP #IsabelleHOL #Math
- A generic and executable formalization of signature-based Gröbner basis algorithms. A. Maletzky. #ITP #IsabelleHOL #Math
- Algorithms. ~ Jeff Erickson. #eBook #Algorithms
- Building blocks for theoretical computer science. ~ M.M. Fleck. #eBook #CompSci
- Open data structures (An open content textbook). P. Morin. #eBook #Algorithms #CompSci
- Towards a constructive formalization of Perfect Graph Theorems. ~ A.K. Singh, R. Natarajan. #ITP #Coq
- Port of Aleph (an Inductive Logic Programming system) to SWI-Prolog. ~ Fabrizio Riguzzi. #ILP #Prolog
- Groups of order 2019. ~ John D. Cook. #Math #Python
- Resumen de cálculos sobre el año 2019. ~ Antonio Roldán. #Matemáticas
- Nombre 2019, deux-mille-dix-neuf. ~ Gérard Villemin. #Maths
- Learning Lean by example. ~ Kevin Buzzard. #ITP #LeanTheoremProver #Math