University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Logical Reasoning for Higher-Order Functions with Local State

Logical Reasoning for Higher-Order Functions with Local State

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Matthew Parkinson.

This talk presents an extension of Hoare logic for higher-order functions with ML-like local reference generation. Local references may be generated dynamically and exported outside their scope, may store higher-order functions and may be used to construct complex mutable data structures. This primitive is captured logically using a predicate asserting reachability of a reference name from a possibly higher-order datum and quantifiers over hidden references.

We explore the logic’s descriptive and reasoning power with non-trivial programming examples combining higher-order procedures and dynamically generated local state. Axioms for reachability and local invariant play a central role for reasoning about the examples.

The logic enjoys the three completeness properties: relative completeness, a logical characterisation of the contextual congruence and derivability of characteristic formulae.

Joint work with Kohei Honda and Martin Berger.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity