A formal proof of the Chip Model Channel Separation Property

Thomas Hallgren, Programatica Meeting, 2004-05-11

A formal proof of the Chip Model Channel Separation Property
Warning
Encouragement
Remember the Curry-Howard isomorphism?
Automation is always welcome!
The Chip
Channel Separation Property
A variant of the Channel Separation Property
Filling in the details
The Chip Model
For reference...
Observations 1
Observations 2
Observations 3
Overall proof structure
Good algorithms
Invariant in the proof of CondSeparation
CondSeparation proof outline
Invariant in the proof of AllGoodAlg
Invariant in the proof of AllGoodAlg, first attempt
Invariant in the proof of AllGoodAlg, degeneralized
AllGoodAlg proof outline
Files
Imports from the Alfa library and other utilities
Random notes and concluding remarks
Pointers
The End
Box drawing tests