The Coq mailing list

[Yannick Zakowski <yannick.zakowski AT inria.fr>]

Hello,

The material from Xavier Leroy’s course at Collège de France is an excellent introduction I believe: https://github.com/xavierleroy/cdf-mech-sem

Best,

Yannick

Le 21 sept. 2021 à 18:27, Talia Ringer <tringer AT cs.washington.edu> a écrit :

Hi all,

Hope you're doing well! I'm trying to onboard some PhD students on a research project, and it would be really helpful to have a Coq homework for compiler verification. I'm curious if any of you have homeworks you'd be willing to share. The more the better, I'm happy to go through and see what's most helpful for the project.

I tried the FRAP homework on this when I was TAing a course a while back and found it too difficult to get used to the custom infrastructure, so then I tried to simplify it for students and I accidentally made it so easy that the core techniques weren't needed anymore. Something with minimal custom infrastructure, but still difficult enough to teach students how to write compiler correctness proofs would be good.

Thanks!

Talia

Attachment: signature.asc
Description: Message signed with OpenPGP