Academic
Publications
A logical analysis of aliasing for higher-order imperative functions

A logical analysis of aliasing for higher-order imperative functions,Martin Berger,Kohei Honda,Nobuko Yoshida

A logical analysis of aliasing for higher-order imperative functions   (Citations: 9)
BibTex | RIS | RefWorks Download
Cumulative Annual
    • ...Jumps are complementary to the evaluation formulae x� ˜ e� A, studied in [5, 16, 18, 36], which means a jump to x carrying values ˜ e leads to a program state where A holds...
    • ...The present work adds a new member to a family of logics for ML-like languages [5, 16, 18, 36], and integrates in a strong sense: e.g...

    Martin Berger. Program Logics for Sequential Higher-Order Control

    • ...Our aim is to identify basic logical primitives needed to capture precisely the semantics of local state, on the basis of a stratification of logics for sequential higher-order functions in our preceding works [2,10,12,13]...
    • ...It extends the logic [2] with two new primitives...
    • ...!e denotes the dereference of a reference e. Formulae include standard logical connectives and first-order quantifiers [17], and following [2,12], quantification over type variables...
    • ...is universal content quantification, introduced in [2] for treating aliasing...
    • ...The located assertion introduced in [2] is used for this purpose: {C}e•e0 =x{C0}@˜e where each ei is of a reference type and does not contain a...
    • ...The full compositional proof rules are given in Appendix A. Despite our semantic enrichment, all compositional proof rules in [2] syntactically stay as they are, except for adding the following rule for reference generation, with fresh i,X:...
    • ...However from the general invariance rule [Inv] from [2] below (on the left), which uses the located form of judgement {C} M :u {C0}@˜e (understood as located evaluation formulae), we can derive an invariance rule for #, [Inv-#]...
    • ...For the sake of space, detailed comparisons with existing program logics and reasoning methods, in particular with Clarke’s impossibility result, Caires-Cardelli’s spatial logic, recent mechanisations of reachability predicates [16], as well as other logics such as LCF, Dynamic logic, higher-order logic, specification logic, Larch/ML, and Extended ML are left to the long version [1] and our past papers [2,10,12,13]...
    • ...The logic studied in the present work aims to capture the behaviour of sequential higher-order programs with local state in the framework of compositional program logics ` a la Hoare, stratified on the basis of simpler program logics [2,10,12,13]...

    Nobuko Yoshidaet al. Logical Reasoning for Higher-Order Functions with Local State

    • ...Details are found in our coming report [8]...

    Kohei Hondaet al. An observationally complete program logic for imperative higher-order ...

    • ...Current research on closures [14,15,3,16,29,24,19] in imperative programming languages is using higher-order logic...
    • ...The most comprehensive framework for dealing with imperative higher-order language features is that of Yoshida, Honda and Berger [14,15,3,16,29], a total correctness Hoare-logic based framework...

    Ioannis T. Kassioset al. Specification and Verification of Closures

    • ...Such constructs include various atomic operations, structured message passing, objects and higher-order functions (for which we can use the embedding of the logics studied in [10,32,55]), unifying their treatment on a common mathematical foundation...

    Kohei Hondaet al. A Unified Theory of Program Logics: AnApproachbasedonthep-Calculus

Sort by: