Coding Binding and Substitution Explicitly
			     in Isabelle

			  Christopher Owens


			       Abstract


Logical frameworks provide powerful methods of encoding object-logical
binding and substitution using meta-logical lambda abstraction and
application.  However, there are some cases in which these methods are
not general enough: in such cases object-logical binding and
substitution must be explicitly coded.  McKinna and Pollack [MP93]
give a novel formalization of binding, but use it principally to prove
meta-theorems of Type Theory.  We analyse the practical use of
McKinna-Pollack binding in Isabelle object-logics, and illustrate its
use with a simple example logic.


References

[MP93] James McKinna and Robert Pollack.  Pure type systems formalized.
       In M. Bezem and J.F. Groote, editors, Proceedings of the International
       Conference on Typed Lambda Calculi and Applications, TLCA'93, num-
       ber 664 in Lecture Notes in Computer Science, pages 289-305.
       Springer-Verlag.