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 listsParticle Physics Seminars Bravo Nuclear physics seminars## Other talksThe science of the large scale heliosphere and the missions that made it possible Hidden Markov Model in Multiple Testing on Dependent Data View fusion vis-à-vis a Bayesian interpretation of Black-Litterman for portfolio allocation Energy release and transport in solar eruptive events Plasmonic Electronic Paper Structured Decompositions: recursive data and recursive algorithms |