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 IBC026 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 IBC026 Semantics and Correctness, which in its turn expects that you did the course Logic and Applications, and one of the courses IPC002 Languages and Automata or IPK001 Introduction to Formal Reasoning, and preferably the course IBC003 Computability. Students that try to do Semantics and Rewriting without having done Semantics and Correctness, have a good 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.
|
|
|
The final grade for this course is based on 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 the final grade will be (E+E+P)/3, rounded according to the rules in Osiris. In all other cases, students will not pass the course.
|
|
|