Abstract. We claim that a continuation style semantics of a programming language can provide a starting point for constructing its proof system. The basic idea is to see weakest preconditions as a particular instance of continuation style semantics, hence to interpret correctness assertions (e.g. Hoare triples { p } C { r }) as inequalities over continuations. This approach also shows a correspondence between labels in a program and annotations.

A typed framework for working with nonterminating computations is provided. The basic system is the calculus of constructions. It is extended using an original idea proposed by R. Constable and S.F. Smith (2nd Ann. IEEE Conf. on Logic in Comput. Sci., 1987) and implemented in Nuprl. From the computational point of view, an equivalent of the Kleene theorem for partial recursive functions over the integers within an index-free setting is obtained. A larger class of algebraic types is defined. Logical aspects need more examination, but a syntactic method for dealing with partial and total objects, leading to the notion of generic proof, is provided.>