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?

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:

- Rejection sampling: generate a random binary string, check if it's balanced, if not then regenerate.
- "Dynamic programming": write a function to count the number of possible strings given a prefix, then use that function as a hint to generate a string at uniform probability.
- ???: there's a way to generate a string at uniform probability in O(nlogn). I have no idea how it works, let's find out!

Except rejection sampling, all the other algorithms can be formalized with monads.

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

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

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

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.

looks like my suggestion is perfect for your background

though if you're good at working on unfamiliar code Karl's suggestion is good too

if you're allowed to open source your work your thesis would make quite a contribution to the world

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.

I may not have expressed myself very clearly. Other suggestions are still welcome :)

Last updated: Nov 29 2023 at 20:01 UTC