Interactive Models of Logic and Computation
Samson Abramsky
Oxford University Computing Laboratory
Wolfson Building, Parks Road
Oxford OX1 3QD
U.K.
(samson@comlab.ox.ac.uk)
Prerequisites: Basic knowledge of logic and discrete mathematics.
Some familiarity with lambda-notation would be useful, but not
essential.
Summary: We begin with a brief introduction (or review for those already familiar
with this material) of Natural deduction, Simply typed lambda calculus,
and the Curry-Howard correspondence. We then give a gentle first
introduction to some basic ideas of Linear Logic.
Attention then turns to interactive models of logical and computational
systems, in which proofs (or programs) are modelled as *strategies*,
i.e. processes which interact with their environment.This is a
fundamental and pervasive point of view, which opens up some new
perspectives on proof theory, complexity, and program semantics and
verification.
Both theoretical results (full abstraction and full completeness) and
applications to model checking and program analysis will be described.
Course Notes:
Lecture Notes on Curry-Howard Correspondence and Linear Logic
Lecture Notes on Game Semantics
Exercises to Accompany the Lecture Notes
Back to course listing.