Abstract:

Programming languages is one of the fundamental topics in Computer Science
that deal with software systems used routinely by programmers. So are
operating systems and database systems. For these two, there exist
well-established undergraduate courses and books, that present both
practical issues and underlying theory. This is not the case for programming
languages. The courses (and books) of the past were mostly surveys, of
programming languages, or of constructs and features. There exist recent
efforts to develop new kinds of courses, but it seems there is no widely
accepted consensus on the desired contents and format. On the other hand,
the last decades have seen the development of extensive and elegant theories
for important aspects of programming languages. These have had quite an
impact on the design of modern languages, such as Java and C#. Ignorance
about these theories has a negative effect on the ability of programmers to
properly use these languages. The development of a modern course that
presents both theory and its application is sorely needed.

In the talk I will describe ideas and directions for such a course, that I
have developed in about ten years of teaching the programming languages
course at HU. Two main subjects are included in my course: operational
semantics and execution models, and (static) type systems. Semantics is the
basis for understanding a language, either for learning to program in it, or
for writing an interpreter or a compiler for it. Operational semantics has
important advantages for teaching: (1) it can be presented using a familiar
mathematical formalism, namely inductive definitions; (2) it allows to
easily derive an interpreter, and that is a good starting point for
programming projects in the course; (3) it allows to present various
execution models, both high-level and implementation oriented, and to relate
them to each other. Type systems are an important component of modern
languages, that affect the structure and behavior of programs, and are based
on elegant interesting theories. They share advantages with operational
semantics: (1) they can also be presented using inductive definitions; (2)
in many cases, their presentations allow to directly derive type checkers.
The fact that the main formalism for the course is both simple and shared
between the two main subjects has obvious advantages. 

In the talk I will describe specific contents that are included under the
two general subjects above, that I believe are appropriate for an advanced
undergraduate course. These included small step and big step operational
semantics, the substitution and the environment execution models,
monomorphic type systems and their correctness (which uses an operational
semantics to prove that that a program that type-checks will not cause a
run-time type error), and some steps into polymorphic systems. Two threads
that run through the course are the derivation of algorithms (interpreters
or type checkers) from operational semantics and type system presentations,
and the use of toy languages as a vehicle for presenting these ideas and
relating them to real languages.