Induction proof of alpha-beta search

Is there a functional specification of alpha-beta search that makes it easy to prove by induction that the algorithm works?

Let's start with ordinary minimax evaluation. If you are trying to evaluate position $p$ when it's the minimizing player's turn, you return $\min\{\operatorname{eval}(p',\text{max}) \mid p'\text{ successor of }p\}$.
To do tree pruning you change what $\operatorname{eval}(p',\text{max})$ does. Instead of returning a single value, it streams messages to you. Messages like "my final value will be at greater than 3", "my value will be greater than 20", "my value is 23". If the minimizer already got a message saying that one successor $p'$ has has value $5$, and it gets a message from $\text{eval}(p'',\text{max})$ saying that its value will be at least $10$ then the minimizer will close the channel with $\text{eval}(p'',\text{max})$.