Linear logic in computer science

Linear logic has many properties that make it suitable for application in various areas of computer science. It is able to describe dynamic processes, non-determinism, parallelism on syntactic level. In our paper we try to discuss resource oriented character of linear logic, its possibility to deal with such important resources for computer science as space (memory) and time. Handling with resources takes place in deduction system of linear logic. We show how special form of proofs, called designs, is constructed and we show the relationship between space and time in designs.