Behavioural equivalence in higher-order calculi

A language is "higher-order" if program code can be passed around, that is, terms of the language can be values. Developing a theory of behavioural equivalence in higher-order languages can be hard. Particularly challenging can be: (1) the proof of congruence, (2) obtaining definitions and results that scale to languages with different features. In the talk, I will discuss the problems that higher-order languages present, and some approaches to tackle these problems. I will start from the lambda-calculus --the best known higher-order language-- and then move to the higher-order pi-calculus.