A formal semantics for Javalette in the K framework

Potential supervisors: 
Research groups/keywords: 

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.

K is a well-developed framework for writing and working with formal semantics. The K framework has been used for writing formal semantics for major real-world languages such as C, Java, Verilog, JavaScript, the language of the Ethereum Virtual Machine and more.

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:

Contact us to discuss directions this could be taken in.


Date range: 
August, 2021 to August, 2026