Midlands Graduate School
-
Georg Struthr: Kleene Algebra
Abstract
Kleene algebras are foundational structures in computing. Their
applications include formal language and automata theory, program
semantics, construction and verification. These lectures survey the core
theory, recent developments and some applications. The first part
introduces axiomatic variants and their most important models. It also
discusses two classical completeness results with respect to the
equational theory of regular expressions. The second part introduces
extensions of Kleene algebras by modal operators, explores connections
with logics of programs such as dynamic, temporal and Hoare logics, and
discusses representability and axiomatisability results in this setting.
The third part surveys another extension towards concurrency and
discusses extensions of Hoare logic related to the Owicki-Gries
calculus, concurrent separation logic and the rely-guarantee method,
which can be derived in this setting. The content of the exercise
sessions depends on the interests of the participants. Possible topics
include completeness theorems, applications in verification or the
implementation of Kleene algebras in Isabelle/HOL.
-
Eike Ritter: Security and applied pi-calculus
Process Calculi for Protocol Verification
In this lecture course I will present the applied Pi-calculus, a
process calculus specifically designed for the verification of
security protocols. I will give example of security protocols and
security properties and show how both the protocols and the
properties can be modelled in the applied Pi-calculus. I will also
briefly present ProVerif, which is a tool for automatically verifying
security properties specified in the applied Pi-calculus.
-
Rick Thomas: Formal Languages and Group Theory
Formal Languages and Group Theory
The purpose of this series of lectures is to survey some connections between formal language theory on the one hand and group theory on the other.
Groups arise in many ways and are often described by means of "presentations". A presentation for a group G consists of a set of generators for G and a set of relations between words in the generators that is sufficient to define the group operation. If we have a presentation for G with a finite set of generators and a finite set of relations, then we say that G is "finitely presented".
One of the classical results in group theory is the unsolvability of the word problem for finitely presented groups; this says that there are finite presentations such that there is no algorithm to decide whether or not a word in the generators represents the identity element of the group defined by that presentation. An alternative way of describing this situation is as follows: there are finitely presented groups G such that, if we consider the set W of all words representing the identity element of G, then there is no algorithm for determining membership of W. There is also an elegant result of Boone and Higman describing which finitely generated groups have a solvable word problem.
One natural question that arises from this is the following: if we take some restricted model of computation, which groups have a word problem which is decidable within that model? The restriction might be, for example, that the word problem is accepted by a particular type of automaton or generated by a particular type of grammar.
The purpose of these lectures is to survey some of what is known in this field. We will not assume any prior knowledge of group theory and we will review what we need from formal language theory.
Lecture Notes
-
Natasha Alechina: Modal Logic
Course Material
-
Nikos Tzevelekos: Typed Lambda-Calculus
Typed Lambda-Calculus
As a language for describing functions, any literate computer scientist would expect to understand the vocabulary of the lambda calculus. It is folklore that various forms of the lambda calculus are the prototypical functional programming languages, but the pure theory of the lambda calculus is also extremely attractive in its own right. This course introduces the terminology and philosophy of the lambda calculus, and then covers a range of self-contained topics, looking into both typed and untyped variants.
Lecture Notes.
-
Venanzio Capretta: Coalgebras and Infinite Data Structures
Coalgebra and Infinite Data Structures
Although computers have a finite memory and cannot store an infinite amount of information, Functional Programming and Type Theory allow us to represent infinite mathematical objects.
These are represented as processes that generate part of the structure at every step.
The mathematical/categorical formulation for these processes is the notion of coalgebra.
The first part of the course is an introduction to coalgebras with important examples like streams (infinite sequences) and non-well-founded trees.
The most powerful proof method for infinite data structures is the Coinduction Principle, which allows us to prove the equality of two objects by a bisimulation, itself an infinite process that generates the equality by successive stages.
We will study methods to construct sound infinite objects, to solve recursive equations on them and to prove their properties.
Examples will be given using functional programming in Haskell and formal reasoning in Coq.
In Type Theory we can define coinductively not just single types, but family of types, predicates and relations.
This leads to a proof technique in which the statement to be proved can be used recursively as long as it satisfies a guardedness conditions.
It amounts to constructing a proof with an infinite number of logical steps.
We can combine coinduction with induction in several ways to define types with a complex internal structure. One example is the definition of all continuous functions between streams.
A further generalization consists in defining a coinductive type simultaneously with a recursive function on it, in the style of induction-recursion.
This leads to a very general notion of Wander types, that can be instantiated to many of the most common type-theoretic constructions.
First lecture
Second lecture
Third lecture
Fourth lecture
Code1
Code2
Code3
Code4
-
Brian Logan: Multi-agent programming
Multi-agent programming
Multi-agent programming is an approach to the development of large, heterogeneous open systems. In a multi-agent system (MAS), individual agents can join and leave the system at run time and interact through a shared environment by performing actions. Each agent has a set of objectives, and agents select actions or sequences of actions that will achieve their objectives. Programming languages and frameworks for the development of MAS are often defined in terms of intentional and normative concepts such as beliefs, goals, intentions, obligations and prohibitions, etc. and relationships between such concepts. This course will survey some of the key approaches in multi-agent programming including the Belief-Desire-Intention model of individual agents and normative models for multi-agent organisations. In addition, we shall explore the deep connections between multi-agent programming languages and (multi-)agent logics, including epistemic logics, logics of action, dynamic logic, coalition logics etc., and the application of such logical techniques to address key practical issues such as the verification of (multi-)agent programs.
First lecture
Second lecture
Third lecture
Fourth lecture
Handouts
Exercises
-
Uday Reddy: Category Theory
Category Theory for Computer Scientists
This course covers the basic concepts of category theory in relation to
Computer Science. The essential view point is that category theory is a
"type theory" in an abstract sense. Functors are type constructors and
natural transformations are polymorphic functions. Adjunctions, the central
topic of the course, represent an "inheritance" framework for types with
structure. We cover both formal (syntactic) and semantic aspects of the
theory so that it has applications to programming as well as program
semantics.
Lecture Notes.
-
Philip Wadler: Topics
in Lambda Calculus and Life
Synopsis: Five talks will cover a range of topics:
|
|
