DS0705 - Fondements du numérique

Reasoning And Programming with Infinite Data Objects – RAPIDO

Submission summary

Rapido aims at gathering young researchers to investigate the applicability of proof-theoretical methods to reason and program on infinite data objects.

The goal of the project is to develop logical systems capturing infinite proofs (proof systems with least and greatest fixed points as well as infinitary proof systems), to design and to study programming languages for manipulating infinite data such as streams both from a syntactical and semantical point of view.

Moreover, the ambition of the project is to apply the fundamental results obtained from the proof-theoretical investigations (i) to the development of software tools dedicated to the reasoning about programs computing on infinite data, e.g. stream programs (more generally coinductive programs), and (ii) to the study of properties of automata on infinite words and infinite trees from a proof-theoretical perspective, with an eye towards model-checking problems.

Project coordination

Alexis Saurin (Preuves, Programmes, Systèmes (PPS UMR 7126))

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.


PPS - UMR 7126 Preuves, Programmes, Systèmes (PPS UMR 7126)

Help of the ANR 398,996 euros
Beginning and duration of the scientific project: September 2014 - 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