Computing with Quantitative Semantics – CoQuaS

The project focuses on formal foundations for language-based (especially static) techniques guaranteeing resource-related runtime properties of programs. The project belongs to the research area whose aim is to associate to a program a certification assuring some specific properties. We will derive the tools and techniques for our investigation from the field of logical proof theory and semantics, with special interest in linear logic and lambda-calculus.

An ever livelier research is flourishing in quantitative semantics --- vectorial based semantics, differential extensions of linear logic, algebraic and resource-sensitive lambda-calculi. As a result, new interactions appear between linear algebra and the formal method approach to computation, renovating the theoretical framework of denotational semantics.

It is now time to apply this approach to one among the basic challenges of computer science --- to describe "what" and "how" programs compute, abstracting away from syntactical details. Our goal is to provide concrete examples of the new observations one can do on computing through quantitative semantics.

As a submission to the ``Jeunes Chercheuses, Jeunes Chercheurs'' program, this proposal has precise and well defined objectives. We plan to achieve two significant outcomes, witnessing the relevance of the quantitative semantics approach to computation:

— develop a semantic description of intensional information about the program’s computational cost (for example, time/space consumption, see Milestone 3.1. of the scientific proposal);

— give a denotational account for higher-order quantum functional programming (see Milestone 3.2).

Both goals are ambitious and their achievement will fill rather big gaps in the current literature (see Task 3 for more details). These milestones will be the main benchmarks for estimating the success of the project. They are independent but both demand for a mathematical account of the computer science notion of non-duplicable resource. Quantitative semantics is there to give it starting from the notion of algebraic linearity.

This project will be developed in the ``Logic, Computation and Reasoning'' (LCR) team of LIPN, in fact three among the five participants of the proposal are members of LCR. Among the main research directions of LCR there are linear logic proof theory, functional programming and implicit computational complexity. We are convinced that quantitative semantics will perfectly install itself as a new research axis in LCR, upgrading the team's research activity and taking benefit from the local expertise. Moreover, this research proposal may also strengthen the interaction with the experts in the algebraic combinatorics areas, which is another main focus of LIPN.