Winter School on Denotational Semantics
Instructor: prof. Achim Jung, University of Birmingham, UK.
General Information
The school will be carried out in English, attendance is free of charge, but the number of participants is potentially limited. The exact time and venue will be announced later.
To register for the school and receive future announces please join the following group:
https://groups.google.com/forum/#!forum/jbr_winter...
Synopsis
Summary: In this course we will focus on the denotational semantics of the simply typed lambda calculus. We will in parallel introduce enough of the lambda calculus so that the course is accessible to those also who have not studied it in detail before. (In any case, for us the lambda calculus is just a very concise way of writing programs in a functional language.)
We aim to show the following results:
 the completeness of alpha, beta and eta rules with respect to the set theoretic model over the natural numbers;
 the adequacy of the Scott model for PCF;
 Milner's context lemma;
 modelling the untyped calculus.
Along the way we will discuss the substitution lemma, term models, logical relations, and basic domain theory.The first part is based on Chapter 2 of the book "Semantics of Programming Languages" by Carl A. Gunter, MIT Press 1992. The other two on "DomainTheoretic Foundations of Functional Programming" by Thomas Streicher, World Scientific 2006. Both books contain a lot more material than I can present in this course. The same is true for "Foundations for Programming Languages" by John C. Mitchell, MIT Press 1996. The common feature of these three works and my course is that the simply typed lambda calculus is taken as the starting point, whereas other texts on denotational semantics tend to begin with an (imperative) whilelanguage.
School Materials
The 1st Lecture
The 2nd Lecture
The 3rd Lecture
The 4th Lecture
The 5th Lecture
The 6th Lecture
The 7th Lecture
The 8th Lecture
The 9th Lecture
The 10th Lecture
Schools
 About schools

2731 August 2018Summer School on Category Theory

28 August  1 September 2017Summer School on Weak Memory Consistency

30 January  3 February 2017Winter School on Denotational Semantics

2226 August 2016Summer School on Game Semantics

2428 August 2015Summer School on Relational Programming

26 February 2015Winter School on Abstract Interpretation

2529 August 2014Programs and Proofs: Mechanizing Mathematics with Dependent Types

37 February 2014Winter School on Metacalculations

2630 August 2013Summer School on Memory Management