Logo

Type Theory Forall

Type Theory much beyond inference rules

Episode image

#19 Experience Report: Learning Coq

Patrick and Supun

Apr 11th 2024   |  112 min
0:00
0:00

In today’s episode I invite two friends of mine Patrick Lafontaine and Supun Abeysinghe. We will talk about their experience learning Coq and we guide ourselves in a survey that I gave all the 83 students in the class. The class was thought by my advisor Benjamin Delaware and I was his TA.

Patrick researches compilers and have done work in particular with Rust. And Supun works more along the lines of machine learning in the context of systems.