[Prev][Next][Index][Thread]
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)
group.
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
http://www.dcs.gla.ac.uk/research/beauty/.
Interested candidates should submit their c.v. and forward three letters of
reference to one of the following addresses.
Post:
Dr. Fairouz Kamareddine
University of Glasgow
Department of Computer Science
17 Lilybank Gardens
GLASGOW
G12 8QQ
Scotland
E-mail:
Dr. Fairouz Kamareddine <fairouz@dcs.gla.ac.uk>