Lambda the Ultimate

A simple class of Kripke-style models in which logic and computation have equal standing, Michael and Murdoch Gabbay, LPAR 2010:

We present a sound and complete model of lambda-calculus reductions based on structures inspired by modal logic (closely related to Kripke structures). Accordingly we can construct a logic which is sound and complete for the same models, and we identify lambda-terms with certain simple sentences (predicates) in this logic, by direct compositional translation. Reduction then becomes identified with logical entailment.