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