Abstract:

For the purpose of denotational semantics and for reasoning about
programming  languages and lambda-calculi, D.S. Scott has introduced
mathematical structures known under the name domains. The
mathematical theory of domains has order theoretical, topological
and category theoretical aspects.

When using domains for semantics, every operator in the programming
language has to be modelled by a construction on the semantic
domains. Nondeterminism is modelled by powerdomain constructions
(Hoare, Smyth, Plotkin).

Probabilistic choice is of a different flavour and is modelled in
probabilistic powerdomains, a domain theoretical variant of the
classical space of probability measures (Jones and Plotkin).

Our starting point is a simple imperative language with both
nondeterministic and probabilistic choice as considered by Morgan,
McIver, Seidel, etc. For the semantics one has to combine the two
powerdomain constructions. In the direct semantics a programme will
be interpreted by a function associating to every initial state a
certain set of 'probability distributions' on the state space. In
predicate transformer semantics one associates with every observable
property of a program the weakest precondition on the initial states
which guarantees the desired property after program execution.

The two semantics are shown to be equivalent by adapting Minkowski's
classical procedure of representing convex bodies in space by
sublinear functionals to our setting. We are able to do this not
only for discrete but also for continuous state spaces in the spirit
of domain theory.

Short CV:

Professor Klaus Keimel has studied Mathematics and Physics at the
University of T\"ubingen (Germany). He earned the equivalent of a
Master's Degree there. He held a research assistantship at Tulane
University, New Orleans, and a PhD fellowship at Paris before he
obtained his PhD from the University of T\"ubingen. In 1970 he
obtained the Doctorat d'Etat at the University Paris VI.

He worked as an Assistant and Associate Professor in Paris and Tours
(France) for five years until he became a Professor of Mathematics
at Darmstadt (Germany). He held visiting positions at University
Paris VI, University of California at Riverside, Tulane University
at New Orleans, Louisiana State University at Baton Rouge,
University of Birmingham, University of Edinburgh.

Klaus Keimel's research areas are the Mathematical Foundations of
Computer Science, Semantics of Programming Languages, Domain Theory,
Probability and Nondeterminism. He is the author and co-author of
more than fifty refereed research papers and six monographs, among
them 'Continuous Lattices and Domains', Encyclopedia of  Mathematics
and its Applications, vol. 93, Cambridge University Press, 2003,
xxxvi+591 pp. (joint with G.Gierz, K.H.Hofmann, J.D.Lawson,
M.Mislove, and D.S.Scott.)