Midlands Graduate School
-
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.
Notes (from 2005).
-
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.
reference 1
reference 2
-
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.
|
|
