Hello! This is a series of blog posts that I'm writing for an independent study I did during the Spring 2022 semester with Professors Sreepathi Pai and Chen Ding at the University of Rochester.
The purpose of my independent study was to get a better understanding of how Coq and other theorem provers worked by learning about the type system that powers them, the Calculus of Inductive Constructions (CoIC). As a part of the independent study I implemented a type checker and compiler for the CoIC, gave a talk to the systems group within the Computer Science department about the CoIC, and wrote this series of blog posts.
Here's an outline of this series of blogs posts and links to each blog post: