Hello!
3 years later I have to write the bachelor thesis in Computer Science (and 1.5 years later a tinier “middle thesis” too, if I choose). Do you have any suggestions what to research/program/prove? And, maybe, how to prepare?
Thanks in advance.
Proving undecidable results is a non-trivial self-contained task in Coq that should fit your purposes.
1 Like
It looks like we have recently accumulated two more Bachelor thesis-level tasks:
-
Write implementation and proofs for some classic purely functional data structure like queues in several proof assistants (in particular, for cubical type theory based ones and Coq with HoTT) and do detailed comparison of solutions, as outlined here.
-
Prove the Hilbert basis theorem in Coq (possibly several times using different libraries), according to the challenge outlined here.
2 Likes
It’s also probably relevant to mention POPLmark reloaded https://poplmark-reloaded.github.io/
1 Like