Skip to content

Instantly share code, notes, and snippets.

@justinfargnoli

justinfargnoli/Implementing the CoIC - Part 0.md

Last active May 19, 2022 23:53
Show Gist options
  • Save justinfargnoli/41ab2558183746852e8c30589a4bbbaf to your computer and use it in GitHub Desktop.
Save justinfargnoli/41ab2558183746852e8c30589a4bbbaf to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Implementing the CoIC - Part 0.md

Understanding Coq - Part 0 - Outline

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.

Outline

Here's an outline of this series of blogs posts and links to each blog post:

  1. Outline - You're looking at it!
  2. Background - What are theorem provers and the CoIC? Why are theorem provers like Coq and Lean powerful and interesting programming languages?
  3. The Calculus of Inductive Constructions - Getting a first look at Coq syntax and the power of the CoIC. Introduce two running examples.
  4. Type Checking - How did I go about type checking the CoIC?
  5. Compilation - How did I go about compiling the CoIC?
  6. Reflections - Was the project successful? What did I accomplish? What's left to do?

Accompanying Matierals

Here's a link to my implementation on GitHub: Koi.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment