Pico (Rocq) — Alectryon Docs

Rendered Rocq sources for the Pico language mechanization.

Foundations

• LibTactics
• Tactics
• Syntax
• Notations
• Helpers

Type system

• ViewpointAdaptation
• Subtyping
• Typing

Runtime

• Reachability
• Bigstep
• Properties

Capability history

• ExecutionConfinement
• MutableCapability
• AuthorityCapability
• ProtectionHistory
• ComponentColoring
• ForwardCapabilityHistory
• AuthorityHistory
• WatchedFrames
• LiveCapabilityStack
• PotentialCapability
• ProtectedFieldPreservation

Soundness

• Preservation

Immutability

• AbstractStatePreservation
• ConcreteState
• ConcreteStatePreservation
• TransitiveStatePreservation

Readonly

• ReadonlyHelper
• ReadonlyNoMutation
• ReadonlyStatePreservation

Mutation safety

• WFNOMutationEXP