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:




Library Locked Library locked




Author, Editor
Author(s):
Matthews, Seán
Smaill, Alan
Basin, David A.		dblp
dblp
dblp
Editor(s):
Huet, G.
Plotkin, G.		dblp
dblp

BibTeX cite key*:

MatthewsSmaillBasin93a

Title, Booktitle

Title*:

Experience with {$FS_0$} as a Framework Theory

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*:

61-82

Month:


VG Wort Pages:


ISBN:


Year*:

1993

Abstract, Links, ©

Note:

Also available as Technical Report {MPI-I-92-214}

LaTeX Abstract:

Feferman has proposed a system, ${FS_0}$, as an alternative framework for encoding logics and also for reasoning about those encodings. We have implemented a version of this framework and performed experiments that show that it is practical. Specifically, we describe a formalisation of predicate calculus and the development of an admissible rule that manipulates formulae with bound variables. This application will be of interest to researchers working with frameworks that use mechanisms based on substitution in the lambda calculus to implement variable binding and substitution in the declared logic directly. We suggest that meta-theoretic reasoning, even for a theory using bound variables, is not as difficult as is often supposed, and leads to more powerful ways of reasoning about the encoded theory.

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{MatthewsSmaillBasin93a,
AUTHOR = {Matthews, Se{\'a}n and Smaill, Alan and Basin, David A.},
 EDITOR = {Huet, G. and Plotkin, G.},
 TITLE = {Experience with {$FS_0$} as a Framework Theory},
 BOOKTITLE = {Logical Environments},
 PUBLISHER = {Cambridge University Press},
 YEAR = {1993},
 PAGES = {61--82},
 ADDRESS = {Cambridge, UK},
 NOTE = {Also available as Technical Report {MPI-I-92-214}},
}

Entry last modified by Christine Kiesel, 08/29/2014
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)
[Library]		Created
01/14/1995 06:52:20 PM
Revisions
5.
4.
3.
2.
1.		Editor(s)
Christine Kiesel
Christine Kiesel/AG2/MPII/DE
Uwe Brahm/MPII/DE
Uwe Brahm/MPII/DE
Uwe Brahm/MPII/DE		Edit Dates
28.08.2001 15:27:06
14/02/95 14:26:32
21/01/95 20:53:53
17/01/95 17:45:53
17/01/95 17:45:26