Guide to Papers: Logics and Semantics of Computation

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.

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.

here

Two-Lambda-Calculus:

Towards a Proof Theory of Rewriting: The Simply-Typed 2-lambda-Calculus
Barnaby P. Hilken

This paper describes the simply-typed 2-lambda-calculus, a language with three levels: types, terms and rewrites. The types and terms are those of the simply-typed lambda-calculus, and the rewrites are expressions denoting sequences of beta-reductions and eta-expansions. An equational theory is imposed on the rewrites, based on 2-categorical 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 long-beta\eta-normal 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.

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 cut-eliminination result for this calculus. For comparison, a presentation of a classical modal logic in sequent style is given along with its semantics.

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.

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, relation-preserving functions into the space, and the relational sections of a relational bundle are defined as relation-preserving 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 quasi-topos and hence models first order logic with modalities.

here

p-Frames:

Topological Duality for Intuitionistic Modal Algebras II: p-Frames
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 `p-frames'. p-frames 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.

here

Contact the Website Administrator with comments or queries about this website.
All material copyright ©The University of Manchester. Last update Jan 2007.