A Modular Hierarchy of Logical Frameworks. / Adams, Robin.

2004. 254 p.

Research output: ThesisDoctoral Thesis

Unpublished

Standard

A Modular Hierarchy of Logical Frameworks. / Adams, Robin.

2004. 254 p.

Research output: ThesisDoctoral Thesis

Harvard

Adams, R 2004, 'A Modular Hierarchy of Logical Frameworks', PhD, University of Manchester.

APA

Vancouver

Author

BibTeX

@phdthesis{24696b101cc04e32b4ad6ee59d5e3224,
title = "A Modular Hierarchy of Logical Frameworks",
abstract = "Logical frameworks - formal systems for the specification and representation of other formal systems - are now a well-established field of research, and the number and variety of logical frameworks is large and growing continuously. In this thesis, I tie several examples of logical frameworks into a single hierarchy.I begin by introducing an infinite family of new, weak, lambda-free logical frameworks. These systems do not use lambda-abstraction, local definition, or any similar feature; parameterisation, and the instantiation of parameterisation, is taken as basic. These frameworks form conservative extensions of one another; this structure of extension is what I call the modular hierarchy of logical frameworks.I show how several examples of existing logical frameworks - specifically, the systems PAL and AUT-68 from the AUTOMATH family, the Edinburgh Logical Framework, Martin-Lof's Logical Framework, and Luo's system PAL+ - can be fitted into this hierarchy, in the sense that one of the weak frameworks can be embedded in each as a conservative subsystem. I give several examples of adequacy theorems for object theories in the weak frameworks; these theorems are easier to prove than is usually the case for a logical framework. Adequacy theorems for the systems higher in the hierarchy follow as immediate corollaries.In the second part of this thesis, I investigate an approach to the design of logical frameworks suggested by the existence of such a hierarchy: that a framework could be built by specifying a set of features, the result of adding any of which to a framework is a conservative extension of the same. I show how all of the weak frameworks from the first part, as well as two of the systems we gave there as examples, can indeed be built in this manner.",
author = "Robin Adams",
year = "2004",
language = "English",
school = "University of Manchester",

}

RIS

TY - THES

T1 - A Modular Hierarchy of Logical Frameworks

AU - Adams, Robin

PY - 2004

Y1 - 2004

N2 - Logical frameworks - formal systems for the specification and representation of other formal systems - are now a well-established field of research, and the number and variety of logical frameworks is large and growing continuously. In this thesis, I tie several examples of logical frameworks into a single hierarchy.I begin by introducing an infinite family of new, weak, lambda-free logical frameworks. These systems do not use lambda-abstraction, local definition, or any similar feature; parameterisation, and the instantiation of parameterisation, is taken as basic. These frameworks form conservative extensions of one another; this structure of extension is what I call the modular hierarchy of logical frameworks.I show how several examples of existing logical frameworks - specifically, the systems PAL and AUT-68 from the AUTOMATH family, the Edinburgh Logical Framework, Martin-Lof's Logical Framework, and Luo's system PAL+ - can be fitted into this hierarchy, in the sense that one of the weak frameworks can be embedded in each as a conservative subsystem. I give several examples of adequacy theorems for object theories in the weak frameworks; these theorems are easier to prove than is usually the case for a logical framework. Adequacy theorems for the systems higher in the hierarchy follow as immediate corollaries.In the second part of this thesis, I investigate an approach to the design of logical frameworks suggested by the existence of such a hierarchy: that a framework could be built by specifying a set of features, the result of adding any of which to a framework is a conservative extension of the same. I show how all of the weak frameworks from the first part, as well as two of the systems we gave there as examples, can indeed be built in this manner.

AB - Logical frameworks - formal systems for the specification and representation of other formal systems - are now a well-established field of research, and the number and variety of logical frameworks is large and growing continuously. In this thesis, I tie several examples of logical frameworks into a single hierarchy.I begin by introducing an infinite family of new, weak, lambda-free logical frameworks. These systems do not use lambda-abstraction, local definition, or any similar feature; parameterisation, and the instantiation of parameterisation, is taken as basic. These frameworks form conservative extensions of one another; this structure of extension is what I call the modular hierarchy of logical frameworks.I show how several examples of existing logical frameworks - specifically, the systems PAL and AUT-68 from the AUTOMATH family, the Edinburgh Logical Framework, Martin-Lof's Logical Framework, and Luo's system PAL+ - can be fitted into this hierarchy, in the sense that one of the weak frameworks can be embedded in each as a conservative subsystem. I give several examples of adequacy theorems for object theories in the weak frameworks; these theorems are easier to prove than is usually the case for a logical framework. Adequacy theorems for the systems higher in the hierarchy follow as immediate corollaries.In the second part of this thesis, I investigate an approach to the design of logical frameworks suggested by the existence of such a hierarchy: that a framework could be built by specifying a set of features, the result of adding any of which to a framework is a conservative extension of the same. I show how all of the weak frameworks from the first part, as well as two of the systems we gave there as examples, can indeed be built in this manner.

M3 - Doctoral Thesis

ER -