University of Leicester

informatics

Midlands Graduate School

Course Descriptions

  • 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:

Author: Alexander Kurz.
University of Leicester February 2013. Last modified: 15th April 2013, 08:05:36.
Informatics Web Maintainer. This document has been approved by the Head of Department.