Part, Chapter of a Book @InBook, Buchkapitel Beitrag im Sammelband

 Show entries of: this year (2019) | last year (2018) | two years ago (2017) | Notes URL
 Action: login to update Options: Goto entry point

 Author, Editor
 Author(s): Basin, David A. Constable, Robert L. dblp dblp
 Editor(s): Huet, Gérard Plotkin, Gordon dblp dblp
 BibTeX cite key*: Basin93a

 Title, Booktitle
 Title*: Metalogical Frameworks Booktitle*: Logical Environments Chapter: Series: Language: English

 Publisher
 Name*: Cambridge University Press URL: Address*: Cambridge, UK Publication Type:

 Vol, No, pp., Year
 Volume: Number: Edition: Pages*: 1-29 Month: VG Wort Pages: ISBN: Year*: 1993

 Note: Also available as Research Report MPI-I-92-205 LaTeX Abstract: In computer science we speak of {\em implementing\/} a logic; this is done in a programming language, such as Lisp, called here the {\em implementation language}. We also reason about the logic, as in understanding how to search for proofs; these arguments are expressed in the {\em metalanguage\/} and conducted in the {\em metalogic\/} of the {\em object language\/} being implemented. We also reason about the implementation itself, say to know it is correct; this is done in a {\em programming logic\/}. How do all these logics relate? This paper considers that question and more. We show that by taking the view that the metalogic is primary, these other parts are related in standard ways. The metalogic should be suitably rich so that the object logic can be presented as an abstract data type, and it must be suitably computational (or constructive) so that an instance of that type is an implementation. The data type abstractly encodes all that is relevant for metareasoning, i.e., not only the term constructing functions but also the principles for reasoning about terms and computing with them. Our work can also be seen as an approach to the task of finding a generic way to present logics and their implementations, which is for example the goal of the Edinburgh Logical Frameworks (ELF) effort. This approach extends well beyond proof-construction and includes computational metatheory as well. URL Abstract: Tags, Keywords: Copyright Message: HyperLinks / References / URLs: Personal Comments: Download Access Level:

 Correlation
 MPG Unit: Max-Planck-Institut für Informatik MPG Subunit: Programming Logics Group Audience: experts only Appearance:
BibTeX Entry:
@INBOOK{Basin93a,
AUTHOR = {Basin, David A. and Constable, Robert L.},
EDITOR = {Huet, G{\'e}rard and Plotkin, Gordon},
TITLE = {Metalogical Frameworks},
BOOKTITLE = {Logical Environments},
PUBLISHER = {Cambridge University Press},
YEAR = {1993},
PAGES = {1--29},