Resumen de lecturas compartidas durante abril de 2019

Esta entrada es una recopilación de lecturas compartidas, durante abril 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.

• Students’ Proof Assistant (SPA). ~ Anders Schlichtkrull, Jørgen Villadsen, Andreas Halkjær From. #Logic #IsabelleHOL
• Towards ranking geometric automated theorem provers. ~ N. Baeta, P. Quaresma. #ATP #Math
• Learning how to prove: From the Coq proof assistant to textbook style. ~ S. Böhne, C. Kreitz. #Teaching #Logic #ITP #Coq
• Building a bigger World. James Bowen. #Haskell #FunctionalProgramming
• A history of the theory of types. ~ J. Collins. #Logic #History
• The pillars of functional programming (part 1). N. Mozgovoy. #FunctionalProgramming
• Dynamic typing in Haskell. ~ Chris Done. #Haskell #FunctionalProgramming
• Jupyter kernel for Coq. ~ Eugene Loy. #ITP #Coq #Jupyter
• IFL2: Chapters on propositional natural deduction, again. ~ Peter Smith. #Logic
• Theorem and algorithm checking for courses on logic and formal methods. ~ W. Schreiner. #Logic #RISCAL
• Proof complexity. ~ Jan Krajicek. #Book #Logic
• Verified code generation from Isabelle/HOL. ~ L. Hupel. #PhD_Thesis #ITP #IsabelleHOL
• Proving soundness of extensional normal-form bisimilarities. ~ P. Polesiuk, S Lenglet, D. Biernacki. #ITP #Coq
• Hammering Mizar by learning clause guidance. ~ J. Jakubův, J. Urban. #ITP #Mizar #MachineLearnig
• The Open Problem Garden: a collection of unsolved problems in mathematics. #Math
• Idempotent applicatives, parametricity, and a puzzle. ~ D. Mlot. #Haskell #FunctionalProgramming
• Proving addition is commutative in Haskell using singletons. ~ Philip Zucker. #Haskell #FunctionalProgramming
• Data Science in Haskell: An example using temperature data from Thailand and Myanmar. ~ Dominic Steinitz. #Haskell #FunctionalProgramming #DataScience
• A tiny compiler for a typed higher order language. ~ Danny Gratzer. #Haskell #FunctionalProgramming
• Imperative Haskell. ~ Vaibhav Sagar. #Haskell #FunctionalProgramming
• Programación funcional para mortales con Scalaz. ~ S. Halliday, O. Vargas. #Scalaz #ProgramaciónFuncional
• Analysing mathematical reasoning abilities of neural models. ~ D. Saxton, E. Grefenstette, F. Hill, P. Kohli. #MachineLearnig
• Libro de soluciones de problemas de programación funcional con Haskell propuestos en Exercitum (versión del 6-abr-19). #Haskell #Exercitium
• Isomorphism and embedding. ~ Marko Dimjašević. #ITP #Agda #Math
• Six easy ways to run your Jupyter Notebook in the cloud. #Jupyter
• Fun with functors. ~ Marco Perone. #FunctionalProgramming #CategoryTheory
• Foundations of functional programming. ~ L.C Paulson. #FunctionalProgramming #LambdaCalculus
• Set theory for Computer Science. ~ G. Winskel. #Logic #Math
• Foundations of Data Science. ~ D. Wischik. #DataScience
• Type systems. ~ N. Krishnaswami. #TypeTheory
• Web engines in Haskell. ~ Chris Done. #Haskell #FunctionalProgramming
• Vado: A demo web browser engine written in Haskell. ~ Chris Done. #Haskell #FunctionalProgramming
• The nature of infinity and beyond (An introduction to Georg Cantor and his transfinite paradise). ~ Jørgen Veisdal. #Logic #Math
• The Riemann Hypothesis, explained. ~ Jørgen Veisdal. #Math
• Abstract completion, formalized. ~ N. Hirokawa, A. Middeldorp, C. Sternagel, S. Winkler. #ITP #IsabelleHOL
• On initial categories with families (Formalization of unityped and simply typed CwFs in Agda). ~ K. Brilakis. #Msc_Thesis #ITP #Agda
• Constructing inductive-inductive types in cubical type theory. ~ J. Hugunin. #ITP #Agda #Coq
• What making a cup of tea taught me about functional programming. Sam Fare. #FunctionalProgramming
• Programming prospect theory in Prolog. ~ I. Kenryo. #Prolog #LogicProgramming
• Generating more difficult mazes! ~ James Bowen. #Haskell #FunctionalProgramming
• Julia Data Science Tutorial: Working with DataFrames and CSV. #JuliaLang #DataScience
• A general theory of syntax with bindings in Isabelle/HOL. ~ L. Gheri. #ITP #IsabelleHOL
• HOList: An environment for machine learning of higher-order theorem proving (extended version). ~ K. Bansal et als. #ITP #HOL_Light #MachineLearnig
• A gentle introduction to symbolic execution. ~ B. Schroeder, J. Burget. #Haskell #SMT
• Logic, explainability and the future of understanding. ~ S. Wolfram. #Logic
• Applicative regular expressions using the free alternative. ~ Justin Le. #Haskell #FunctionalProgramming
• To kata haskellen evangelion (Learn Haskell the easy way). ~ Cosmia Fu. #eBook #Haskell #FunctionalProgramming
• Short proof of Menger’s Theorem in Coq (Proof Pearl). ~ C. Doczkal. #ITP #Coq #Math
• Hammering Mizar by learning clause guidance. ~ J. Jakubův, J. Urban. #ATP #Mizar #MachineLearnig
• Quantitative continuity and computable analysis in Coq. ~ F. Steinberg, L. Thery, H. Thies. #ITP #Coq #Math
• The Rubik’s cube group. ~ Jared Corduan. #Haskell #FunctionalProgramming #Math
• Become a better haskeller by learning about inductive types. ~ Marko Dimjašević. #Haskell #FunctionalProgramming
• A primer on scientific programming with Python. ~ Hans Petter Langtangen. #eBook #Python #Programming
• Introduction to Python for computational science and engineering (A beginner’s guide). ~ Hans Fangohr. #eBook #Python #Programming
• Lisp used to generate rhythms for a contemporary string trio. #Lisp #Programming #Music
• Learning Haskell through Google Code Jam. ~ Ashwin Narayan. #Haskell #FunctionalProgramming
• New in CodeWorld: Share a folder as a gallery. ~ Chris Smith. #CodeWorld #Haskell
• A cheatsheet to regexes in Haskell. ~ William Yao. #Haskell
• Learning heuristics for automated reasoning through deep reinforcement learning. ~ G. Lederman et als. #ATP #DeepLearning
• Executable formal specification of programming languages with reusable components. ~ L.T. van Binsbergen. #PhD_Thesis #Haskell #FunctionalProgramming
• A new foundational crisis in mathematics, is it really happening? ~ M. Džamonja. #Logic #Math #HoTT
• Declaring victory! (and starting again!) ~ James Bowen. #Haskell #FunctionalProgramming
• A graphical introduction to dynamic programming. ~ Avik Das. #Algorithms #Programming #Python
• Modern SAT solvers: fast, neat and underused (part 3 of N). ~ M. Hořeňovský. #Logic #SAT
• Basic Cheat Sheet for Python (PDF, Markdown and Jupyter Notebook). ~ Carlos Montecinos Geisse. #Python #Programming
• Evolution of programming languages. #Programming
• Cubical Agda and probability monads. ~ Donnacha Oisín Kidney. #Agda
• Can you avoid functional programming as a policy? ~ Eric Elliott. #FunctionalProgramming
• Every day recursion schemes. ~ David Smith. #Haskell #FunctionalProgramming
• Towards evolutionary theorem proving for Isabelle/HOL. ~ Yutaka Nagashima. #ITP #IsabelleHOL #MachineLearning
• Eisbach: A proof method language for Isabelle. ~ D. Matichuk, T. Murray, M. Wenzel. #ITP #IsabelleHOL
• Automation for proof engineering (Machine-checked proofs at scale). ~ D. Matichuk. #PhD_Thesis #ITP #IsabelleHOL
• Other classical reasoning methods in Isabelle: From tactics and tacticals to automated reasoning in Isabelle. ~ Stephan Scheele. #ITP #IsabelleHOL
• Microsoft debuts Bosque – a new programming language with no loops, inspired by TypeScript. ~ T. Clarbun. #FunctionalProgramming
• Regularized programming with the BOSQUE language (Moving beyond structured programming). ~ Mark Marron. #FunctionalProgramming
• Towards machine learning induction. ~ Yutaka Nagashima. #ITP #IsabelleHOL #MachineLearning
• Course: Interactive theorem proving using Isabelle/HOL. ~ Christian Sternagel. #ITP #IsabelleHOL
• Automated proof synthesis for propositional logic with deep neural networks. ~ Taro Sekiyama, Kohei Suenaga. #ATP #MachineLearning
• PSL: proof strategy language for Isabelle/HOL. ~ Yutaka Nagashima. #ITP #IsabelleHOL
• A certificate-based approach to formally verified approximations. ~ F. Bréhard, A. Mahboubi, D. Pous. #ITP #Coq #Math
• Did Functional Programming get it wrong? (Why do monads feel so clumsy?). ~ reinman. #FunctionalProgramming
• From theory to systems: a grounded approach to programming language education. ~ W. Crichton. #Teaching #Programming
• Soundness and completeness: with precision. ~ Bertrand Meyer. #CompSci
• Just do it: Simple monadic equational reasoning. ~ Jeremy Gibbons and Ralf Hinze. #Haskell #FunctionalProgramming
• Microsoft’s new programming language ‘Bosque’ keeps your code simple. ~ Manisha Priyadarshini #Programming #Bosque
• A working mathematician’s guide to parsing. ~ Jeremy Kun | Math ∩ Programming #Programming #LaTeX
• Serializing mazes! ~ James Bowen. #Haskell #FunctionalProgramming
• P=NP proofs. ~ R.J. Lipton. #CompSci #Math
• Rewriting functions with fold and reduce. ~ Max Strübing. #Programming #Haskell #JavaScript
• The theorem prover museum (Conserving the system heritage of automated reasoning). ~ M. Kohlhase. #ATP #ITP
• Competitive programming in Haskell: Basic setup. ~ Brent Yorgey. #Haskell
• Declarative programming with Prolog. ~ Aaron Kraus. #Prolog #LogicProgramming
• Why check a proof? ~ R.J. Lipton. #CompSci
• Formalization of logical calculi in Isabelle/HOL. ~ M. Fleury. #PhD_Thesis #ITP #IsabelleHOL #Logic
• A verified SAT solver framework including optimization and partial valuations. ~ M. Fleury, C. Weidenbach, D. Zimmer. #ITP #IsabelleHOL #Logic
• Continuous improvement with hlint code smells. ~ Ben Weitzman. #Haskell
• Demystifying folds with GHCi. ~ Ayman Nadeem. #Haskell
• Thinking in types. ~ Pat Brisbin. #Haskell
• Transitioning to Haskell from other languages. ~ @typeclasses #Haskell #Java #JavaScript #Python
• Python iterators. ~ @typeclasses #Python #Haskell
• Python function decorators. #Python #Haskell
• Intro to Higher Kinded Types in Haskell. ~ Patxi Bocos. #Haskell
• Exercises for understanding Lenses. ~ William Yao. #Haskell
• Compile driven development in action: refactoring to arrays! ~ James Bowen. #Haskell
• Logic for exact real arithmetic. ~ H. Schwichtenberg, F. Wiesnet. #Logic #Mayh #MinLog #Haskell