Grupo de Computación Teórica
- We invesigate the theory and technology of Programming, i.e. the languages, methods and tools employed in program construction and proof.
- The evidence of the correctness of programs is achieved by deductive methods. Therefore, programming is a mathematical activity.
- Modern Formal Logic provides a wealth of formal languages into which to carry out the mathematical activity. Since they are formal, it is possible to construct automatic verifiers of e.g. theorems developed in those languages. Some of those theorems will ascertain the correctness of programs with respect to specifications and therefore, the verifiers in question become verifying compilers. In other words, they realize the motto “if it compiles, it works”.
- In the same way as we conceive Programming as Mathematics, it is possible, conversely, to investigate what kind of Mathematics arises when one takes as primitive the concepts of the discipline of Programming and Computing Science as developed during its history. This is what we call “Mathematics as Programming”.
- One fundamental aspect of our work is the one connected to disclosing, explaining and making generally accessible strategies of problem solving. This stimulates our interest in the didactics of Programming, Mathematics and Logic.