
Guide to papers
Guide to papers
This page describes papers and working drafts in the Logics and Semantics of Computation.
Papers are available in PDF format.
 Duality:
Topological Duality for Intuitionistic Modal Algebras
Barnaby P. Hilken
This paper describes a generalisation of the adjunction and duality between
topological spaces and frames, inspired by the Kripke semantics of modal logic.
A relational space is defined as a topological space with a binary
relation on the points, and a modal frame is defined as a frame with two
modal operations satisfying various axioms. The frame of open
sets of a relational space has a natural modal structure; with appropriate
morphisms, this extends to a contravariant functor from the category of
relational spaces to the category of modal frames. This paper defines an
adjoint to this functor, and shows that the adjunction restricts to a duality
between the subcategories in the image of the adjunction.
Journal of Pure and Applied Algebra, Vol. 148 pp 171189. 2000.
Paper available in PDF format here.
 Type Classes:
A Theory of Classes: Proofs and Models
Barnaby P. Hilken and David E. Rydeheard
We investigate the proof structure and models of theories of classes, where classes are `collections' of entities. The theories are weaker than set theories and arise from a study of type classes in programming languages, as well as comprehension
schemata in categories. We introduce two languages of proofs, one a simple type theory and the other involving proof environments for storing and retrieving proofs. The relationship between these languages is defined in terms of a normalisation result
for proofs. We use this result to define a categorical semantics for classes and establish its coherence. Finally, we show how the formal systems relate to type classes in programming
languages.
Math. Struct. in Comp. Sci., Vol. 7 pp 95127. 1997.
Paper available in PDF format here.
 TwoLambdaCalculus:
Towards a Proof Theory of Rewriting: The SimplyTyped 2lambdaCalculus
Barnaby P. Hilken
This paper describes the simplytyped 2lambdacalculus, a language
with three levels: types, terms and rewrites. The types
and terms are those of the simplytyped lambdacalculus, and the
rewrites are expressions denoting sequences of betareductions
and etaexpansions. An equational theory is imposed on the rewrites,
based on 2categorical justifications, and the word problem for this
theory is solved by finding a canonical expression in each equivalence class.
The canonical form of rewrites allows us to prove several properties
of the calculus, including a strong form of confluence and a classification
of the longbeta\etanormal forms in terms of their rewrites.
Finally we use these properties as the basic definitions of a theory of
categorical rewriting, and find that the expected relationships between
confluence, strong normalisation and normal forms hold.
Theor. Comp. Sci. Vol. 170, 12, pp 407444. 1996.
Paper available in PDF format here.
 Modal Logic Sequent Calculi:
Semantics and Proof Theory of an Intuitionistic Modal Sequent Calculus M.J. Collinson, B.P. Hilken and D.E. Rydeheard
We prove soundeness and adequacy for an intuitionistic modal sequent calculus
with a modal Heyting algebra semantics. We produce a cuteliminination
result for this calculus. For comparison, a presentation of a classical modal logic in sequent style is given along with its semantics.
Technical Report UMCS9961. June 1999.
Paper available in PDF format here.
 Polymodal Algebra:
Topological Semantics for Intuitionistic Polymodal Algebras
Donald J. MacInnes, Barnaby P. Hilken and David E, Rydeheard
In a recent paper, Hilken presents a generalisation of the adjunction
and duality between frames and topological spaces. This paper describes a
further generalisation of this result by extending the adjunction and duality
to polymodal languages.
Technical Report UMCS0101. Jan 2001.
Paper available in PDF format here.
 Relational Sheaves:
Relational Sheaves and Predicate Intuitionistic Modal Logic
Barnaby P. Hilken
This papers generalises and adapts the theory of sheaves on a topological space to
sheaves on a relational space: a topological space with a binary relation.
Relational bundles on a relational space are defined as continuous, relationpreserving
functions into the space, and the relational sections of a relational bundle are defined as
relationpreserving partial sections. This defines a functor to the category of
presheaves on the space, which has a left adjoint. We define relational sheaves and
set up equivalences of categories, showing that the category of relational sheaves
forms a quasitopos and hence models first order logic with modalities.
Draft paper available in PDF format here.
 pFrames:
Topological Duality for Intuitionistic Modal Algebras II: pFrames
Barnaby P. Hilken
This paper is the second in a series investigating topological structures
arising from the study of modal logic. In the first paper, categories of
relational spaces and modal frames are defined and used to give a sound
and complete semantics of propositional intuitionistic modal logic.
In this paper, we examine the relationship between relational spaces
and modal frames, factorising the link between them by
introducing `pframes'. pframes consist of frames with a(n internal)
binary relation, and are of some independent interest as well as
providing an analysis of the construction of relational spaces
from modal frames.
Draft paper available in PDF format here.
Contact the
Website
Administrator with comments or queries about this website.
All material copyright ŠThe University of Manchester. Last update
Jan 2007.
