LLM-assisted mechanized metatheory for act

[zoep]

Rocq mechanization of the Act metatheory, following the pen-and-paper formalization in our tech report. The formalization was ported to Rocq using Claude Code (with Opus 4.6) and human guidance.

What's included

• Syntax: types, expressions, references, and top-level constructs (contracts, constructors, transitions)
• Semantic domains: values, store, state, and environments for pointer semantics
• Big-step operational semantics for pointer semantics
• Type system: typing judgments for all syntactic categories (references, expressions, mappings, slots, creates,
  updates, constructors, transitions, contracts)
• Type safety: type preservation and progress for all syntactic categories
• Value semantics and soundness (WIP): denotational value semantics and its soundness w.r.t. pointer semantics