Jarosław Miller
supervisor: Agata Pilitowska
Formal methods is a branch of theoretical computer science that deals with the mathematical proving of the properties of programming languages and the programs themselves. One of the most powerful (and probably the most beautiful) tools of formal methods is Curry-Howard correspondence. This is a surprising property that links logic systems with typed programming languages. In short, it identifies propositions of logic with types and, going further, programs of a given type with proofs of the corresponding proposition. It is worth emphasizing: these programs do not generate proofs, they are proofs! By using tools based on Curry-Howard correspondence, such as the Agda proof assistant, we can, inter alia, construct new languages and prove their properties.
In my research, I try to use Agda and linear logic (also known as logic of resources) to construct a language used to describe the operation of the financial market. Such a language could define not only basic market operations, such as exchanging currencies or buying shares, but also sophisticated financial instruments such as shorts. Combined with modern technologies such as blockchain, this language can be used to create a decentralized and automated stock market whose security would be formally proven.