Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of controlReportar como inadecuado




Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 LACL - Laboratoire d-Algorithmique Complexité et Logique

Abstract : We derive a Floyd-Hoare logic for non-local jumps and mutable higher-order procedural variables from a formulæ-as-types notion of control for classical logic. A key contribution of this work is the design of an imperative dependent type system for Hoare triples, which corresponds to classical logic, but where the famous consequence rule is admissible. Moreover, we prove that this system is complete for a reasonable notion of validity for Hoare judgments.





Autor: Tristan Crolard - Emmanuel Polonowski -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados