Hi everyone,
With the academic year just getting underway, I’m opening a few 1-on-1 tutoring slots for students working with Rocq.
This may be helpful if you are:
- Taking a course that uses Rocq
- Working through Software Foundations or similar material
- Struggling with tactics, proof structure, or dependent types
- Building a project and feeling stuck
- Wanting a deeper understanding beyond “getting the script to compile”
My approach focuses on conceptual clarity and long-term independence. The goal is not to produce proofs for you, but to help you understand how to construct them yourself.
To be completely explicit:
I do not solve graded assignments, and I am strongly opposed to any form of academic dishonesty. If you are struggling, the right path is guided understanding, not outsourcing your work. My interest is in helping students build the skill and confidence to complete their own assignments properly.
A bit about me:
- 10+ years in Programming Languages and Formal Methods
- Experience in academia and industry
- ACM Best Teaching Assistant Award (Purdue, 2018)
- Host of the Type Theory Forall podcast
- Experience with Rocq, Lean, OCaml, and Haskell
I’ve taught logic, functional programming, and advanced PL courses, and I adapt sessions depending on your background, whether you are new to proof assistants or already comfortable with dependent types.
If you know students who might benefit from structured, ethical tutoring support, please feel free to share this with them.
You can reach out via DM or through:
pedro@typetheoryforall.com
Or schedule a free initial meeting directly at:
https://www.typetheoryforall.com/mentorship
Best,
Pedro