Evgenii Kosogorov (Sep 24 2023 at 19:04): Evgenii Kosogorov (Sep 24 2023 at 19:04):I'm interested in proof assistants(mostly Coq), logic and functional programming. I'm looking for a project that would be suitable for a bachelor thesis. Do you have any suggestions?
Huỳnh Trần Khanh (Sep 24 2023 at 23:47):Yes. As an undergraduate myself, I can suggest a topic that fits your skill level.
You can formalize several algorithms to generate a random regular bracket string of length n, where every string has an equal chance of being generated. Here are some suggestions:
Except rejection sampling, all the other algorithms can be formalized with monads.
Yannick Forster (Sep 25 2023 at 09:18):Evgenii Kosogorov said:
I'm interested in proof assistants(mostly Coq), logic and functional programming. I'm looking for a project that would be suitable for a bachelor thesis. Do you have any suggestions?
It's hard to generate suggestions without more information :) Relevant questions are: What is your background in logic and Coq? Did you take classes covering first-order logic, higher-order logic, model theory, set theory, type theory, etc? None of these things are mandatory, but it helps to come up with ideas. Then: Do you know about the differences between intuitionistic and classical logic? What material did you use to learn Coq? Do you know about computability theory? Automata theory and formal languages? Complexity theory? Computational methods for logic, e.g. SAT or SMT solvers? And then: What are the requirements for a Bachelor's thesis at your university? Will you need to write a thesis in prose, or can it be a project just using Coq? Feel free to answer them in a private message if you feel more comfortable that way
Huỳnh Trần Khanh (Sep 25 2023 at 09:35):in vietnam, a bachelor thesis isn't too complicated. you can just make a web application. you don't need to present anything novel. but you do need tens of pages of prose, not just code. all the above stuff is probably too much for a bachelor thesis. I'm in my 3rd year and the hardest thing I had to learn was writing a parser
Karl Palmskog (Sep 25 2023 at 09:38):here is a bachelor-level idea for an existing open source project in Coq-community I could help out with:
I maintain a verified implementation in Coq of a distributed causally consistent key-value store (https://github.com/coq-community/chapar). While the code can be extracted to OCaml and compiled, it can't be run due to some low-level bugs that haven't been addressed, and there are several serious issues even so, e.g., the verification assumes removal of duplicates while the OCaml implementation does not remove duplicates due to using raw UDP (https://github.com/coq-community/chapar/issues). An interesting task is make the OCaml code run again and try to figure out the best way of fixing the most serious issues such as message deduplication, at both the Coq and OCaml levels. See original paper and paper where flaws were found: http://adam.chlipala.net/papers/ChaparPOPL16/ https://unsat.cs.washington.edu/papers/fonseca-dsbugs.pdf
Evgenii Kosogorov (Sep 27 2023 at 11:26):Yannick Forster said:
Evgenii Kosogorov said:
I'm interested in proof assistants(mostly Coq), logic and functional programming. I'm looking for a project that would be suitable for a bachelor thesis. Do you have any suggestions?
It's hard to generate suggestions without more information :) Relevant questions are: What is your background in logic and Coq? Did you take classes covering first-order logic, higher-order logic, model theory, set theory, type theory, etc? None of these things are mandatory, but it helps to come up with ideas. Then: Do you know about the differences between intuitionistic and classical logic? What material did you use to learn Coq? Do you know about computability theory? Automata theory and formal languages? Complexity theory? Computational methods for logic, e.g. SAT or SMT solvers? And then: What are the requirements for a Bachelor's thesis at your university? Will you need to write a thesis in prose, or can it be a project just using Coq? Feel free to answer them in a private message if you feel more comfortable that way
Thank you! I'll try to answer your questions:
The thesis can be just a project.
I studied logic, type theory, formal semantics of programming languages(just a bit). Studied Coq with Software Foundations. A part of my current job is to prove properties of smart-contracts using Coq. Took a few classes about SAT and SMT solvers. Familiar with automate theory, computability theory and complexity theory.
Huỳnh Trần Khanh (Sep 27 2023 at 12:17):looks like my suggestion is perfect for your background
Huỳnh Trần Khanh (Sep 27 2023 at 12:18):though if you're good at working on unfamiliar code Karl's suggestion is good too
Huỳnh Trần Khanh (Sep 27 2023 at 12:20):if you're allowed to open source your work your thesis would make quite a contribution to the world
Evgenii Kosogorov (Sep 27 2023 at 12:28):I'd like to also add that I took courses about distributed systems and parallel programming.
The criteria for bachelor thesis in my university is pretty vague. I think I can take a closer look at the ideas you mentioned and ask the person in the university if any of these fit and then follow up.
Thank you for all your suggestions. I'll pick something later.
Evgenii Kosogorov (Sep 27 2023 at 12:48):I may not have expressed myself very clearly. Other suggestions are still welcome :)
Last updated: Oct 13 2024 at 01:02 UTC