![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
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 StateAdd 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. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsEmpowered Voices Year Newnham College MCR Speaker Series CamPoS (Cambridge Philosophy of Science) seminarOther talksA novel aspect of Macrophage biology: learning from the great opportunist HIV-1 Giant response of weakly driven systems Immigration policy-making beyond 'Western liberal democracies' Systems for Big Data Applications:Revolutionising personal computing An intellectual history of the universal basic income Assessing the Impact of Open IP in Emerging Technologies |