Baltoli/k-spls

K definitions for SPLS July 2022

K Framework SPLS Talk (July 2022)

This repository contains K definitions to go along with my talk at the July 2022 edition of SPLS.

To follow along, first set up your development environment to build the K framework¹ following the README here. Then, build the K framework with:

git submodule update --init --recursive
make deps

You can build the full set of semantics I mention with:

make

once K itself is built. These are:

• Two tiny definitions used to demonstrate K basics
• A simple imperative language with account balance state
• A variant of the pi-calculus

The examples/ directory contains a set of examples you can run with (for example):

make examples/in.one.run

for the file examples/in.one.

Footnotes

1. Note that if you have difficulty building from source, you can instead install K from your system package manager following the instructions on the same page, and setting SYSTEM_K=1 when you run make later on. ↩