A constructive logic for services and information flow in computer networks

V.A.J. Borghuis, L.M.G. Feijs

Research output: Contribution to journalArticleAcademicpeer-review

8 Citations (Scopus)

Abstract

In this paper we introduce a typed -calculus in which computer networks can be formalized and directed at situations where the services available on the network are stationary, while the information can flow freely. For this calculus, an analogue of the ‘propositions-as-types ’interpretation of constructive type theory holds with respect to information push and pull in computer networks: in the calculus a type represents a task that the user wants to carry out, while a term inhabiting this type represents a procedure that will yield the desired result. Under this interpretation, techniques for theorem proving can be used for finding a procedure to achieve a certain task on the network. Techniques for type checking can be used for checking a complex network program before running it. Reductions on terms can be used for finding alternative procedures to achieve a certain task. Terms constructed in this abstract calculus can be ‘compiled ’to procedures which are executable on the actual network. We show this for a simple Unix network.
Original languageEnglish
Pages (from-to)274-289
Number of pages16
JournalThe Computer Journal
Volume43
Issue number4
DOIs
Publication statusPublished - 2000

Fingerprint Dive into the research topics of 'A constructive logic for services and information flow in computer networks'. Together they form a unique fingerprint.

Cite this