Semantics Specification of Types and Programming Languages

FDA184, 2005VT

Status	Archive
School	National Graduate School in Computer Science (CUGS)
Division	SAS
Owner	Peter Fritzson


	Log in

Course plan

Lectures

Lectures and seminars by
invited speakers and course participants.

Recommended for

All graduate students

The course was last given

New course.

Goals

Provide insight into semantics specification of typing and programming language concepts.

Learn practical specification of such concepts using Natural Semantics and operational

semantics.

Prerequisites

Undergraduate courses in programming languages.
Also: either the ECSEL foundational course Principles of programming languages and systems,
or at least one of the undergraduate courses
Compiler Construction, Formal Languages and Automata, Programming Theory
or equivalent.

Specification of Untyped Systems
Specification of Untyped Lambda-Calcuclus

Specification of Simple Types
Specification of Typed Arithmetic Expressions
Specification of Simply Typed Lambda Calculus
Specification of Function Types
Specification of Based Types
Specification of the Unit Type
Specification of Pairs, Tuples, Records, Sums, Variants
Specification of Normalization of simple types
Specification of References, Store typesing, Safety
Specification of Exception handling

Specification of Subtyping
Specification of Subsumption
Specification of Top and Bottom Types
Specification of Intersection of Union types
Specification of Imperative Objects

Specification of Recursive Types
Specification of Finite and Infinite Tyeps

Specification of Polymorphism
Specification of Type variables and substitutions
Specification of Constraint-based typing
Specification of Unification

Natural Semantics based generation of compilers
and interpreters

RML - The Relational Meta Language
Interpreter generation
Compiler Generation
Interpretive semantics
Translational semantics
Interfacing to parsers
Debugging of Natural Semantics specifications
Type checking
A large translational semantics

Organization

Seminars with active participation by course participants, some lectures, presentations by course participations, practical semantics specification and compiler/interpreter/type checker

generation from semantics specification.
Group discussions and presentations of solutions.

Literature

Benjamin C. Pierce: "Types and Programming Languages"
MIT Press 2002

Peter Fritzson: "Efficient Language Implementation by Natural Semantics", book draft.

Lecturers

Peter Fritzson, invited speakers

Examiner

Peter Fritzson

Examination

Examination: oral presentations of the course literature and problem solving of semantics specification

Specification excercises

Credit

4 credits

Organized by