Structure and representation in LF

R. Harper, D. Sannella, A. Tarlecki

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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. All inferential activity in an object logic (in particular, proof search) is to be conducted in the logical framework via the representation of that logic in the framework. An important tool for controlling search in an object logic is the use of structured theory presentations. In order to apply these ideas to the setting of a logical framework, we study the behavior of structured theory presentations under representation in a framework, focusing on the problem of "lifting" presentations from the object logic to the metalogic of the framework. We also consider imposing structure on logic presentations so that logical systems may themselves be defined in a modular fashion. This opens the way to a CLEAR-like language for defining both theories and logics in a logical framework.
Original languageEnglish
Title of host publicationLogic in Computer Science, 1989. LICS '89, Proceedings., Fourth Annual Symposium on
Pages226-237
Number of pages12
DOIs
Publication statusPublished - 1 Jun 1989

Fingerprint

Dive into the research topics of 'Structure and representation in LF'. Together they form a unique fingerprint.

Cite this