Especificação de sistemas utilizando lógica linear com subexponencias

Abstract

Logic programming is defined as the use of logic formulas representing programs and proof search of these formulas as the execution of the program (computation). This is an interesting paradigm because of the specifications' formality, which is inherited from the logic itself and facilitates the proof of some properties that would not be so obvious if the program was written in an imperative programming language, for example. However, a logic needs to have some important characteristics to be the basis of a programming language. Namely, it is necessary that the proof search is well-behaved'', meaning that there is a deterministic procedure to look for proofs. Due to this restriction, only a few logics, or parts of it, can be implemented as a programming language. As a consequence, these languages are also limited, not having some basic features such as modularization, data abstraction or concurrency. The most popular logic programming language, Prolog, is an example of such limited programming languages. Since the popularization of the logic programming paradigm, numerous attempts have been made to increase the expressiveness of the underlying logic, so that the programming language obtained has more features yet still purely logic. Among the most significant contributions are LO and lambda-Prolog, whose logics can capture modularization, data abstraction and some aspects of concurrency. Nevertheless, the logics implemented are still fragments (of linear and classical logic, respectively). The impossibility to implement a programming language with the whole classical logic is the main motivation for the study of linear logic, which, in contrast, is a programming language itself. Recently a refinement of the linear logic was proposed with the use of subexponentials, interpreted as locations in the language. With this new logic, the correspondence between algorithms and proof search could be proved. This master dissertation presents an implementation for the linear logic with subexponentials. In order to show the increase of expressiveness of the logic, it is shown the codification of some sequent calculus proof systems in the new language. It also presents the implementation of a simple imperative programming language. The semantics of this language is described using linear logic with subexponentials, therefore it is possible to execute a program using this logic's implementation and it becomes clear the correspondence between algorithms and proof search.