Practical foundations for programming languages

Comprehensive theory of programming languages based on:

• Type system.
• Small-step/Structural operational semantics (SOS).

Language concepts are precisely defined by:

• Static semantics.
• Dynamic semantics.

-> Essential intuitive and rigorous tools.

-> Rely on only elementary mathematics.

Usages of Static semantics and Dynamic semantics:

• Analyze and prove properties of languages.
• Provide the framework for combining and comparing language features.

Concepts:

• Fundamental data types: Sums and products.
• Polymorphic and abstract types.
• Dynamic typing.
• Dynamic dispatch.
• Subtyping and refinement types.
• Symbols and dynamic classification.
• Parallelism and cost semantics.
• Concurrency and distribution.

Applications:

• Language implementation.
• Development of logics for reasoning about programs.
• Formal verification language properties such as type safety.