Logical concepts and methods are of growing importance in many areas of computer science. The logical notion of a formal proof in various constructive systems can be viewed as a very explicit way to describe a computation procedure.