Programming interfaces and basic topology

Annals of Pure and Applied Logic 137 (1--3):189-239 (2006)

Abstract
A pattern of interaction that arises again and again in programming is a 'handshake', in which two agents exchange data. The exchange is thought of as provision of a service. Each interaction is initiated by a specific agent--the client or Angel--and concluded by the other--the server or Demon. We present a category in which the objects--called interaction structures in the paper--serve as descriptions of services provided across such handshaken interfaces. The morphisms--called (general) simulations--model components that provide one such service, relying on another. The morphisms are relations between the underlying sets of the interaction structures. The proof that a relation is a simulation can serve (in principle) as an executable program, whose specification is that it provides the service described by its domain, given an implementation of the service described by its codomain. This category is then shown to coincide with the subcategory of 'generated' basic topologies in Sambin's terminology, where a basic topology is given by a closure operator whose induced sup-lattice structure need not be distributive; and moreover, this operator is inductively generated from a basic cover relation. This coincidence provides topologists with a natural source of examples for non-distributive formal topology. It raises a number of questions of interest both for formal topology and programming. The extra structure needed to make such a basic topology into a real formal topology is then interpreted in the context of interaction structures
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/j.apal.2005.05.022
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 38,992
Through your library

References found in this work BETA

Inductively Generated Formal Topologies.Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini - 2003 - Annals of Pure and Applied Logic 124 (1-3):71-106.
A Semantics of Evidence for Classical Arithmetic.Thierry Coquand - 1995 - Journal of Symbolic Logic 60 (1):325-337.
Topology Via Logic.P. T. Johnstone & Steven Vickers - 1991 - Journal of Symbolic Logic 56 (3):1101.
The Problem of the Formalization of Constructive Topology.Silvio Valentini - 2004 - Archive for Mathematical Logic 44 (1):115-129.

View all 6 references / Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Sublocales in Formal Topology.Steven Vickers - 2007 - Journal of Symbolic Logic 72 (2):463 - 482.
Philosophical Topology.Yi Jiang - 2008 - Proceedings of the Xxii World Congress of Philosophy 15:59-74.
On the Formal Points of the Formal Topology of the Binary Tree.Silvio Valentini - 2002 - Archive for Mathematical Logic 41 (7):603-618.
Type-Definable and Invariant Groups in O-Minimal Structures.Jana Maříková - 2007 - Journal of Symbolic Logic 72 (1):67 - 80.
Zeeman-Göbel Topologies.Adrian Heathcote - 1988 - British Journal for the Philosophy of Science 39 (2):247-261.

Analytics

Added to PP index
2013-12-22

Total views
21 ( #347,892 of 2,319,688 )

Recent downloads (6 months)
19 ( #33,517 of 2,319,688 )

How can I increase my downloads?

Monthly downloads

My notes

Sign in to use this feature