Reasoning with Circular proofs for Programming – RECIPROG
ReCiProg is a collaborative project (Lyon-Marseille-Nantes-Paris) aiming at extending the proofs-as-programs correspondence (also known as Curry-Howard correspondence) to recursive programs and circular proofs for logic and type systems using induction and coinduction. The project will contribute both to the necessary theoretical foundations of circular proofs and to the software development allowing to enhance the use of coinductive types and coinductive reasoning in the Coq proof assistant: such coinductive types present, in the current state of the art serious defects that the project will aim at solving.
Project coordination
Alexis Saurin (Institut de Recherche en Informatique Fondamentale)
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.
Partnership
IRIF Institut de Recherche en Informatique Fondamentale
LS2N Laboratoire des Sciences du Numérique de Nantes
LIP - CNRS Laboratoire d'Informatique du Parallélisme
LIS Laboratoire d'Informatique et Systèmes
Help of the ANR 456,182 euros
Beginning and duration of the scientific project:
September 2021
- 48 Months
