Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020

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, let/letrec constructs for defining recursive functions, pattern matching, and a callcc construct.

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).

Thu 27 Aug

Displayed 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
Xiaohong Chen University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign