A Modular Hierarchy of Logical Frameworks

Robin Adams

doi:10.1007/978-3-540-24849-1_1

A Modular Hierarchy of Logical Frameworks

Robin Adams

Department of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

87 Downloads (Pure)

Abstract

We present a method for defining logical frameworks as a collection of features which are defined and behave independently of one another. Each feature is a set of grammar clauses and rules of deduction such that the result of adding the feature to a framework is a conservative extension of the framework itself. We show how several existing logical frameworks can be so built, and how several much weaker frameworks defined in this manner are adequate for expressing a wide variety of object logics.

Original language	English
Title of host publication	Types for Proofs and Programs
Editors	Stefano Berardi, Mario Coppo, Ferruccio Damiani
Publisher	Springer
Pages	1-16
Number of pages	16
Volume	3085
ISBN (Print)	3-540-22164-6
DOIs	https://doi.org/10.1007/978-3-540-24849-1_1
Publication status	Published - 2004
Event	TYPES 2003 - Torino, Italy Duration: 30 Apr 2003 → 4 May 2003

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
ISSN (Print)	0302-9743

Conference

Conference	TYPES 2003
Country/Territory	Italy
City	Torino
Period	30/04/03 → 4/05/03

Access to Document

10.1007/978-3-540-24849-1_1

ModhierSubmitted manuscript, 57 KB

Cite this

@inproceedings{2b842adb4beb4963ad4f2de773c13529,

title = "A Modular Hierarchy of Logical Frameworks",

abstract = "We present a method for defining logical frameworks as a collection of features which are defined and behave independently of one another. Each feature is a set of grammar clauses and rules of deduction such that the result of adding the feature to a framework is a conservative extension of the framework itself. We show how several existing logical frameworks can be so built, and how several much weaker frameworks defined in this manner are adequate for expressing a wide variety of object logics.",

author = "Robin Adams",

year = "2004",

doi = "10.1007/978-3-540-24849-1_1",

language = "English",

isbn = "3-540-22164-6",

volume = "3085",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "1--16",

editor = "Stefano Berardi and Mario Coppo and Ferruccio Damiani",

booktitle = "Types for Proofs and Programs",

note = "TYPES 2003 ; Conference date: 30-04-2003 Through 04-05-2003",

}

TY - GEN

T1 - A Modular Hierarchy of Logical Frameworks

AU - Adams, Robin

PY - 2004

Y1 - 2004

N2 - We present a method for defining logical frameworks as a collection of features which are defined and behave independently of one another. Each feature is a set of grammar clauses and rules of deduction such that the result of adding the feature to a framework is a conservative extension of the framework itself. We show how several existing logical frameworks can be so built, and how several much weaker frameworks defined in this manner are adequate for expressing a wide variety of object logics.

AB - We present a method for defining logical frameworks as a collection of features which are defined and behave independently of one another. Each feature is a set of grammar clauses and rules of deduction such that the result of adding the feature to a framework is a conservative extension of the framework itself. We show how several existing logical frameworks can be so built, and how several much weaker frameworks defined in this manner are adequate for expressing a wide variety of object logics.

U2 - 10.1007/978-3-540-24849-1_1

DO - 10.1007/978-3-540-24849-1_1

M3 - Conference contribution

SN - 3-540-22164-6

VL - 3085

T3 - Lecture Notes in Computer Science

SP - 1

EP - 16

BT - Types for Proofs and Programs

A2 - Berardi, Stefano

A2 - Coppo, Mario

A2 - Damiani, Ferruccio

PB - Springer

T2 - TYPES 2003

Y2 - 30 April 2003 through 4 May 2003

ER -