TaPL proofs

This repository contains various exercises from the book "Types and Programming Languages", 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.