Several aspects of the relationship between concurrency and proof theory shall be investigated in this project. In particular, theoretical connections between them shall be explored and a programming language based upon the pi-calculus will be designed and implemented using the techniques of logic programming. This should result in both a programming language for the implementation of algorithms centered around concurrency and communication and a logical specification language for the high-level description and analysis of such software.
