View  Edit  Attributes  History  Attach  Print 
Coquas / Coquas

edit SideBar

Welcome on the web-site of the ANR 12 JS02 006 01 project COQUAS.


The project "COQUAS: COmputing with QUAntitative Semantics" is a three-year young researcher project, started on January 2013 and supported by the French national research agency ANR.

Quantitative semantics refers to a family of denotational models of linear logic and functional programming that interpret proofs as linear mappings between vector spaces, and ordinary programs as power series. Nowadays, an ever livelier research is flourishing in this framework --- vectorial based semantics of functional languages, 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 setting 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. In particular, we plan to achieve two significant outcomes, witnessing the relevance of this approach:

  • develop a semantic description of intensional information about program's computational cost (for example, time/space consumption);
  • give a denotational account for higher-order probabilistic and quantum functional programming.

The two goals 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.

Click here for a more detailed description of the project.


↑ Top  View  Edit  Attributes  History  Attach  Print 
This page was last modified on March 10, 2015, at 05:45 PM