Mini-Projects
Presentations (2018/19)
Instructions
As part of this course, you are encouraged (but not required!) to do a mini-project on a topic related to programming languages, with preference on topics that relate to the main themes studied in this course (interactive theorem proving, reasoning, and semantics). The structure and nature of the project is intentionally left open so that you can choose something that you are really interested in. However, if you decide to do a mini-project, you will have to follow the following rules:
- The topic you choose must be approved by João. You need to send João an email by the 30th of April confirming your intention to do the mini-project together with an indication of the topic you want to explore.
- You will have to present your mini-project to the class (20-minute presentation). The presentation will be in the week commencing the 27th of May.
- You are strongly encouraged to prepare a practical demo of your work (except in cases where the topic is 100% theoretical)
Please find below some suggestions for topics (you can take the main idea and change the details as you see fit, provided that it's approved by João). If you have an idea of a generic topic you would like to explore and need help refining it into a more detailed project, please get in touch.
- Use the Verified Software Toolchain to verify some C code that you find interesting (for example, a small file system or a small memory allocator)
- Explore the compiler Certicoq and/or Compcert and create demos that show how to compile Gallina into machine code using these tools
- Certified Agent-Based Programming
- Model in Coq a language for programming AI agents. Define its semantics and prove that some simple programs are correct.
- Model in Coq a language for programming AI agents. Define its semantics and prove that some simple programs are correct.
- Encode Cartesian Hoare Logic in Coq
- Explore property-based testing in Coq (see volume 4 of the book Software Foundations)
- Explore the topic of program synthesis (e.g. a very recent and interesting logic-based work is Synthetic Separation Logic)
- Projects related with Blockchain
- Explore the language Michelson used by the Tezos Blockchain and explore/improve the available Tezos Coq Encoding
- Explore the Scilla language for blockchain smart contracts. Encode a few contracts using Scilla (e.g. an auction or double auction contract)
- Explore the language Michelson used by the Tezos Blockchain and explore/improve the available Tezos Coq Encoding