SICSA Summer School on Types and Programming Languages

Thursday June 7th - Saturday June 9th 2012

School of Computer Science, University of St Andrews

(Colocated with Trends in Functional Programming 2012)


The role of types in programming language research, including language design and compiler construction, has increased greatly in recent years. Type systems research has led to new concepts and methods in program verification, such as dependently typed programming (e.g. Agda, Epigram and Idris). Domain specific languages and type systems have led to new approaches to network and security protocol verification, including the F7 language, an enhancement to F# developed at Microsoft Research in Cambridge, motivated by the desire to verify security properties of code.

This summer school will give participants an overview of the research landscape and state of the art in programming language theory, focussing in particular on types for program specification and verification. The school will consist of a series of lectures covering theoretical topics (e.g. category theory and type lambda calculus) and practical topics (e.g. security oriented languages, and verified systems programming). Thus the school will cover "what", "how", and "why" --- what is a typed programming language, how is it designed and implemented, and why are they applicable to wider problems in Computer Science.


Confirmed speakers are:

There will also be a session of "lightning talks" giving students 15 minutes to present their own research.


Wednesday 5th June
Thursday 6th June
Friday 7th June
Saturday 8th June


(Further resources will be added here)


Registration is now closed.


For more details, contact Edwin Brady (