Search

• < Previous
• 1
• Next >

---

Logical Reasoning for Higher-Order Functions with Local State

Nobuko Yoshida ; Kohei Honda ; Martin Berger.

We introduce an extension of Hoare logic for call-by-value 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.&nbsp;[&hellip;]

---

Program Logics for Homogeneous Generative Run-Time Meta-Programming

Martin Berger ; Laurence Tratt.

This paper provides the first program logic for homogeneous generative run-time meta-programming---using a variant of MiniML by Davies and Pfenning as its underlying meta-programming language. We show the applicability of our approach by reasoning about example meta-programs from the literature. We&nbsp;[&hellip;]

---