Hoare logic with explicit contexts

M.G.J. Franssen

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureHoofdstukAcademicpeer review

Samenvatting

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.
Originele taal-2Engels
TitelThirty five years of automating mathematics
RedacteurenF.D. Kamareddine
Plaats van productieDordrecht
UitgeverijKluwer Academic Publishers
Pagina's125-148
ISBN van geprinte versie978-1-4020-1656-5
StatusGepubliceerd - 2003

Publicatie series

NaamApplied Logic Series
Volume28
ISSN van geprinte versie1386-2790

Vingerafdruk

Duik in de onderzoeksthema's van 'Hoare logic with explicit contexts'. Samen vormen ze een unieke vingerafdruk.

Citeer dit