justinfargnoli

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:

justinfargnoli

Understanding Coq - Part 5 - Reflections

Outline ------- Previous post: Part 4 - Compilation

Reflections

My motivation behind doing this project was to get a better understanding of how to use theorem provers. To this end, I thought that a good way to go about this would be to get a better understanding of the foundation of a theorem provers, their type system, the Calculus of Inductive Constructions (CoIC).

justinfargnoli

Understanding Coq - Part 4 - Compilation

Outline ------- Next post: Part 5 - Reflections ------- Previous post: Part 3 - Type Checking

In this blog post I'll walk through the approach I took to compile the Calculus of Inductive Constructions (CoIC).

Table of Contents

justinfargnoli

Understanding Coq - Part 3 - Type Checking

Outline ------- Next post: Part 4 - Compilation ------- Previous post: Part 2 - The Calculus of Inductive Constructions

In this blog post I'll walk through the approach I took to type check the Calculus of Inductive Constructions (CoIC).

A special feature of the CoIC is that every construct in the CoIC has a type (even types themselves). So, in each subsection, I will look at how to type-check one construct of the CoIC and what the type of each language construct is.

justinfargnoli

Understanding Coq - Part 2 - The Calculus of Inductive Constructions

Outline ------- Next post: Part 3 - Type Checking ------- Previous post: Part 1 - Background

In this blog post, I want to walk through four examples of Coq code and explain what's going on. My goal is to introduce Coq syntax and show some of the power of the Calculus of Inductive Construction. Two of these code snippets, Natural Number and Vector, will be running examples used in the next two blog posts which will focus on type checking and compilation respectively.

Table of Contents

justinfargnoli

Understanding Coq - Part 1 - Background

Outline ------- Next post: Part 2 - The Calculus of Inductive Constructions ------- Previous post: Part O - Outline

This blog post is intended to describe what theorem provers are, show some interesting use cases of them in the real world, introduce the Calculus of Inductive Constructions, and, finally, describe what this series of blog posts is about and what it is not about.

Table of Contents

justinfargnoli

Building a Search Engine from Scratch - WIP

Context

In the summer of 2020 I worked with Paul Oullette in a Research Experience for Undergraduates (REU) lead by Professor Fatemeh Nargesian. Our goal was to build a dataset search engine that would show off some of Professor Nargesian's research.

Goals

1. Build a publicly availible dataset search engine.
2. Allow users to use keyword search to find datasets.

justinfargnoli

Alive2 for SIL - GSoC Final Report

The Alive2 for SIL project aims to do translation validation of the Swift compiler's optimization passes using Alive2. For more details about the project checkout it's abstract and proposal.

Final Product

Running sil-opt with the --translation-validation flag at the beginning and end of the list of optimization passes will invoke translation validation engine on said optimization passes.

Where's the Code?