Semantic Framework

pdf epub mobi html

Section 1: Basic K Concepts

Lesson 1.1: Setting up a K Environment

Lesson 1.2: Basics of Functional K

Lesson 1.3: BNF Syntax and Parser Generation

Lesson 1.4: Disambiguating Parses

Lesson 1.5: Modules, Imports, and Requires

Lesson 1.6: Integers and Booleans

Lesson 1.7: Side Conditions and Rule Priority

Lesson 1.8: Literate Programming with Markdown

Lesson 1.9: Unparsing and the format and color attributes

Lesson 1.10: Strings

Lesson 1.11: Casting Terms

Lesson 1.12: Syntactic Lists

Lesson 1.13: Basics of K Rewriting

Lesson 1.14: Defining Evaluation Order

Lesson 1.15: Configuration Declarations and Cell Nesting

Lesson 1.16: Maps, Semantic Lists, and Sets

Lesson 1.17: Cell Multiplicity and Cell Collections

Lesson 1.18: Term Equality and the Ternary Operator

Lesson 1.19: Debugging with GDB or LLDB

Lesson 1.20: K Backends and the Haskell Backend

Lesson 1.21: Unification and Symbolic Execution

Lesson 1.22: K Deductive Verification

Section 2: Intermediate K Concepts

Lesson 2.1: Macros, Aliases, and Anywhere Rules

Lesson 2.2: Fresh Constants

Lesson 2.3: KLabels and Abstract Syntax

Lesson 2.4: Overloaded Symbols

Lesson 2.5: Matching Logic Connectives and #Or Patterns

Lesson 2.6: Function Context

Lesson 2.7: Record Productions and Named Nonterminals

Lesson 2.8: #fun and #let

Lesson 2.9: #as Patterns

Lesson 2.10: The Matching Operators, :=K and :/=K

Lesson 2.11: Uncommon Evaluation Order Concepts

Lesson 2.12: IEEE 754 Floating Point and Fixed Width Integers

Lesson 2.13: Alpha-renaming-aware Substitution

Lesson 2.14: File I/O

Lesson 2.15: String Buffers and Byte Sequences

Lesson 2.16: The Intermediate Language of K, KORE

Lesson 2.17: Debugging Proofs using the Haskell Backend REPL

K Tool Reference

Part 1: Defining LAMBDA

Lesson 1, LAMBDA: Syntax Modules and Basic K Commands

Lesson 2, LAMBDA: Module Importing, Rules, Variables

Lesson 3, LAMBDA: Evaluation Strategies using Strictness

Lesson 4, LAMBDA: Generating Documentation; Latex Attributes

Lesson 5, LAMBDA: Adding Builtins; Side Conditions

Lesson 6, LAMBDA: Selective Strictness; Anonymous Variables

Lesson 7, LAMBDA: Derived Constructs; Extending Predefined Syntax

Lesson 8, LAMBDA: Multiple Binding Constructs

Lesson 9, LAMBDA: A Complete and Commented Definition

Part 2: Defining IMP

Lesson 1, IMP: Defining a More Complex Syntax

Lesson 2, IMP: Defining a Configuration

Lesson 3, IMP: Computations, Results, Strictness; Rules Involving Cells

Lesson 4, IMP: Configuration Abstraction, Part 1; Types of Rules

Lesson 5, IMP: Completing and Documenting IMP

Part 3: Defining LAMBDA++

Lesson 1, LAMBDA++: Abrupt Changes of Control

Lesson 2, LAMBDA++: Semantic (Non-Syntactic) Computation Items

Lesson 3, LAMBDA++: Reusing Existing Semantics

Lesson 4, LAMBDA++: Do Not Reuse Blindly!

Lesson 5, LAMBDA++: More Semantic Computation Items

Lesson 6, LAMBDA++: Wrapping Up and Documenting LAMBDA++ (environment-based)

Part 4: Defining IMP++

Lesson 1, IMP++: Extending/Changing an Existing Language Syntax

Lesson 2, IMP++: Configuration Refinement; Freshness

Lesson 3, IMP++: Tagging; Superheat/Supercool Kompilation Options

Lesson 4, IMP++: Semantic Lists; Input/Output Streaming

Lesson 5, IMP++: Deleting, Saving and Restoring Cell Contents

Lesson 6, IMP++: Adding/Deleting Cells Dynamically; Configuration Abstraction, Part 2

Lesson 7, IMP++: Everything Changes: Syntax, Configuration, Semantics

Lesson 8, IMP++: Wrapping up Larger Languages

Part 5: Defining Type Systems

Lesson 1, Type Systems: Imperative, Environment-Based Type Systems

Lesson 2, Type Systems: Substitution-Based Higher-Order Type Systems

Lesson 3, Type Systems: Environment-Based Higher-Order Type Systems

Lesson 4, Type Systems: A Naive Substitution-Based Type Inferencer

Lesson 5, Type Systems: A Naive Environment-Based Type Inferencer

Lesson 6, Type Systems: Parallel Type Checkers/Inferencers

Lesson 7, Type Systems: A Naive Substitution-based Polymorphic Type Inferencer

Lesson 8, Type Systems: A Naive Environment-based Polymorphic Type Inferencer

Lesson 9, Type Systems: Let-Polymorphic Type Inferencer (Damas-Hindley-Milner)

Learning Language Design and Semantics using K

Part 7: SIMPLE: Designing Imperative Programming Languages

Lesson 1, SIMPLE untyped

Lesson 2, SIMPLE typed static

Lesson 3, SIMPLE typed dynamic

Part 8: KOOL: Designing Object-Oriented Programming Languages

Lesson 1, KOOL untyped

Lesson 2, KOOL typed dynamic

Lesson 3, KOOL typed static

Part 9: FUN: Designing Functional Programming Languages

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

Lesson 1, LOGIK

Projects using K

Lesson 2.17: Debugging Proofs using the Haskell Backend REPL

Return to Top

Click here to return to the Table of Contents for Section 2.

Lesson 2.17: Debugging Proofs using the Haskell Backend REPL

333 North Green Street, Chicago, IL

2024 © all rights reserved

privacy policy | terms of use