K Tutorial

From K Framework
Jump to: navigation, search

Here you will learn how to use the K tool to define languages by means of a series of screencast movies. It is recommended to do these in the indicated order, because K features already discussed in a previous language definition will likely not be rediscussed in latter definitions. The screencasts follow quite closely the structure of the files under the tutorial folder in the K tool distribution. If you'd rather follow the instructions there and do the tutorial exercises yourself, then go back to http://kframework.org and download the K tool, if you have not done it already. Or, you can first watch the screencasts below and then do the exercises, or do them in parallel.


K Overview

Make sure you watch the K overview video before you do the K tutorial:

[9'59"]   K Overview

Learning K

[34'46"]   Part 1: Defining LAMBDA

Here you will learn how to define a very simple functional language in K and the basics of how to use the K tool. The language is a call-by-value variant of lambda calculus with builtins and mu, and its definition is based on substitution.

[04'07"]   Lesson 1, LAMBDA: Syntax Modules and Basic K Commands
[04'03"]   Lesson 2, LAMBDA: Module Importing, Rules, Variables
[02'20"]   Lesson 3, LAMBDA: Evaluation Strategies using Strictness
[03'13"]   Lesson 4, LAMBDA: Generating Documentation; Latex Attributes
[04'52"]   Lesson 5, LAMBDA: Adding Builtins; Side Conditions
[02'14"]   Lesson 6, LAMBDA: Selective Strictness; Anonymous Variables
[05'10"]   Lesson 7, LAMBDA: Derived Constructs; Extending Predefined Syntax
[02'40"]   Lesson 8, LAMBDA: Multiple Binding Constructs (uncommented)
[06'07"]   Lesson 9, LAMBDA: A Complete and Commented Definition (commented)

[37'07"]   Part 2: Defining IMP

Here you will learn how to define a very simple, prototypical textbook C-like imperative language, called IMP, and several new features of the K tool.

[09'15"]   Lesson 1, IMP: Defining a More Complex Syntax
[04'21"]   Lesson 2, IMP: Defining a Configuration
[10'30"]   Lesson 3, IMP: Computations, Results, Strictness; Rules Involving Cells
[09'16"]   Lesson 4, IMP: Configuration Abstraction, Part 1; Types of Rules
[03'45"]   Lesson 5, IMP: Completing and Documenting IMP

[33'10"]   Part 3: Defining LAMBDA++

Here you will learn how to define constructs which abruptly change the execution control, as well as how to define functional languages using environments and closures. LAMBDA++ extends the LAMBDA language above with a callcc construct.

[06'28"]   Lesson 1, LAMBDA++: Abrupt Changes of Control (substitution-based, uncommented)
[08'02"]   Lesson 2, LAMBDA++: Semantic (Non-Syntactic) Computation Items
[03'21"]   Lesson 3, LAMBDA++: Reusing Existing Semantics
[03'37"]   Lesson 4, LAMBDA++: Do Not Reuse Blindly!
[05'19"]   Lesson 5, LAMBDA++: More Semantic Computation Items
[06'23"]   Lesson 6, LAMBDA++: Wrapping Up and Documenting LAMBDA++ (environment-based)

[46'46"]   Part 4: Defining IMP++

Here you will learn how to refine configurations, how to generate fresh elements, how to tag syntactic constructs and rules, how to exhaustively search the space of non-deterministic or concurrent program executions, etc. IMP++ extends the IMP language above with increment, blocks and locals, dynamic threads, input/output, and abrupt termination.

[07'47"]   Lesson 1, IMP++: Extending/Changing an Existing Language Syntax
[04'06"]   Lesson 2, IMP++: Configuration Refinement; Freshness
[06'56"]   Lesson 3, IMP++: Tagging; Superheat/Supercool Kompilation Options
[05'21"]   Lesson 4, IMP++: Semantic Lists; Input/Output Streaming
[04'30"]   Lesson 5, IMP++: Deleting, Saving and Restoring Cell Contents
[11'40"]   Lesson 6, IMP++: Adding/Deleting Cells Dynamically; Configuration Abstraction, Part 2
[??'??"]   Lesson 7, IMP++: Everything Changes: Syntax, Configuration, Semantics
[06'26"]   Lesson 8, IMP++: Wrapping up Larger Languages

[17'03"]   Part 5: Defining Type Systems

Here you will learn how to define various kinds of type systems following various approaches or styles using K.

[10'11"]   Lesson 1, Type Systems: Imperative, Environment-Based Type Systems (IMP++ type checker)
[06'52"]   Lesson 2, Type Systems: Substitution-Based Higher-Order Type Systems (LAMBDA type checker, substitution, uncommented)
[??'??"]   Lesson 3, Type Systems: Environment-Based Higher-Order Type Systems (LAMBDA type checker, environment, uncommented)
[??'??"]   Lesson 4, Type Systems: A Naive Substitution-Based Type Inferencer (for LAMBDA, uncommented)
[??'??"]   Lesson 5, Type Systems: A Naive Environment-Based Type Inferencer (for LAMBDA, uncommented)
[??'??"]   Lesson 6, Type Systems: Parallel Type Checkers/Inferencers (for LAMBDA, uncommented)
[??'??"]   Lesson 7, Type Systems: A Naive Substitution-based Polymorphic Type Inferencer (for LAMBDA, uncommented)
[??'??"]   Lesson 8, Type Systems: A Naive Environment-based Polymorphic Type Inferencer (for LAMBDA, uncommented)
[??'??"]   Lesson 9, Type Systems: Let-Polymorphic Type Inferencer (Damas-Hindley-Milner) (for LAMBDA, uncommented)

[??'??"]   Part 6: Miscellaneous Other K Features

Here you will learn a few other K features, and better understand how features that you have already seen work.

[??'??"]   ...

Learning Language Design and Semantics using K

[??'??"]   Part 7: SIMPLE: Designing Imperative Programming Languages

Here you will learn how to design imperative programming languages using K. SIMPLE is an imperative language with functions, threads, pointers, exceptions, multi-dimensional arrays, etc. We first define an untyped version of SIMPLE, then a typed version. For the typed version, we define both a static and a dynamic semantics.

[??'??"]   Lesson 1, SIMPLE untyped
[??'??"]   Lesson 2, SIMPLE typed static
[??'??"]   Lesson 3, SIMPLE typed dynamic

[??'??"]   Part 8: KOOL: Designing Object-Oriented Programming Languages

Here woul will learn how to design object-oriented programming languages using K. KOOL is an object-oriented language that extends SIMPLE with classes and objects. We first define an untyped version of KOOL, then a typed version, with both a dynamic and a static semantics.

[??'??"]   Lesson 1, KOOL untyped
[??'??"]   Lesson 2, KOOL typed dynamic
[??'??"]   Lesson 3, KOOL typed static

[??'??"]   Part 9: FUN: Designing Functional Programming Languages

Here woul will learn how to design functional programming languages using K. FUN is a higher-order functional language with general let, letrec, pattern matching, references, lists, callcc, etc. We first define an untyped version of FUN, then a let-polymorphic type inferencer.

[??'??"]   Lesson 1, FUN untyped, Environment-Based
[??'??"]   Lesson 2, FUN untyped, Substitution-Based
[??'??"]   Lesson 3, FUN polymorphic type inferencer

[??'??"]   Part 10: LOGIK: Designing Logic Programming Languages

Here you will learn how to design a logic programming language using K.

[??'??"]   Lesson 1, LOGIK
Personal tools