A constructive logic for services and information flow in computer networks

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