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:








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