Challenges

• State the correctness criteria for a memory allocator (the malloc, and free routnines of C). Prove correctness of memory allocator.
• State the correctness criteria for a simple copying garbage collector. Prove correctness of garbage collector.
• Concurrency (and passivity).
• Axiomatizing directed graphs.
• Regions.
• Connections with type systems -- relative pointers.
• Embedding code pointers in data structures (Reynolds currently working on this).
• Higher-order logic and syntactic control of interference.
• Reasoning rules for a language like ML (with immutable variables and updatable references).
• Mechanized checking, model checking.

• Relation to Pitts and Stark's work on Reasoning about Local Names.