In this tutorial, we will show how to use the K formal semantic framework (http://kframework.org) to define your own programming languages, which is easy and fun. Specifically, the tutorial will cover the following topics:
- Use the BNF grammar notation to define programming language syntax;
- Define the computation configurations of the language, which consist of program code and its execution environment;
- Define the operational semantics of the language using rewrite rules.
- Use K to automatically generate the language tools, including a parser and an interpreter of the language.
We will be using a pedagogical and research language called FUN as an example, which captures the essence of the functional programming paradigm and includes many interesting language features such as user-defined data types,
letrec constructs for defining recursive functions, pattern matching, and a
We highly recommend that the attendants of the tutorial download the K tools from its URL (https://github.com/kframework/k) and install it on their machines (instructions have been provided for Linux-like systems; for Windows, an installation instruction on fresh Windows Subsystem for Linux is provided).
Conference DayThu 27 AugDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 17:30
Using the K Framework to Formalize Functional LanguagesTutorials at Tutorials 1
|Using the K Framework to Formalize Functional Languages|