Objectives CoLoHA

Mathematical logic is a fundamental area at the frontier of mathematics and computer science. Historically, it is considered as a fundamental field of mathematics, and on the other side nowadays the urge for trustworthy and reliable software and hardware is met by grounding their development on formal mathematical methods, which makes it fundamental to computer science as well. Our research is primarily focused on the computational logics and corresponding type systems, and represents a theoretical foundation and starting point for the development of both typed functional programming and environments for the provably correct development of programs. Verification of formal proofs of correctness of software, as well as of complex mathematical proofs on computers with domain-specific formalisms, is an innovative approach that will increasingly substitute costly and only ideally exhaustive testing of software or hand-checking of long mathematical proofs that are prone to errors. Modern interactive theorem provers, also called proof-assistants, embody the idea of checking of proof-sketches given by a human user, and relieving him by automating some of the easy or cumbersome proof steps. Proof-assistants are also increasingly important in academia, where they already play a role either in the process of the research in mathematics, or in the meta-theoretical effort related to symbolic systems, as those studied in logic and computer science. They begin as well to intervene in the process of the contemporary education of mathematicians, computer scientists and engineers. We believe that the sociological and economical importance of such systems will increase, as they will become integrated in production processes demanding mathematics at industrial scale.

Our research contributes at large to:

• (i) the logical foundations of low-level aspects of such systems, by investigating alternative formats of the manipulated objects (which can be used as internal representations), and the logical aspects of issues related to such systems’ implementation (like efficient evaluation strategies);
• (ii) the logical foundation of delimited control operators in programming languages, and
• (iii) the theory of operads and higher algebra in relation with Homotopy Type Theory and foundations of mathematics.