Upon completion of this course, the students are able to:
- Model computations in functional languages using rewrite systems (term rewrite systems, lambda calculus). Analyze computational properties of rewrite systems, for example, confluence and termination.
- Design alternative formalisms for state and memory models for semantics of imperative programming languages.
- Model the semantics of existing programming languages by selecting appropriate existing formalisms, extending and modifying these if necessary. Perform a case study using the resulting model. Present the results in a professional report and review reports handed in by other students.
|
|
In this course, you will learn about computation models that are used for functional programming languages. These models form the basis for the implementation of such functional languages. Moreover, they can be used for studying the behavior of functional programs.
In addition, you will learn to design alternative semantic models for characterizing the semantics of imperative programming languages. You will apply this in a case study on a real-life language. This part of the course builds upon the course Semantics and Correctness.
Instructional Modes
The learning cycle of the course typically starts with a two hour plenary lecture. Then, students have to work on a learning task. Finally, during a two hour plenary response lecture, students can obtain feedback about the learning tasks.
In addition, students participate in a group project about semantics of imperative languages. This results in a written report and a review of a report handed in by a different group.
|
|
|
You have experience in programming, both in imperative languages and functional languages. In addition, you are able to
- specify programming languages or extensions of programming languages using context-free grammars;
- specify operational semantics of imperative languages using natural semantics as well as using structural operational semantics;
- formulate clearly, both in motivating solutions and in expressing mathematical proofs.
These prerequisites can be obtained by doing the course Semantics and Correctness, which in its turn expects that you did the course Logic and Applications, and one of the courses Languages and Automata or Introduction to Formal Reasoning, and preferably the course Computability. Students that try to do Semantics and Rewriting without having done Semantics and Correctness, have a reasonable chance to pass the exam on term rewrite systems and lambda calculus, but they usually fail the group project of the Semantics and Rewriting course.
|
|
You will get a grade E for the digital Cirrus exam about term rewrite systems and lambda calculus, and a grade P for the project on semantics of imperative programming languages. If both of these are at least 5.5, then your final grade will be (E+E+P)/3, rounded according to the rules in Osiris. In all other cases, you will not pass the course.
|
|
|