Esta entrada es una recopilación de lecturas compartidas, durante noviembre 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.
- Resumen de lecturas compartidas durante octubre de 2018. #FunctionalProgramming #Haskell #ITP #IsabelleHOL #Coq #Agda
- Formalisation and evaluation of Alan Gewirth’s proof for the principle of generic consistency in Isabelle/HOL. ~ D. Fuenmayo. #ITP #IsabelleHOL #Logic
- I/O logic in HOL. ~ A. Farjami, P. Meder, X. Parent, C. Benzmüller. #ITP #IsabelleHOL
- Åqvist’s dyadic deontic logic E in HOL. ~ C. Benzmüller, A. Farjami, X. Parent. #ITP #IsabelleHOL #Logic
- Formal proofs of Tarjan’s algorithm in Why3, Coq, and Isabelle. ~ R. Chen, C. Cohen, J.J. Levy, S. Merz, L. Thery. #ITP #Why3 #Coq #IsabelleHOL
- Automated theorem proving in intuitionistic propositional logic by deep reinforcement learning. ~ M. Kusumoto, K. Yahata, M. Sakai. #ATP #DeepLearning
- Haskell by example: The birthday bar. ~ Jan van Brügge #FunctionalProgramming #Haskell
- Haskell: journey from 144 min to 17 min. ~ Denis. #FunctionalProgramming #Haskell
- History of “Structured programming”. ~ Maarten van Emden. #Programming
- Hasktorch: a library for tensors and neural networks in Haskell. ~ Sam Stites. #FunctionalProgramming #Haskell #DeepLearning
- Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL. ~ J.C. Blanchette. #ITP #IsabelleHOL #Logic
- Mechanizing focused linear logic in Coq. ~ B. Xavier, C. Olarte, G. Reis, V. Nigam. #ITP #Coq #Logic
- Formalization of universal algebra in Agda. ~ E. Gunther, A. Gadea, M. Pagano. #ITP #Agda
- Type theory as a framework for modelling and programming. ~ C. Ionescu, P. Jansson, N. Botta. #FunctionalProgramming #TypeTheory
- Proving for Fun: proving competitions and learning material for Interactive Proof Assistants such as Isabelle. #ITP #IsabelleHOL
- Moving towards dialogue. ~ Vaibhav Sagar. #FunctionalProgramming #Haskell #Idris
- Elm III: adding effects. ~ James Bowen. #FunctionalProgramming #Elm
- Graphics programming in Elm develops Math knowledge & social cohesion. ~ J. Zhang et als. #Teaching #Math #FunctionalProgramming #Elm
- A Lisp way to type theory and formal proofs. ~ Frédéric Peschanski. #ITP #LaTTe #Clojure #FunctionalProgramming
- LaTTe: a Laboratory for Type Theory experiments (in Clojure). ~ Frederic Peschanski. #ITP #LaTTe #Clojure #FunctionalProgramming
- Proceedings of the 11 th European Lisp Symposium (April 16-17, 2018). #Lisp #FunctionalProgramming
- Carnap: a new free open-source multi-purpose multi-system logic software. ~ Graham Leach-Krouse. #Logic #Haskell #FunctionalProgramming
- Carnap: A formal logic framework that runs in the browser. ~ Graham Leach-Krouse. #Logic #Haskell #FunctionalProgramming
- Carnap.io: A formal logic framework for Haskell. ~ Graham Leach-Krouse. #Logic #Haskell #FunctionalProgramming
- Haskell by example: Utopian tree. ~ Jan van Brügge. #Haskell #FunctionalProgramming
- R and Haskell, meant for each other?. ~ Richard Careaga. #Rstats #Haskell
- HaskellR: Programming R in Haskell. #Rstats #Haskell
- Why is functional programming gaining traction? Why now? ~ Eric Normand. #FunctionalProgramming
- SAT-based explicit LTLf satisfiability checking. ~ J. Li, K.Y. Rozier, G. Pu, Y. Zhang, M.Y. Vardi. #Logic #SAT #ATP
- Hakyll Pt. 1: Setup & initial customization. ~ Robert Pearce. #Haskell #Hakyll #FunctionalProgramming
- Haskell at FINN.no. ~ Sjur Millidahl. #Haskell #FunctionalProgramming
- Signal processing in Haskell. ~ Rinat Stryungis. #Haskell #FunctionalProgramming
- Waargonaut the JSONer. ~ Sean Chalmers. #Haskell #FunctionalProgramming
- So, you want to write a DSL interpreter … H-Calc!. #Haskell #DSL #FunctionalProgramming
- On the naturalness of proofs. ~ V.J. Hellendoorn, P.T. Devanbu, M.A. Alipour. #ITP #HOL_Light #Coq
- Tarski on truth: a thumbnail sketch. ~ Peter Smith. #Logic
- Exploring a shipping puzzle. ~ Kevin Lynagh. #Clojure #Alloy #FunctionalProgramming
- Exceptionally monadic error handling (Looking at bind and squinting really hard). ~ J. Malakhovski. #Haskell #FunctionalProgramming
- A formal proof of Hensel’s lemma over the p-adic integers. ~ R.Y. Lewis. #ITP #Lean #Math
- A very simple prime sieve in Haskell. ~ Donnacha Oisín Kidney #Haskell #FunctionalProgramming
- Existential quantification. ~ Mark Karpov. #Haskell #FunctionalProgramming
- Typeclasses: Show. ~ Daniel J. Harvey #Haskell
- Problemas y algoritmos. ~ Luis Vargas. #Libro #Algoritmos #Programacion #Cpp
- Algoritmos. ~ Pier Paolo Guillen Hernandez. #Algoritmos
- Informática para las Matemáticas, Matemáticas para la Informática, Informática aplicada. ~ J. Aransay et als. #Matematicas #Informatica
- À la recherche du logiciel parfait. ~ Xavier Leroy. #ITP
- Teaching Functional Programming: two big picture approaches. ~ Ed Toro. #FunctionalProgramming
- Elm IV: navigation! ~ James Bowen. #FunctionalProgramming #Elm
- SMCDEL: A symbolic model checker for Dynamic Epistemic Logic. ~ Malvin Gattinger. #Logic #Haskell #FunctionalProgramming
- SMCDEL: an implementation of symbolic model checking for Dynamic Epistemic Logic with Binary Decision Diagrams. ~ Malvin Gattinger. #Logic #Haskell #FunctionalProgramming
- Course: Functional programming for logicians. ~ Malvin Gattinger and Jana Wagemaker. #Logic #Haskell #FunctionalProgramming
- Davis, Putnam, Logemann, Loveland (DPLL) theorem proving in Haskell. ~ Jan van Eijck. #Logic #Haskell #FunctionalProgramming #ATP
- Why IO input types are confusing. ~ Malvin Gattinger. #Haskell #FunctionalProgramming
- UCLID5: Integrating modeling, verification, synthesis, and learning. ~ S.A. Seshia, P. Subramanyam. #FormalVerification #ITP
- Simple proofs of great theorems. #Math
- Simple proofs: The irrationality of pi. #Math
- Simple proofs: The fundamental theorem of algebra. #Math
- Simple proofs: The impossibility of trisection. #Math
- Introduction to state machine testing: part 2. ~ Andrew McMiddlin #Haskell #FunctionalProgramming
- A touch of topological quantum computation in Haskell pt. I. ~ Philip Zucker. #Haskell #FunctionalProgramming
- A SAT+CAS approach to finding good matrices: new examples and counterexamples. ~ C. Bright et als. #SAT #CAS
- Programs as the language of science. ~ G. Pantelis. #CompSci
- Libro de exámenes de programación funcional con Haskell (versión del 14 de noviembre de 2018). #ProgramacionFuncional #Haskell #I1M2018
- An abstract stack based approach to verified compositional compilation to machine code. ~ P. Wilke, Y. Wang, Z. Shao. #ITP #Coq
- Simple high-level code for cryptographic arithmetic (with proofs, without compromises). ~ A. Erbsen, J. Philipoom, J. Gross, R. Sloan, A. Chlipala. #ITP #Coq
- Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report). ~ J. Breitner, A. Spector-Zabusky, Y. Li, C. Rizkallah, J. Wiegley, S. Weirich. #ITP #Coq #Haskell
- Termonad: A terminal emulator configurable in Haskell. ~ Dennis Gosnell. #Haskell #FunctionalProgramming
- Great works in programming languages. ~ Benjamin C. Pierce. #CompSci
- Ex-Hack: a Haskell example-based documentation. ~ @ninjatrappeur #Haskell
- GTK+ programming with Haskell. ~ Oskar Wickström. #Haskell
- Typed-holes and valid hole fits. ~ Matthías Páll Gissurarson. #Haskell #FunctionalProgramming
- Suggesting valid hole fits for typed-holes (experience report). ~ Matthías Páll Gissurarson. #Haskell #FunctionalProgramming
- Haskell Weekly 133: News from the Haskell community (November 15 2018). #Haskell
- Isabelle/MMT: export of Isabelle theories and import as OMDoc content. ~ Makarius Wenzel. #ITP #IsabelleHOL #MMT
- Proof-carrying plans. ~ C. Schwaab et als. #ITP #Agda IA #Planning
- On synthetic undecidability in Coq, with an application to the Entscheidungsproblem. ~ Y. Forster, D. Kirst, G. Smolka. #ITP #Coq #Logic
- Breadth-first extraction: lessons from a small exercice in algorithm certification. ~ D. Larchey-Wendling, R. Matthes. #ITP #Coq #Algorithms
- Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines. ~ Y. Forster, D. Larchey-Wendling. #ITP #Coq #Logic
- Practical Web Development with Haskell (Master the essential skills to build fast and scalable Web applications). ~ Ecky Putrady. #Haskell
- Hakyll Pt. 2: Generating a sitemap XML file. ~ Robert Pearce. #Haskell #Hakyll #FunctionalProgramming
- The emergence of first-order logic. ~ William Ewald. #Logic
- Formal verification of control systems properties with theorem proving. ~ D. Araiza-Illan, K. Eder, A. Richards. #ITP
- 2018 state of Haskell survey results. ~ Taylor Fausak. #Haskell
- Pros and cons of functional programming. ~ Iren Korkishko. #FunctionalProgramming
- The tensor product, demystified. ~ Tai-Danae Bradley. #Math
- Matroids in Isabelle/HOL. ~ Jonas Keinholz. #ITP #IsabelleHOL #Math
- Human-competitive patches in automatic program repair with Repairnator. ~ M. Monperrus et als. #Programming
- Creative Maths Challenge. #Math
- Curry-Howard-Lambek correspondence. ~ John D. Cook. #CompSci
- Keeping formal verification in bounds. ~ Donnacha Oisín Kidney. #Haskell #Agda
- Analysis and solution of a collection of algorithmic problems. ~ R.E. López. #Algorithms #Programming #Cpp
- Deriving generic class instances for datatypes in Isabelle/HOL. ~ Jonas Rädle, Lars Hupel. #ITP #IsabelleHOL
- What is elementary geometry? ~ Alfred Tarski #Math #Logic #History
- Programming with Math. ~ Bartosz Milewski. #Logic #Math #Programming #Haskell
- High-performance mathematical paradigms in Python. ~ Harshit Tyagi #Python #Math
- Formalised set theory: well-orderings and the axiom of choice. ~ Dominik Kirst. #ITP #Coq #Math
- Axiomaticl set theory in type theory. ~ Gert Smolka. #ITP #Coq #Math
- Writing a Thesis with Org Mode. #Emacs #OrgMode
- Writing a PhD thesis with Org Mode. ~ Daniel Gómez. #Emacs #OrgMode
- An Emacs Library for frictionless Blogging. ~ Daniel Gómez. #Emacs #OrgMode
- Producto de Euler y ceros. ~ Juan Arias de Reyna. #Matemáticas
- Course: Introduction to computational logic. ~ Gert Smolka. #ITP #Coq #Logic
- Function totality: Abstraction tool in programming. ~ Marko Dimjašević. #Haskell #FunctionalProgramming
- State monad comes to help sequential pattern matching. ~ Dmitrii Kovanikov. #Haskell #FunctionalProgramming
- Holophrasm: a neural automated theorem prover for higher-order logic. ~ D. Whalen. #ITP #NeuralNetworks
- Why functional programming matters. ~ J. Hughes. #FunctionalProgramming
- pLam: command line interpreter for learning and exploring pure λ-calculus. ~ Sandro Lovnički. #Haskell #LambdaCalculus
- New site for Google’s coding competitions. ~ Sue Gee. #CompetitiveProgramming
- An introduction to QuickCheck by example: Number theory and Okasaki’s red-black trees. ~ Matt Might. #Haskell #QuickCheck #FunctionalProgramming
- Category theory for programmers. (Scala edition). ~ B. Milewski, I. Tabachnik. #CategoryTheory #Haskell #Scala #FunctionalProgramming
- Haskell for Scala developers. ~ Claire Neveu. #Haskell #Scala #FunctionalProgramming
- Exploring languages with interpreters and functional programming. ~ H. Conrad Cunningham. #CompSci #Programming #FunctionalProgramming #Haskell
- (Emacs+Org-Mode) Choosing the best writing and publishing software. #Emacs #OrgMode
- Functional programming principles in Javascript. ~ @leandrotk_ #FunctionalProgramming #JavaScript
- Surgery for data types. ~ Xia Li-yao. #Haskell #FunctionalProgramming
- Directory of links on logic and foundations of mathematics. ~ Sylvain Poirier. #Logic #Math
- Getting started with Purescript! ~ James Bowen. #Purescript #Haskell #FunctionalProgramming
- Is Rust functional? ~ M. Snoyman. #Rust #FunctionalProgramming
- Haskell and Rust. ~ Chris Allen. #Haskell #Rust #FunctionalProgramming
- Computer programming as an art. ~ Donald Knuth. #Programming #CompSci
- Counting polynomial roots in Isabelle/HOL: A formal proof of the Budan-Fourier theorem. ~ W.Li, L.C. Paulson. #ITP #IsabelleHOL #Math
- Graph saturation in Isabelle/HOL. ~ S.J.C. Joosten. #ITP #IsabelleHOL
- From C to interaction trees: Specifying, verifying, and testing a networked server. ~ N. Koh et als. #ITP #Coq
- Experience report on formally verifying parts of OpenJDK’s API with KeY. ~ A. Knüppel, T. Thüm, C. Pardylla, I. Schaefer. #ATP #KeY
- Lightweight interactive proving inside an automatic program verifier. ~ S. Dailler, C. Marché, Y. Moy. #ITP #ATP
- Gentle introduction to dependent types with Idris. ~ Boro Sitnikovski. #Idris #FunctionalProgramming #ITP
- Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents. ~ M. Wenzel. #ITP #IsabelleHOL
- Some beautiful arguments using mathematical induction. ~ E.W. Dijkstra. #Math #CompSci
- Towards live programming environments for statically verified JavaScript. ~ C. Schuster. #PhD_Thesis #ITP #LeanProver #JavaScript
- Formalism and proofs for esverify. ~ C. Schuster. #IPT #LeanProver #JavaScript
- esverify: Program verification for ECMAScript/JavaScript. ~ C. Schuster. #IPT #LeanProver #JavaScript
- Traf: A proof tree viewer that works with Coq through Proof General. ~ Hideyuki Kawabata. #ITP #Coq
- Synquid: synthesizes programs from refinement types. ~ Nadia Polikarpova. #Haskell #FunctionalProgramming
- Automated synthesis of functional programs with auxiliary functions. ~ S. Eguchi, N. Kobayashi, T. Tsukada. #Haskell #FunctionalProgramming
- Auto2 prover. ~ B. Zhan. #ITP #IsabelleHOL
- A verified functional implementation of Bachmair and Ganzinger’s ordered resolution prover. ~ A. Schlichtkrull, J.C. Blanchette, D. Traytel. #ITP #IsabelleHOL
- Simplicity: High-assurance smart contracting. ~ R. Oconnor, A. Poelstra. #Haskell #Coq #ITP #FunctionalProgramming #Blockchain
- Simplicity: a blockchain programming language designed as an alternative to Bitcoin script. ~ R. Oconnor. #Haskell #Coq #ITP #FunctionalProgramming #Blockchain
- Type-driven program synthesis. ~ N. Polikarpova #Haskell #FunctionalProgramming