Structure and representation in LF
- 7 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 226-237
- https://doi.org/10.1109/lics.1989.39177
Abstract
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, the authors 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. The authors 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.Keywords
This publication has 13 references indexed in Scilit:
- Generalised algebraic theories and contextual categoriesPublished by Elsevier ,2003
- Elf: a language for logic definition and verified metaprogrammingPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- A framework for defining logicsJournal of the ACM, 1993
- Toward formal development of programs from algebraic specifications: Implementations revisitedActa Informatica, 1988
- Extended ML: An institution-independent framework for formal program developmentPublished by Springer Nature ,1986
- Program specification and development in standard MLPublished by Association for Computing Machinery (ACM) ,1985
- Introducing institutionsPublished by Springer Nature ,1984
- Structured theories in LCFPublished by Springer Nature ,1983
- Completeness of many-sorted equational logicACM SIGPLAN Notices, 1981
- The semantics of clear, a specification languagePublished by Springer Nature ,1980