TypiCal

Je parlerai de quelques aspects du travail mené dans l'équipe Parsifal, et de la façon dont cela pourrait s'articuler avec Coq.

Dans une première partie je présenterai les logiques avec points fixes (définitions inductives et coinductives) que nous utilisons, en comparant un peu avec le calcul des constructions inductives. Cela me permettra d'introduire certains fragments et des stratégies de recherche de preuve, en discutant de la pertinence de leur adaptation à Coq.

Dans une seconde partie, je traiterai de la notion plus délicate de quantification générique (nabla). Cette notion apporte une expressivité très intéressante à nos logiques, puisqu'elle permet de spécificier naturellement des systèmes tels que le lambda ou le pi-calcul, mais son "adaptation" à Coq semble difficile; j'évoquerai cependant des pistes.