This course introduces algebraic methods based on semirings and Kleene algebras that have recently found some applications in computing. These mathematical structures support the analysis of programs and systems through simple equational calculi, they provide a uniform view on models based on processes, games, traces, languages or relations, they admit powerful decision procedures, and they are suitable for off-the-shelf automated theorem proving. The first lecture introduces semirings and Kleene algebras, it presents the basic calculus and some interesting models, and it discusses Kozen's fundamental completeness result with respect to regular expressions. The second lecture introduces extensions of semirings and Kleene algebras by modal operators and it relates the resulting algebraic structures with popular logics of programs. The third lecture discusses applications of these formalisms in Hoare-style program verification, termination analysis, program refinement and concurrency control. The fourth lecture introduces to automated theorem proving with the algebraic structures considered and beyond.
This course is directly related to the introductory courses Operational Semantics, Category Theory, and Typed Lambda Calculus. A denotational semantics assigns objects of a category to program types, and morphisms of that category to programs. In very restricted situations, the category of sets and functions works (a type is a set, a program is a function). In more complex situations, more sophisticated categories are needed, such as domains or games. In this course we study on domains. (Another course studies games.) Domains are particularly suited to reason about the relationship between the finite character of computers and the infinite nature of mathematical entities one wants to compute with (functions, infinite sequences over an alphabet, real numbers etc.). Typically, domains are sold as a tool for aiding program verification. Here we instead emphasize their role in discovering algorithms one wouldn't otherwise have thought of, and that are slightly surprising and counter-intuitive. For example, there are infinite sets that admit exhaustive search in finite time, and some kinds of function types have decidable equality. A domain is a mathematical structure that contains (possibly infinite) entities together with (finite) approximate versions, in such a way that any entity (that we imagine) can be completely recovered from its approximate versions (that we see in the computer screen). In this course we develop both the mathematical aspects and some applications such as the above.
Two languages are presented, a simple imperative language with state, and a simple pure (that is, stateless) eager functional language. For each language we present an evaluation (natural) semantics, an abstract machine, and we prove that the machine and evaluation semantics are mutually correct. This forms a nice story for a course of five (rapid) lectures. We do not cover types in great detail (polymorphism and type inference are not covered). Also, we do not cover transition (Plotkin) semantics, nor any form of lazy evaluation for the functional language. The MGS notes are based on previous courses given by the author which do cover these topics, and also denotational semantics.
This course provides an introduction to ordinal-based proof theory, and the notion of proof-theoretic strength particularly for type-theories, or systems which can be seen as type-theories through the Curry-Howard correspondence. The technical content will be divided into 3 pieces,
I'll stress connections with programming, where possible. I promote an algebraic approach to this subject, which is perhaps eccentric. One or two juicy exercises will be set to chew on between sessions. Pointers will be given for further study. If there is any time, I might gossip about some interesting problems in modern ordinal-based proof theory.
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.
Page maintained by E.Ritter@cs.bham.ac.uk
Last modified: Tue Apr 15 10:38:59 BST 2008