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:
- Outline - You're looking at it!
- Background - What are theorem provers and the CoIC? Why are theorem provers like Coq and Lean powerful and interesting programming languages?
- The Calculus of Inductive Constructions - Getting a first look at Coq syntax and the power of the CoIC. Introduce two running examples.
- Type Checking - How did I go about type checking the CoIC?
- Compilation - How did I go about compiling the CoIC?
- Reflections - Was the project successful? What did I accomplish? What's left to do?
Here's a link to my implementation on GitHub: Koi.