Hoare logic with explicit contexts

In this paper, we combine a Hoare logic with a typed ¿-calculus to create a reliable tool for deriving correct programs. In this combined system proofs become part of the programs. The main advantages of our approach are (1) that the Hoare logic conforms to the de Bruijn criterion and hence, can be implemented in reliable way; (2) that the Hoare logic and the typed ¿-calculus co-exist at the same level and therefore programs do not have to be encoded within a theorem prover and (3) scopes of variables are dealt with explicitly using contexts for Hoare triples and hence, the specification language is strictly separated from the programming language