Some Proposals Under The Supervision Of Engelbert Hubbers
These projects are not related to security, but more to theoretical computing science.
- Proof systems (natural deduction, sequent calculus) for propositional, predicate, or modal logic.
- Formalizing a TRS framework in Coq to support the course Semantics and Rewriting, possibly based on tools like CSI, AProVE, Cime3, CoLoR.
- Formalizing a TRS framework in the computer algebra system Maxima so it can be used as a backend for the Sowiso platform.
- Automatic evaluation of Coq scripts, in particular, for the courses Logic and Applications and Semantics and Correctness. Compare for instance the options of GitLab Classroom, Jupyter notebooks, and the Software Foundation approach. (This topic is already taken.)
- Formalizing logic puzzles to derive provably correct solutions. (This topic is already taken.)
- Investigate whether the Waterproof system (https://research.tue.nl/en/publications/waterproof-educational-software-for-learning-how-to-write-mathema) can be used for courses like Mathematical Structures, Logic and Applications, and Semantics and Correctness. (This topic is already taken.)
If you are interested in one of these topics, please send an email to Engelbert Hubbers via hubbers@cs.ru.nl .
