Blanc Inter II SIMI 2 - Blanc International II - SIMI 2 - Science informatique et applications

Logical Approach to Novel Computational Paradigms – Locali

Submission summary

Logic and algorithms are two important research areas in computer science. Traditionally, logic has been one of the important cornerstones of mathematics in Europe, while Chinese scholars have been more adept in the research on algorithms. The famous "Nine Chapters on Algorithms" in ancient China and the contemporary mathematician Professor Wu Wenjun’s mechanical proof theory are precisely the incarnation of traditional Chinese philosophy. The dialogs between logics and algorithms have been a constant source of progress for both disciplines, which, in turn, stimulates the development of computer science.

The dialogs are reflected in two aspects: one aspect focuses on the languages used to express proofs and algorithms. The algorithmic interpretation of proofs permits the use of algorithmic languages as proof languages, i.e. to import languages from computer science to logic, and conversely to equip proof languages with an operational semantics and to give computer science new algorithmic languages, by importing them from logic. Another aspect of this dialog is the challenge to incorporate concurrent programs. This duality is reflected by the distinction between lambda-calculus and pi-calculus. Our project extends and reformulates both calculi and proposes to design new programming languages and proof systems, based on a study of their relation to logic.

The research of this project will focus on new emerging directions in this dialogs between logics and algorithms : namely, a new logically inspired computational method : the scheme calculus, a new way to express theories in a computationally inspired way in clausal polarized Deduction modulo, a new extension of tree automata with internal communication and parallel composition, that extends also the language CCS: CCTS, and a new calculus to solve distributed constraint optimization problems and other similar problems (e.g., multi-core scheduling) from the perspective of co-induction. The members of the project have been active in the emergence of these new calculi. The project has not only theoretical significance but also practical relevance.

Project coordination

Gilles Dowek (INRIA Paris-Rocquencourt) – gilles.dowek@inria.fr

The author of this summary is the project coordinator, who is responsible for the content of this summary. The ANR declines any responsibility as for its contents.

Partner

INRIA INRIA Paris-Rocquencourt
PPS UNIVERSITE DE PARIS 7

Help of the ANR 426,055 euros
Beginning and duration of the scientific project: December 2011 - 48 Months

Useful links

Explorez notre base de projets financés

 

 

ANR makes available its datasets on funded projects, click here to find more.

Sign up for the latest news:
Subscribe to our newsletter