A formal proof of the Chip Model Channel Separation Property
Thomas Hallgren,
Talk at the Programatica Review Meeting, 2004-09-16
A formal proof of the Chip Model Channel Separation Property
The Chip
Proof of the separation property
The Chip Model in Haskell
Channel Separation Property in P-logic
Alternative view of the Channel Separation Property
Filling in the details
The Chip Model in Haskell, more details
For reference...
An observation
Overall proof structure
Observations
CondSeparation proof outline
AllGoodAlg proof outline
Proof effort
Proof size
Relevance to current work
The End
References