Computational effects in computable and formalized mathematics (EFFMATH) Project summary

In mathematics the application of a function f to an argument x always yields the same result y = f(x), which depends just on x and nothing else. In programming the situation is different. A program may do other things apart from computing the result from the given input: it may get caught in a non-terminating loop, abort execution, interact with the external world through communication channels, use internal memory to store and retrieve data between invocations, compute results using random numbers, etc. All such phenomena are collectively known as computational effects. A comprehensive mathematical theory of computational effects was developed by Moggi [9] under the slogan “effects are monads”. It has been very successful, not only in theory but also in practice, as it heavily influenced the design of real-world programming languages, most notabl