The research activity is based on the development of formal tools for describing computational models, programming languages, programs, services and complex systems (e.g., biological or financial).
These tools are employed also for the verification of properties such as security and resource control access and for the development of new languages and principles of programming.
Formal methods are mathematical approaches to solving software problems of specification and design, for safety-critical or security-critical software. An emerging trend is to write the specification of the software problem as a type for a function in some typed programming language, and then finding a program with such a type.
Lambda calculus is an abstract counterpart of higher-level programming languages such as Mathematica or LISP, whose main feature is defining functions through possibly recursive equations. Research in lambda calculus provided models, to be used in software-checking techniques as abstract interpretation, and type systems for static checking of these languages.
