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


Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

login to update
Options:








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

Abstract, Links, ©

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},
 ADDRESS = {?},
}

Entry last modified by Christine Kiesel, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Uwe Brahm		Created
01/14/1995 06:50:42 PM
Revisions
8.
7.
6.
5.
4.		Editor(s)
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel		Edit Dates
28.08.2001 15:26:40
28.08.2001 15:23:43
28.08.2001 15:23:32
28.08.2001 15:23:15
28.08.2001 15:23:05