PhD course in Specifying and Reasoning About Computational System

Title:
Specifying and Reasoning About Computational Systems

Organizer: Gopalan Nadathur

Lecturer: Gopalan Nadathur

Course description:
We will introduce a logical approach to specifying, prototyping and
reasoning about formal systems that are presented via syntax-directed
rules. This style of description includes, for example, the typical
presentation of typing and evaluation relations for programming
languages, proof systems for varied logics, software modelling
languages and software specifications, and process calculi and
encodings of concurrent systems. Many of these systems characterize
relations over syntactic objects that involve binding, a notion whose
correct treatment in specification and reasoning tasks has proven to
be surprisingly tricky. The first part of the course will expose a
specification language based on a higher-order logic that provides a
natural and effective means for formalizing such systems. This part
will also develop the proof-theoretic and computational properties of
the specification language that allows it to be used also as a means
for programming and prototyping. The second part of the course will
consider logics for reasoning about formalizations in the
specification language. Such logics must internalize the "closed
world" assumption inherent to specifications and should support
reasoning principles such as induction. We will develop a treatment of
such aspects and will also discuss mechanisms for reasoning
effectively in the presence of binding notions. Finally, we will
understand the two-level logic approach that smoothly integrates
specification, prototyping and reasoning and also allows
meta-theoretic properties of the specification logic to be used to
advantage. Implementations of the specification and reasoning logics
in the form of the Teyjus, Bedwyr and Abella systems will be used to
provide concreteness to the foundational and methodological
discussions.

Program:
A tentative schedule for the lectures is the following:

Lecture 1: Relational Specifications, Foundations of Logic
Programming. Motivation for logic programming in formal
specification, desiderata. Sequent calculus based formulation of logic
programming, first-order Horn clauses and hereditarily Harrop
formulas.

Lecture 2. Higher-Order Logic Programming. A logic over the lambda
calculus, the need for typing, Church's higher-order logic (Simple
Theory of Types), predicate variables and proof search, higher-order
hereditary Harrop formulas, programming in hohh, higher-order abstract
about:blank 1 of 3 19-03-2012 09:12 syntax, introduction to Lambda Prolog.

Lecture 3. Higher-Order Unification. Unification described as equation
solving under a mixed prefix of quantifiers, raising and
Skolemization, complexity of higher-order unification, Huet's
procedure for general higher-order unification, motivation for
higher-order pattern unification and its properties and realization.

Lecture 4. Case studies in specification. Extended examples
illustrating the use of higher-order abstract syntax and logic
programming a la Lambda Prolog in encoding proof systems, process
calculi, evaluation and typing for programming languages, and other
related formal systems.

Lecture 5. Design of a logic for reasoning about specifications.
Motivation for reasoning through specifications via simple examples
such as subject reduction for lambda calculus, identification of
logical properties needed, logic of fixed-point definitions as a means
for encoding specifications.

Lecture 6. Continued development of a logic of definitions. Treatment
of induction and co-induction, the need for generic quantification,
the nabla quantifier, nominal abstraction for analysis of contexts,
issues related to adequacy of encoding, further developments such as
the addition of rewriting for encoding recursive definitions.

Lecture 7. Reasoning based on the logic of definitions. Model checking
oriented reasoning about finite behavior via a generalized logic
programming interpreter, the Bedwyr system and example
applications. Two level approach to reasoning about specifications,
the Abella system.

Lecture 8. Reasoning based on the logic of definitions
(continued). More on the two level style of reasoning, exploiting
meta-theoretic properties of the specification logic, case studies
using the Abella system, issues related to realizing proof search.
Sources for the material to be covered:

The first half of the course will be based on a forthcoming book:
Programming with Higher Order Logic by Dale Miller and Gopalan
Nadathur. Drafts of relevant portions of the book will be provided in
hard copy form. The book will be out in print on May 31 - see here - and
students in the course wishing to own a copy can avail of a discount
voucher from Cambridge University Press.

The second half of the course will be based on doctoral theses by
David Baelde, Andrew Gacek, Ray McDowell, Alwen Tiu and recent
research papers involving these individuals and Dale Miller and
Gopalan Nadathur. Particular articles and portions of the theses that
are especially important to read for the course will be announced
through the web page at a time closer to the coverage of the
material.

The course will also involve the use of the Bedwyr, Abella and Teyjus
systems. These can be downloaded over the internet.

Will you create your own course website? Yes.
http://www.cs.umn.edu/~gopalan/courses/ITU-2012

Dates of the course:
April 23 - June 11 (8 weeks)

Location: Room 3A20 June 4 and June 11 - both days the lecture will take place from 9-12.

Time: (one lecture each week, two hours in duration)

Exam: There will be no formal exams, evaluation will be based on class
participation.

Credits: 5 ECTS

Availiable spaces: About 10-15 participants