Post-Doctoral Research Position at Glasgow

There is a post-doctoral research position for two years in the
Department of Computing Science at Glasgow University to work on the
project Efficient Programming in Classical Logic.

The researcher must be very competent in theory and implementation. 

The researcher will be working within the BeaUTy (Better and Ultimate Types) 

The post is funded by EPSRC and is on the RA 1A salary scale. 

The goals of the project are: 

    1.Improving reasoning about control using classical logic by combining 
	control operators with new notions of reduction and rewriting, 
	concentrating on the important questions of termination, confluence, 
	subject reduction and typing. In particular, we hope to develop general
       	results describing the termination of languages with control operators.
	We believe that using classical logic in combination with new methods 
	of reasoning about reduction will lead to more general results. 
    2.Relating classical logic to other paradigms. Using a control operator to 
	describe the computational meaning of a classical axiom is only the 
	first step in exploiting classical logic in general. We believe that 
	nondeterminism is a strength of the general system since it allows
        for parallelism, and we intend to study the problem in this context. 
	Especially, this is related to the introduction and use of the new 
	reduction strategies and explicit rewriting and substitutions to 
	represent laziness, parallelism and concurrency. 
    3.Using classical logic as a descriptive tool. The theories developed 
	under the first two goals will also be studied from more practical 
	sides. For example, the use of the foundationally sound theories of 
	control that are precisely written using explicit rewriting and typing
	can be used to improve the efficiency of the search of proofs in 
	theorem proving. This will be studied within the theorem-proving 
	expertise of the BeaUTy group. 
    4.Prototype implementation of program extraction from proofs. In order to 
	demonstrate the practicality of program extraction from classical 
	proof, we will develop prototype implementations of tools for program 
	development. We expect to use existing theorem proving technology and 
	especially the active research of the BeaUTy team writing explicit
       theories of proofs and programs as much as possible for this aspect of 
	the implementation. 

Further descriptions of the project and the group can be found at

Interested candidates should submit their c.v. and forward three letters of 
reference to one of the following addresses. 
          Dr. Fairouz Kamareddine
          University of Glasgow
          Department of Computer Science
          17 Lilybank Gardens
          G12 8QQ
          Dr. Fairouz Kamareddine <fairouz@dcs.gla.ac.uk>