coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Compiler verification homeworks

From: Talia Ringer <tringer AT cs.washington.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Compiler verification homeworks
Date: Tue, 21 Sep 2021 11:27:10 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=Pass smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mx7.cs.washington.edu
Ironport-hdrordr: A9a23:tv8RrqDaPfpQ/XjlHemv55DYdb4zR+YMi2TDsHoBKyC9E/bo9PxG+c5x6faaslsssR0b9uxoW5PhfZq/z/9ICOAqVN/JYOCMggWVxe9ZgbfK8nnJBzD++ulB1a1pbqRyTP38ZGIK6PrH3A==
Ironport-phdr: A9a23:PnlUJB2pATaxK8jgsmDOUQQyDhhOgF0UFjAc5pdvsb9SaKPrp82kYBaHo6Q0xwKWFazgqNt8w9LMtK7hXWFSqb2gi1slNKJ2ahkelM8NlBYhCsPWQWfyLfrtcjBoVJ8aDAwt8H60K1VaF9jjbFPOvHKy8SQSGhLiPgZpO+j5AIHfg9qr2+yo/5DffgpEiTq/bLhvMBi4sALdu9UMj4B/MKgx0BzJonVJe+RS22xlIE+Ykgj/6Mmt4pNt6jxctP09+cFOV6X6ZLk4QqdDDDs6KWA15dbkugfFQACS+3YTSGQWkh5PAwjY8BH3W4r6vyXmuuZh3iSRIMv7Rq02Vzu/9admUBDnhicJOTA67W/ZlNB/gblBrx69vRFy2ZLYbJ2XOfd4Y6jTfckaRW1EXstJSSJOGIe8b4oVAOEcIehYro/9p1QQohukGAKhA//vyiVJhn/w0q01zf4hHBra0ww7Bd4Pvm7brM71NKcTV+C1w7XIzTLFb/9Mxzjy9ZXIfwknrPqRUr1+bdDfxlMzFwPZkFqQs4rlMiua2+gRt2WW4eVuW+yhhWMjtw19vCWiy9sjhIXUgo8Y11DK+Th2zYsrKtC1VEB2bNGmHZZetiyXNJZ7Tt4gTmxpvisx174IuYajcSQXx5kr2wTTZ+GIfoSW+B7uWvydLSp3iX9hYL6zmQq+/Ey6xuD/VsS4yktGoytEn9XWq3wA1ADf586aQfVn5EihwyyA1wXL5+FEP080ka3bJoYkwr8/lJcfq1jMHjTslET4lqCWbUUk+umu6+TofrXmoZmcO5VqhQ7jL6Qigs2/AeImPQgSR2WX5Oux2KH58UHkT7hGkOc6n6fDvJzHKskWora1AwpP3YYi7xa/AS2m0NMdnXQfMFJFYhOHj47mO17QOvD1Fuuwg0+2nDZl3f/GJb3hApTLLnjMjLfherB951RCxwUu0NBT/4hUBa0ZIPLvRk/xs8TVAQM+Mwyt2uroFNF91p4FVm+UGa+YMKbSsUeS6e41IumMYpUVuDfnJPQ/6f7ulyxxpVhIdq6wmJATdXqQH/J8Ikzfb2C/rM0GFDI2tw4/RaTQiVuNXCQbM2qoXqQz6ysTA5ngEo7YRoGrj6CG2mG2EoAANTMOMUyFDXq9L9bMYPwLci/HeqeJdxQPTv6+QpQh1BehqAj8jbdrM7iMksX3nZn4ksd8/O3Skx4u8joyAsiAgTjlp4Bcm3NXATQtmr92ukx8zFif1q4+jvBFR4Q72g==

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

[Coq-Club] Compiler verification homeworks, Talia Ringer, 09/21/2021
- Re: [Coq-Club] Compiler verification homeworks, Yannick Zakowski, 09/21/2021
  - Re: [Coq-Club] Compiler verification homeworks, Talia Ringer, 09/21/2021
- <Possible follow-up(s)>
- Re: [Coq-Club] Compiler verification homeworks, Yves Bertot, 09/24/2021