This project will investigate the nature of computational systems which are meant to discover proofs and compute with them after they are discovered. The concept of proofs-as-values is not only interesting in its own right but also central for the development of interesting theorem provers and proof assistants for use by mathematicians and computer scientists. As a guide in designing such proof systems, several relevant issues in the semantics of constructive logics and higher-order polymorphic -calculus will be investigated. A clear understanding of such models would help in developing a consistent and clean programming paradigm for the implementation of higher-order proof systems. The project will also investigate the role which extensions of logic programming languages could play as the underlying implementation languages for higher-order proof systems. The central role of search and equation solving (unification) in logic programming may make it more suitable for the implementation of proof systems than more traditionally used languages such as ML.
