@inproceedings{8a113d43c93f4939a856864d6900eaa9,
title = "Logic representation in LF",
abstract = "The purpose of a logical framework such as LF is to provide a language for defining logical systems suitable for use in a logic-independent proof development environment. In previous work we have developed a theory of representation of logics in a logical framework and considered the behaviour of structured theory presentations under representation. That work was based on the simplifying assumption that logics are characterized as families of consequence relations on “closed” sentences. In this report we extend the notion of logical system to account for open formula, and study its basic properties. Following standard practice, we distinguish two types of logical system of open formulae that differ in the treatment of free variables, and show how they may be induced from a logical system of closed sentences. The technical notions of a logic presentation and a uniform encoding of a logical system in LF are generalized to the present setting.",
author = "Robert Harper and Donald Sannella and Andrzej Tarlecki",
year = "1989",
doi = "10.1007/BFb0018356",
language = "English",
isbn = "978-3-540-51662-0",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "250--272",
editor = "Pitt, {David H.} and Rydeheard, {David E.} and Peter Dybjer and Pitts, {Andrew M.} and Axel Poign{\'e}",
booktitle = "Category Theory and Computer Science",
address = "United Kingdom",
}