- TypeScript in Truffle: Internship at Oracle Labs in Zürich. Contact Eelco Visser
- Océ DSL: Internship at Océ. Contact Eelco Visser
- Code Generation at CERN: Internship at CERN in Geneva. Contact Eelco Visser
- Verified compilation of inline assembly in C. Contact Robbert Krebbers
- Formal semantics of the C preprocessor. Contact Robbert Krebbers
- Reasoning about programs with I/O. Contact Robbert Krebbers
- Verification of concurrent algorithms. Contact Robbert Krebbers
- Prove coherence of traits in Rust. Contact Robbert Krebbers
- Incremental type checking for Rust. Contact Sebastian Erdweg
- Styx: An incremental programming language. Contact Sebastian Erdweg
- How to compile functional programs using arrows? Contact Sebastian Erdweg
- Programmable refactorings: Preserving a program’s control flow. Contact Sebastian Erdweg
Spoofax Shell: Create an interactive shell for the Spoofax Language Workbench that can be used with all languages defined in Spoofax.
Safe and Stateful Native Code Execution: To support a wider range of language in the WebLab programming education system, it is necessary to safely execute native code on the server. Furthermore, in order to support interactive sessions, such executions should maintain a stateful connection with a client.
- Spoofax LSP: Adapt Spoofax (Core) so that it supports the Language Service Protocol.