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

  • Polytopes in the Fiat-Shamir with Aborts Paradigm

    • 29 novembre 2024 (13:45 - 14:45)

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

    Orateur : Hugo Beguinet - ENS Paris / Thales

    The Fiat-Shamir with Aborts paradigm (FSwA) uses rejection sampling to remove a secret’s dependency on a given source distribution.  Recent results revealed that unlike the uniform distribution in the hypercube, both the continuous Gaussian and the uniform distribution within the hypersphere minimise the rejection rate and the size of the proof of knowledge. However, in practice both these[…]

    • Cryptographie

    • Primitive asymétrique

    • Mode et protocole

  • Post-quantum Group-based Cryptography

    • 20 décembre 2024 (13:45 - 14:45)

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

    Orateur : Delaram Kahrobaei - The City University of New York

Voir les exposés passés
Haut de page