ITreeLang & small examples - #1

Open

petrosyh wants to merge 15 commits into

dongjaelee1:mainfrom

Commits on Mar 3, 2026

vibe: ITreeLang
petrosyh
committed
7451e7f
vibe: Imp-ITreeLang finite sim
petrosyh
committed
a77b577

Commits on Mar 4, 2026

vibe: ITree coinduction
petrosyh
committed
1fcd55e
vibe: Imp-ITreeLang sim
petrosyh
committed
9843d48

Commits on Mar 5, 2026

rename
petrosyh
committed
8d5b70a

Commits on Mar 12, 2026

vibe: restructure directories
petrosyh
committed
467a542

Commits on Mar 18, 2026

vibe: mem_handler refinement (WIP)

petrosyh
and
claude
committed
2a96f51
vibe: revert tau from CSeq, add com_size induction for handle_mem

petrosyh
and
claude
committed
4cdfdb8
vibe: mem_handler progress - CSkip/CAsgn/CSeq/CIf/CWhile/CRet working

petrosyh
and
claude
committed
0b7c1e4
WIP: mem_handler - no_aeval_sim helper proved, main theorem Admitted

petrosyh
and
claude
committed
199f121
bsim with claude
petrosyh
committed
66ae689
bsim with claude
petrosyh
committed
4f38231
bsim with claude
petrosyh
committed
981a34f

Commits on Mar 19, 2026

bsim with claude
petrosyh
committed
0dd19a3
bsim with claude
petrosyh
committed
cd29fc3