# TaPL proofs

This repository contains various exercises from the book ["Types and Programming Languages"](https://www.cis.upenn.edu/~bcpierce/tapl/), solved in Rocq.

I'm pretty new to the entire Rocq ordeal while solving this, so I would not encourage using this as a reference solution.