David Pym (1W2.35)

1. A Graphical Tool for Proof-nets. 

  Natural deduction proofs are an appealing way to represent 
  formal logical reasoning. The work well, however, only for 
  logics which follow the intuitionistic pattern: consequences 
  are single-conclusioned and negation is not dualizing (i.e.,
  not(not p) is not logically equivalent to p).    

  Proof-nets have been introduced as a natural, and very efficient, 
  representation of proofs in classical logic. 

  In contrast to natural deductions, the drawing, on the page, of 
  proof-nets is a complex activity. This project is to provide a 
  graphical tool for constructing proof-nets for a given logical 
  theorem. 

  The project will develop knowledge and skills mathematical logic, 
  language implementation, and system and interface design. Some 
  starting knowledge of logic/formal proof is necessary. 
  
Look at `Logic for Computer Science', by Reeves and Clarke, published
by Addison Wesley, for background in Natural Deduction.  Look at
`Proofs and Types', by Girard, Lafont and Taylor, published by
Cambridge University Press, for an introduction to proof-nets.

2. A Graphical Tool for Turing Machines.

Suitable for any M.Sc. student with some mathematical background,
skills in programming, and an interest in interfaces.  Turing machines
are a basic model of computation which we teach to all
undergraduates. However, because they perform computations in very
primitive steps, very difficult to design and execute. A possible
M.Sc. project is to implement a graphical tool for designing and
executing Turing machines represented as flow-graphs. Advanced
extensions of the project would include a tool for checking the
correctness of a machine with respect to partial recursive
functions. The project would start with primitive recursive functions.


3. A Graphical Tool for Abacus Machines.

Suitable for any M.Sc. student with some mathematical background,
skills in programming, and an interest in interfaces.  Abacus machines
are a basic model of computation based on the idea of assignment,
increment and decrement for registers. A possible M.Sc. project is to
implement a graphical tool for designing and executing abacus machines
represented as flow-graphs. The project would include a tool for
checking the correctness of a machine with respect to partial
recursive number-theoretic functions. The project would start with
primitive recursive functions.


4. Resource Semantics for Program Logics.  

Suitable for a student with strong mathematical skills.  Starting from
a mathematical model of resources (examples of resources include,
time, space, such as computer memory, and money), it is possible to
give a mathematical semantics to imperative programs. This project
would investigate some possible models of languages with parallel
composition and resource-access constructs. This is foundational,
mathematical project which could form the basis of a PhD project here
at Bath.


5. A range of possible projects in theorem proving and logic programming. 

All require a mix of mathematical and programming skills.  The theory
of resource-distribution provides several possible projects. The basic
idea is this: in order to prove that P is a logical consequence of
assumptions P1, ... , Pn it may be necessary to split up the list 
P1 , ... , P_n into many parts and work on the parts separately. However,
at any give point in our calculation, we may not know how to do the
splitting. The solution is to delay the splitting by maintaining
constraints which are resolved when enough information becomes
available. The result is an elegant and (relatively) efficient
algorithm. For example: (a) Implement a constraint-based resource
distribution algorithm for linear logic; (b) Implement a
constraint-based resource distribution algorithm for bunched logic.
(c) Develop the theory of resource-distribution algorithms to account
for different proof-search strategies.