Defining Programming Languages in a Formal Framework
Logical frameworks allow formally defining the syntax and semantics of languages such as type theories and logics. Here the framework provides the language-independent concepts (names, declarations, typed expressions, proofs, etc.), and individual languages are defined by specifying the rules to parse and type-check the language-specific concepts (e.g., quantification or function types).
In this project, we extend that approach to also representing programing languages. We add an execution algorithm to the existing algorithms for parsing and type-checking that interprets a program. Execution creates a heap and stack and then interprets a program step-wise using language-specific rules that describe the effect that the execution of one program step has on stack, heap, and IO.
As concrete case studies and applications, we rigorously define simple programming languages akin to mainstream languages like Java or Haskell.