informatics

Course Descriptions

• Thorsten Altenkirch: Quantum Programming

I will introduce QML a first-order functional quantum programming language, whose design is motivated by semantic considerations. To explain this I will introduce the denotational semantics of reversible and irreversible quantum programs and compare them with their classical counterparts. Finally, I will introduce an "Algebra of Quantum Programs" and discuss completeness and normalisation for this calculus. The following papers are relevant for this course:

Altenkirch and Grattage, A functional quantum programming language (LICS 2005)

Grattage and Altenkirch, A Compiler for a Functional Quantum Programming Language (Draft 2005)

Altenkirch and Grattage, QML: Quantum data and control (Draft 2005)

Altenkirch, Grattage, Vizzotto, Sabry An Algebra of Pure Quantum Programming (QPL 2005)

• Roy Crole: Operational Semantics (Provisional Indicative Description Only)

Syntax is the formal arrangement of symbols and words, often to create a language; and all programming languages have a particular syntax. Semantics is the study of meaning, and in this course we shall be concerned with the meaning of programming languages. An example may help. Consider if true then x:=3 else x:=4; and if (true) x=3; else x=4; The syntax of the two statements is clearly different, but Pascal and C(++) or Java programmers will know that their semantics should be the same. In this example, the semantics of each statement is the ``effect on a computer at run time''.

All programming languages should have a clear syntax and semantics, from the low level of microprogramming in a CPU, right up to high level programming languages. In this course you will learn methods for giving a run-time semantics to various programming languages. The languages range from high level programming languages (such as Java, C, and Haskell) to intermediate languages (which resemble assembler). We shall see that we can give both high and low level semantics to any choice of language syntax, and show that the high and low level semantics are equivalent to each other. The high level semantics describes how a large program executes by the step-by-step execution of smaller sub-programs, whose execution is easy to specify precisely. The low level semantics works by translation of a high level language into a low level language; the simpler low level language can also be executed simply and precisely.

• Martin Escardo: Operational domain theory and topology

Traditionally, domain theory and topology in programming language semantics have been applied to manufacture and study so-called denotational models. In this course we use them to study operational semantics directly. Domain theory and topology (in either of their denotational or operational manifestations) can be applied to prove program correctness, and, more interestingly, to derive the existence of unsuspected programs that perform seemingly impossible tasks with infinite objects. We will develop some examples.

• Paul Levy: Typed Lambda Calculus

We learn the typed lambda-calculus, a language for describing functions and tuples, with sum, product and function types. We look at denotational semantics, using sets and functions, the substitution lemma and equational theory. We then explore the consequences of adding computational effects such as divergence, with call-by-value and call-by-name evaluation.

• Henrik Nilsson: Advanced Functional Programming

Monads and Arrows are concepts with roots in Category Theory that has found important applications as aids for structuring functional programs and libraries. The Advanced Functional Programming stream is going to introduce and explore these concepts and their relationships, with an emphasis on practical applications like modular interpreters and embedded domain-specific languages.

• Thomas Streicher: Constructive Logic

We present Gentzen's Natural Deduction calculus which allows one to clearly separate constructive and classical logic. We briefly discuss Kripke models for constructive propositional logic and use them for proving that certain classical figures of thought are not available in constructive logic. We further introduce the concept of "Propositions-as-Types" and the basic ideas of Martin-Löf type theory. Finally we give a more detailed account of the constructive treatment of Peano arithmetic, i.e. we show that the provably recursive functions of Peano arithmetic are those number theoretic functions which can be implemented in Gödel's T, a simply typed λ-calculus extended by primitive recursion in all higher types.

• Emilio Tuosto: Concurrency and Mobility

Concurrent systems have acquired great momentum during the last decades and, nowadays, it is hard to think to systems which work in isolation without being connected to remote systems. From its very first appearance, it was clear that features and peculiarities of concurrency were hard to be captured using classic models and semantics adopted for sequential computations. An example might clarify (from R. Milner "Communication and Concurrency, Prentice Hall 1989):

 P is x:=1 Q is x:=0;x:=x+1
are equivalent sequential programs. Indeed, after their executions, variable x is set to 1. What happens if P and Q run concurrently? The final value of x might be either 1 or 2!

Modern systems are "mobile" under many acceptations. One of those is link mobility, namely the possibility that a concurrent system dynamically reconfigures its connections. Mixing concurrency and mobility yields quite interesting new phenomena to study.

Traditionally CCS and pi-calculus, two processes calculi invented by R. Milner, have been widely used to study many facets of concurrent and mobile systems. Notably, behavioural equivalences have been proposed as suitable observational semantics and extensively studied in these contexts.

In this course, you will learn fundamental notions related to concurrent and mobile systems and use them for formally reasoning on such systems. After introducing basic notions as SOS and bisimulation equivalence in CCS, we consider the pi-calculus framework and how the notion of behavioural equivalences have been rephrased in its more general context. We will see the impact of link mobility on notions like bisimulation and labelled transition systems. More precisely, the distinguishing feature of pi-calculus is the ability of dynamically generating new names. This, together with the possibility of communicating names, yields several complications that are reflected on the operational and observational semantics of the calculus and that will be discussed in the course.

 Author: Roy Crole.© University of Leicester January 2006. Last modified: 13th March 2006, 14:46:58.Informatics Web Maintainer. This document has been approved by the Head of Department.