Introduction to Introductions

PUBLISHED ON NOV 19, 2019 — TUTORIALS

There are a number of topics in the field of Computer Science that I believe aren’t taught well. What I would like to do is take complex topics like Type Theory, Compiler Design, Concurrency, etc, and make digestible articles that will giver newcomers a surface level understanding and the resources to explore these fields more. There have been many times where I have wanted to research a new topic that some might consider niche, like Floyd-Hoare Logic, and the only resources I will find are blog posts that expect the reader to know way too much or to have studied it in school, or academic papers that use way too much jargon.

These articles will hopefully change that. I want to start out with the basics of Type Theory and go up the ladder to Dependent Types, Proof Assistants, and other complex topics that the average Software Engineer doesn’t need to know, but might enjoy learning if they want to continue growing in Computer Science. I want these articles to be beneficial to “wanderers”, the people searching the web trying to teach themselves these topics without formal study.

I am currently an undergraduate obtaining my Bachelor’s in Computer Science. Over the years, I have been heavily invested in programming language design and have built plenty of complex applications. My GitHub might have a lot of cool projects, but I have only recently started “formal study” at a university. As such, my word isn’t law. What I am writing is simply my interpretation of what I have learned. I will triple check any facts I present, and probably show these articles to friends so they can proofread them, but I am not a professor. I’m not a published author, and I have never written a textbook. These articles will be informal but informational. I will try my best to provide links to PDFs and related texts so readers can get a better understanding of the topics I am presenting.

Without further ado, the first article will be an Introduction to Type Theory that explains what Type Theory is, how it is applicable to programming languages, and why it is important.

Below is a roadmap of topics I would like to cover. This list may change.

  • Type Theory
  • Algebraic Data Types
  • Hindley-Milner Type System
  • Lambda Calculus and its Derivatives
  • Parametric Polymorphism and Type Operators
  • Row Polymorphism
  • Inductive Types
  • Dependent Types
  • Calculus of Constructions
  • Homotopy Type Theory
  • Cubical Type Theory