Coq Programming & Formal Verification - Internship

We are seeking interns who are already strong in Coq programming and have
hands-on experience using the Coq proof assistant for formalization and proof
development. This internship focuses on advanced Coq development, applying
theory of computation concepts through rigorous, executable proofs and
verified models.

Selected intern's day-to-day responsibilities include:

1. Develop non-trivial Coq programs and proofs independently
2. Formalize Theory of Computation concepts (automata, grammars, Turing
machines, decidability) in Coq
3. Write clean, well-structured Coq scripts using: Inductive types, recursive
functions, dependent types (where applicable)
4. Prove correctness, termination, and logical properties
5. Refactor and optimize existing Coq codebases
6. Review and improve proof strategies for clarity and reusability