Sommaire

  • Cet exposé a été présenté le 03 décembre 2004.

Description

  • Orateur

    Pierre Castéran - LABRI

L'exposé se veut une introduction à l'assistant de démonstration Coq, ( http://coq.inria.fr ) ainsi qu'au formalisme sur lequel se base cet outil : le Calcul des Constructions Inductives. Des exemples, empruntés aux mathématiques ou a l'algorithmique, montreront la puissance d'expression de ce formalisme.

Prochains exposés

  • Schéma de signature à clé publique : Frobénius-UOV

    • 29 mai 2026 (13:45 - 14:45)

    • IRMAR - Université de Rennes - Campus Beaulieu Bat. 22, RDC, Rennes - Amphi Lebesgue

    Orateur : Gilles Macario-Rat - Orange

    L'exposé présente un schéma de signature à clé publique post-quantique inspiré du schéma UOV et introduisant un nouvel outil : les formes de Frobénius. L'accent est mis sur le rôle et les propriétés des formes de Frobénius dans ce nouveau schéma : la simplicité de description, la facilité de mise en oeuvre et le gain inédit sur les tailles de signature et de clé qui bat RSA-2048 au niveau de[…]

  • Yoyo tricks with a BEANIE

    • 05 juin 2026 (13:45 - 14:45)

    • IRMAR - Université de Rennes - Campus Beaulieu Bat. 22, RDC, Rennes - Amphi Lebesgue

    Orateur : Xavier Bonnetain - Inria

    TBD

    • Cryptography

    • Symmetrical primitive

Voir les exposés passés
Haut de page