Contents

• Contents
• Introduction
• Overview
  • The kernel
  • The types
  • The instructions
  • The backend
• The kernel language
  • Expression kernel
    • Sanitizer
    • Typechecker
    • Compiler
  • Kernel expression
  • Constant
  • Abstraction
  • Application
  • Local
  • Global
  • IfThenElse
  • AndOr
  • Sequence
  • Let
  • Loop
  • ExitWithValue
  • Definition
  • Parameter
  • Assignment
  • NewObject
  • FieldUpdate
  • NewArray
  • ArraySlot
  • ArraySlotUpdate
  • Tuple
  • NamedTuple
  • TupleProjection
  • TupleUpdate
  • Dummy
  • Monoid Homomorphism
  • Monoid Comprehesion
  • CompiledExpression
• The type system
  • Overview
    • Polymorphism
    • Multiple Type Overloading
    • Currying
    • Standardizing
    • Copying
    • Equality
    • Unifying
    • Boxing/Unboxing
  • Structure of the TypeChecker
  • Type Definitions
    • Type aliasing
    • Type hiding
  • Static types
  • Dynamic types
    • Extensional types
    • Conditional types
• The instruction base
• The error manager
• Conclusion
• A word on traceability
  • Relating concrete and abstract syntax for error traceability
    • Syntax errors
    • Static Semantics errors
    • Dynamic Semantics errors
  • Displaying and reading on concrete/abstract syntax
    • Displaying
    • Reading
    • Concretizing abstract syntax away with writing tables
    • Abstracting concrete syntax away with reading tables
• A four-panelled architecture
  • The Complete Kernel
    • Sanitizing
    • Type checking vs. inference
    • Compiling
  • The Complete Type System
    • The type prover
    • The type constructs
    • Defining new types
  • The Basic Instruction Set
  • The Complete Backend
    • The Runtime system
    • The Runtime objects
    • The display manager
    • The error manager
• Bibliography
• About this document ...