University of Birmingham > Talks@bham > Theoretical computer science seminar > Imperative Programs as Proofs via Game Semantics

## Imperative Programs as Proofs via Game SemanticsAdd to your list(s) Download to your calendar using vCal - Martin Churchill, University of Bath
- Friday 08 July 2011, 16:00-17:00
- UG40 Computer Science.
If you have a question about this talk, please contact Paul Levy. 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. We describe a logical counterpart to this extension, in which proofs denote such strategies. We can embed intuitionistic first-order linear logic into this system, as well as an imperative total programming language. The logic makes explicit use of the fact that in the game semantics the exponential can be expressed as a final coalgebra. We establish a full completeness theorem for our logic, showing that every bounded strategy is the denotation of a proof. This talk is part of the Theoretical computer science seminar series. ## This talk is included in these lists:- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Theoretical computer science seminar
- UG40 Computer Science
- computer sience
Note that ex-directory lists are not shown. |
## Other listsCond. Mat. seminar Type the title of a new list here Astrophysics Talks Series## Other talksTBA The tragic destiny of Mileva Marić Einstein Ultrafast Spectroscopy and Microscopy as probes of Energy Materials Wave turbulence in the Schrödinger-Helmholtz equation TBA Life : it’s out there, but what and why ? |