Help Privacy Policy Disclaimer
  Advanced SearchBrowse




Book Chapter

Experience with FS_0 as a Framework Theory


Matthews,  Seán
Programming Logics, MPI for Informatics, Max Planck Society;


Basin,  David
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available

Matthews, S., Smaill, A., & Basin, D. (1993). Experience with FS_0 as a Framework Theory. In G. Huet, & G. Plotkin (Eds.), Logical Environments (pp. 61-82). Cambridge, UK: Cambridge University Press.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0023-C7FA-3
Feferman has proposed a system, FS_0, as an alternative framework for \u000Aencoding logics and also for reasoning about those encodings. We have \u000Aimplemented a version of this framework and performed experiments that show \u000Athat it is practical. Specifically, we describe a formalisation of predicate \u000Acalculus and the development of an admissible rule that manipulates formulae \u000Awith bound variables. This application will be of interest to researchers \u000Aworking with frameworks that use mechanisms based on substitution in the lambda \u000Acalculus to implement variable binding and substitution in the declared logic \u000Adirectly. We suggest that meta‐theoretic reasoning, even for a theory using \u000Abound variables, is not as difficult as is often supposed, and leads to more \u000Apowerful ways of reasoning about the encoded theory.