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

10 Citations (Scopus)


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
Issue number4
Publication statusPublished - 2000


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