Rocq proof artifact
Pico Rocq Mechanization
A mechanized formalization of the Pico core calculus for transitive, abstract, and class polymorphic immutability.
Verification command
make check
Proof gaps
No forbidden
Axiom, Admitted, or admit usage
Rendered docs
Alectryon pages are generated under
site/proofs/
Paper-to-Proof Map
| Paper item | Rocq entry point | File |
|---|---|---|
| Syntax, runtime values, heaps | q, stmt, method_sig, Obj |
Syntax.v |
| Viewpoint adaptation | vpa_mutability_tt_abs_imm, vpa_assignability |
ViewpointAdaptation.v |
| Static typing | stmt_typing, wf_method, wf_class_table |
Typing.v |
| Operational semantics | eval_expr, eval_stmt |
Bigstep.v |
| Theorem 1: preservation | preservation_pico |
Preservation.v |
| Theorems 2 and 3: abstract immutability | shallow_immutability_pico, deep_immutability_pico |
DeepImmutability.v |
| Theorem 4: safe readonly | readonly_method_call_preserves_arguments |
ReadonlySafety.v |
| Theorem 5: concrete immutability | ConcreteImmutability |
ConcreteImmutability.v |
Proof Organization
- Subtyping.v defines qualifier, base, method, and qualified-type subtyping.
- Reachability.v defines ordinary and abstract-state reachability.
- Properties.v contains preservation support lemmas.
- WFNOMutationEXP.v proves mutation-exception safety.
Local Workflow
make check
make site
open site/index.html
The generated proof pages under site/proofs/ are ignored by git.
The landing page itself is plain static HTML and CSS.