@INCOLLECTION{MatthewsSmaillBasin,
AUTHOR        = {Sean Matthews and Alan Smaill and David Basin},
TITLE         = {Experience with FS0 as a Framework Theory}, 
EDITOR        = {G. Huet and G. Plotkin},
BOOKTITLE     = {Logical Environments},
PUBLISHER     = {Cambridge University Press},
YEAR          = {1993},
PADDRESS       = {Cambridge, MA},
PAGES         = {61--82},
ABSTRACT      = { 
 Feferman has proposed a system, $FS_0$, as an alternative framework for
encoding logics and also for reasoning about those encodings. We have
implemented a version of this framework and performed experiments that show
that it is practical. Specifically, we describe a formalisation of predicate
calculus and the development of an admissible rule that manipulates formulae
with bound variables. This application will be of interest to researchers
working with frameworks that use mechanisms based on substitution in the
lambda calculus to implement variable binding and substitution in the
declared logic directly. We suggest that meta-theoretic reasoning, even for
a theory using bound variables, is not as difficult as is often supposed,
and leads to more powerful ways of reasoning about the encoded theory. },
}