Standard recursion theory deals with extensional aspects of computation, namely properties of the input/output semantics of programs viewed as (computable) functions. A huge toolset is provided to reason about what programs do, the way to specify and reason about the semantics of programs, and what can be automatically proved about their extensional behavior. Much less is known on the side of tools and methods for reasoning about the intensional structure of this code, namely the way these functions are actually implemented as code in a given programming language or as algorithm for efficiently solving problems.

Designing, analysing and reasoning about programs is not just designing, analysing, and reasoning about input/output functions. This intensional aspect of computation hides fundamental properties such as the quality of code, its complexity, its understandability, the way
an automated tool for program analysis is capable to extract information (e.g., alarms for potential bugs), etc. In particular the intensional structure of programs represents the key aspect in the way any code manipulating tool (e.g., an optimizing compiler, a static analyzer, a dynamic testing tool) performs, with important consequences both in software engineering and in complexity.

We lack of a comprehensive theory of intensional aspects of computation, capable in formally specifying within a universal (language independent) and general (property independence) framework the intensional properties of programs and to reason about them.

Interesting results concerning the possibility of widening standard recursion theory towards intensional aspects of code have been made in the last decade. These include, among the others, the Intentional Contents of Rice Theorem in the case of Blumm’s complexity in
POPL2008 until the more recent Analyzing Program Analyses in POPL2015. Also the recent result on the (Im)possibility of Obfuscating Programs in JACM2012 makes this dichotomy evident: It is impossible to deform the intensional structure of programs in such a way that the new code generated preserves the original extensional behaviour but anything can be learnt from it is just its input/output functionality.

Intensional aspects affect code performance, such as its complexity (both in time and space), but also affect what an external (automatic or semiautomatic or even human) analysis can extract and understand about code. Intensionally different but extensionally equivalent programs may exhibit completely different behavior when analyzed, e.g., by a static program analyses, often producing a different number of false alarms when analyzed. This may affect analysis credibility and effectiveness, and well as its performance.

Intensionality is also relevant in security. Malicious code employs intensional transformations for foiling syntactic malware detection, and benign code employs obfuscation as a way for intensionally escaping from reverse engineering when code holds secret information, e,g.,
cryptographic keys when executed in hostile environments.

Recursion theory, complexity theory, security, and program analysis have developed their own corpus of theoretical results for understanding and proving their limits and possibilities often in isolation. Most of these results share a common underlying structure which hints that they belong or are instances of more general results concerning intensional and extensional properties of computation. Understanding this requires a translational approach to theoretical computer science which combines disciplines, resources, expertises, and techniques with the common goal of having a unique corpus of methods for understanding all aspects of computation. The key question that this NII Shonan meeting will attempt to give answer is:

Can we build a general enough theory of intensional and extensional properties of programs (and models of computation) that allows us to prove impossibility and possibility results in many different fields of CS, including code obfuscation, precision of program analysis, and implicit computational complexity?

Knowing the possibilities and the limits of how much of intensional information we can inject into general and universal results describing the behaviors or computation systems, yet keeping these results valid, is a challenge. This challenge has both theoretical and applied fallouts. Theoretically we are interested in understanding the scope of validity of fundamental results of computability theory beyond the standard recursion theory and towards properties affected by the way the code is written and constructed. In applications we are interested in unifying phenomena concerning the way code is written and analysed in different, apparently orthogonal fields, such as program analysis, code obfuscation, and complexity.

This NII Shonan meeting is intended to bring together theoreticians and experts in program reasoning, program analysis, logic, implicit computational complexity, categorical semantics, code transformation, and security, in order to find the common underlying mathematical
structures that are shared by intensional and extensional properties of computational systems. Our goal is to set up a community around these foundational themes with the ambition of influencing the foundations of these disciplines. We will benefit from an interdisciplinary
approach, bridging theoreticians with experts in applied program transformation and analysis. The longterm fallout will be the exploration of the possibility of having a new and unifying theoretical foundation for all phenomena related with the intensional structure of code, which goes beyond standard recursion theory.