Reasoning And Programming With Infinite Data Objects
Alexis Saurin, firstname.lastname@example.org
IRIF, PPS team:
Yann Régis-Gianas – Paris Diderot University
Alexis Saurin (coordinator) – CNRS
Christine Tasson – Paris Diderot University
David Baelde – ENS-Cachan
LIP, PLUME team:
Pierre Clairambault — CNRS
Damien Pous – CNRS
Colin Riba – ENS-Lyon
PhD students and post-docs involved in the project:
Jules Chouquet (anr-funded phd student)
Abhishek De (soon to become phd student)
Amina Doumane (post-doc at LIP)
Marie Kerjean (anr-funded phd student)
Guilhem Jaber (post-doc, intially anr-funded)
Rémi Nollet (phd student)
Pierre Pradic (phd student)
Anupam Das (post-doc)
Pierre-Marie Pédrot (phd student)
Andrew Polonsky (anr-funded post-doc)
In a nutshell
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 trees from a proof-theoretical
perspective with an eye towards model-checking problems.
or contact us.
Open positions and annoucements
We currently have an open post-doc position: apply by july 18, 2018! Read more.
Coming soon: Paris workshop will take place at FLOC on 7th and 8th of july.
june 2018: Pierre-Marie Pédrot and Guilhem Jaber get permanent positions in Nantes as INRIA researcher and Maître de conférences, respectively!
june 2018: Amina Doumane will receive Ackermann award at CSL 2018
may 2018: Abhishek De got a PhD grant to join IRIF next fall and start his PhD on RAPIDO's themes.
may 2018: Paris workshop accepted papers and invited speakers are online!
may 2018: Xavier Onfroy starts his Master internship on formalizing circular proof validity
april 2018: Marie Kerjean joins RAPIDO project.
january 2018: Amina Doumane received Gilles Kahn award for the best french PhD thesis in computer science
january 2018: Andrew Polonsky joins the Appalachian state university as a post-doc!
july 2017: we shall organise a workshop at FLOC 2018
2017/07/04: Workshop on Coinduction in Type Theory to be held in Chambéry during the week of the 4th of july
june 2017: Amina Doumane defends her PhD.
may 2017: Amina Doumane receives Kleene award for the best student paper at LICS 2017: constructive completeness for the linear time mu-calculus
2017/03/17: mid-term evaluation of the project by ANR.
january 2017: Guilhem Jaber moves to PLUME
2016/11/22: Project meeting in IRIF
october 2016: Jules Chouquet, Rémi Nollet and Pierre Pradic start their PhDs
2016/06/10: Project meeting in IRIF
2016/06/03: Second part of Amina' talk at RAPIDO's working group
2016/07/27: Amina Doumane speaks at RAPIDO's working group about infinitary proof theory
2016/04/01: Second part of Guilhem's talk at RAPIDO's working group
2016/03/17: Guilhem Jaber speaks at RAPIDO's working group on using guarded recursion for program reasoning
january 2016: Andrew Polonsky joins the project in Paris
january 2016: PPS and LIAFA labs merges. PPS is now a team part of IRIF
december 2015: Giulhem Jaber joins the project in Paris
spring 2016: Project working group starts in Paris