Imperative programs as proofs via game semantics
Game semantics extends the Curry-Howard isomorphism to a three-way correspondence: proofs, programs, strategies. But the universe of strategies goes beyond intuitionistic logics and lambda calculus, to capture stateful programs. In this thesis we describe a logical counterpart to this extension, in...
| Main Author: | |
|---|---|
| Other Authors: | |
| Published: |
University of Bath
2011
|
| Subjects: | |
| Online Access: | https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.546658 |