A formal semantics for Javalette in the K framework
This proposal is about writing formal semantics in K for the Javalette programming language, and exploring what formal semantics in the K framework can be used for. Here Javalette is the programming language used in the TDA283/DIT300 Compiler Construction course.
The project can explore the following research questions:
- What would a formal semantics for core Javalette look like when expressed in K?
- How can we gain confidence that a formal semantics is correct? (Hint: one could try running the test programs from the Compiler Construction course on the formal semantics.)
- How difficult would it be to extend the formalisation to the Javalette extensions that the Compiler Construction course proposes (see link below)?
- The K framework comes with several tools that take K semantics as input. What can we get "for free" from these tools given our semantics? How usable are those artefacts?
- Can the semantics be used as a reference implementation, against which we can perform more extensive of student implementations?
In practice, this project requires learning to use the K framework, writing formal semantics in K for Javalette, and working with the tools of the K framework to see what they can do.
This project would be jointly supervised by:
- Rikard Hjort former MPALG student and Senior Formal Verification Engineer at Runtime Verification Inc. (email@example.com)
- Magnus Myreen lecturer of TDA283/DIT300 Compiler Construction (firstname.lastname@example.org)
Contact us to discuss directions this could be taken in.
- K framework: https://kframework.org/
- Runtime Verification Inc.: https://runtimeverification.com/
- Javalette language: https://github.com/myreen/tda283/blob/master/project/javalette.md
- Javalette extensions: https://github.com/myreen/tda283/blob/master/project/extensions.md