"N'hésitez pas une seule seconde à participer à Mathinfoly si vous aimez les maths, c'était sans hésitations la meilleure semaine de ma vie" - Diego - Mathinfoly 2019



Présentation

Après l’édition de 2016, Mathinfoly revient avec une école d’été à l’interface de l’informatique et des mathématiques, pour étudiants en licence et master.

Une semaine intensive (cours, TD, TP, projet) pour comprendre la révolution des blockchains et les mécanismes de vérification associés. Animé par deux chercheurs de haut niveau, le stage sera encadré par une équipe de jeunes chercheurs enthousiastes.

Public visé : étudiants, élèves des écoles ou cursus préparatoires, en fin de L1, L2, L3 ou M1.

Prérequis : goût pour les mathématiques et l'abstraction. Familiarité avec un langage de programmation, de préférence OCaml. Français courant  et compréhension de l'anglais.

Frais de participation : 200 € avec possibilité de prise en charge intégrale de certains participants. Les frais de participation couvrent l'hébergement et les repas. Les frais de transport sont à la charge des participants.

Le nombre de places est limité à 60 participants choisis sur dossier de candidature.
Les candidatures sont ouvertes aux étudiants francophones.


Initiation à la cryptographie, introduction aux blockchains et à la logique propositionnelle - Pascal Lafourcade

Enseignement en français.


Conférencier : Pascal Lafourcade a obtenu sa thèse à l’ENS Cachan en 2006 sur la vérification automatique de protocoles cryptographique. Puis il a fait un post-doctorat à ETH Zurich dans l’équipe de David Basin. Ensuite il a été pendant 7 ans maître de conférences à l’Université Grenoble Alpes au sein du laboratoire Verimag. Il a développé des techniques de vérification pour des primitives cryptographiques et à analyser la sécurité de nombreux protocoles (e-voting, e-auction, e-examens …). Il aussi rédigé un livre sur la logique et un livre sur la programmation fonctionnelle avec des collègues grenoblois pour des étudiants en Licence. De 2013 à 2016 il a été titulaire de la chaire de confiance numérique de l’Université d’Auvergne au sein du LIMOS. Il est depuis maître de conférences à l’Université Clermont Auvergne. Il a publié de nombreux articles et livres dont un sur les architectures PKI et les communications sécurisés. En Septembre 2018, il a participé à un ouvrage intitulé les blockchains en 50 questions.


Résumé : L’humanité avance grâce aux progrès des hommes et aux moyens mis en œuvre pour transmettre les connaissances de générations en générations. L’invention de l’écriture, comme mesure et consignation de valeur, par les sumériens aux environs de 3 300 avant notre ère, constitue une première révolution. Ensuite la révolution de l’imprimerie aux XVe siècle avec Johannes Gutenberg est une nouvelle étape dans la diffusion des savoirs. Enfin la révolution numérique est en marche et le monde du XXIe siècle est en pleine mutation. Ainsi de nouveaux usages se créent grâce aux progrès technologiques. La création de bitcoin en 2009 par Satoshi Nakamoto, première monnaie dématérialisée et décentralisée, marque clairement une révolution dans la manière de gérer l’information. Cette invention est remarquable et visionnaire à plusieurs titres. L’innovation majeure de bitcoin est la possibilité de créer et d’utiliser de manière décentralisée et distribuée une monnaie sans autorité de confiance. Pour cela chacun peut vérifier la création monétaire et s’assurer que les échanges sont correctement effectués entes les participants. L’autre grande innovation est le mécanisme de la blockchain, en français une chaîne de blocs, qui est au cœur de bitcoin. Ce mécanisme permet d’enregistrer de manière distribuée des informations dans un registre ineffaçable et vérifiable par tout le monde. Ainsi chacun peut, en observant la blockchain, vérifier quel numéro de compte a créé des bitcoins. Ce mécanisme accentue la confiance des utilisateurs dans ce système que personne ne contrôle vraiment totalement.


Dans ce cours nous présenterons les différentes primitives cryptographiques utilisées dans Bitcoin. Nous expliquerons aussi le fonctionnement de bitcoin afin de mieux comprendre les origines des blockchains en se référant aux ouvrages de chez Dunod : « Les blockchains en 50 questions Comprendre le fonctionnement et les enjeux de cette technologie innovante », « Architectures PKI et communications sécurisées » et « Théorie des codes ». Enfin nous introduirons la logique propositionnelle en se référant à l’ouvrage « Logique et démonstration automatique - Introduction à la logique propositionnelle et à la logique du premier ordre » Editions Ellipses

Writing and Verifying Functional Programs in Coq - Cătălin Hrițcu

Enseignement en anglais.


Conférencier : Cătălin Hrițcu is a researcher at Inria Paris where he develops rigorous formal techniques for solving security problems. He is particularly interested in formal methods for security (secure compilation, memory safety, compartmentalization, dynamic monitoring, integrity, security protocols, information flow), programming languages (type systems, verification, proof assistants, property-based testing, semantics, formal metatheory, certified tools), and the design and verification of security-critical systems (reference monitors, secure compilation chains, secure hardware). He is actively involved in the design of the F* verification system and was awarded an ERC Starting Grant on secure compilation with Coq. Catalin was also a PhD student at Saarland University, a Research Associate at University of Pennsylvania, and a visiting researcher at Microsoft Research Redmond.


Résumé : This course will give a gentle introduction to:

  1. logic and proofs,
  2. functional programming, and
  3. program verification.
The most interesting aspect of this course is the use of the Coq proof assistant ( https://coq.inria.fr) to write functional programs and to prove logical theorems about these programs, in a way that is one hundred percent formalized and machine-checked. The course will follow the 1st half of the Logical Foundations book (i.e., Volume 1 of the Software Foundations series: https://softwarefoundations.cis.upenn.edu/). The students will learn the most by solving Coq exercises, from very simple to more interesting ones. The course will also give an overview of the practical successes of functional programming (e.g., the Tezos blockchain implementation is written in OCaml) and of verification in proof assistants like Coq (from machine-checked proofs of mathematical results such as the 4-color theorem to the CompCert verified compiler). We will end with an introduction to the Curry-Howard correspondence, a deep and beautiful connection between functional programs and logical proofs, which lies at the heart of the Coq proof assistant.

Calendrier

  • - Dépôt du dossier de candidature jusqu'au 30 juin.
  • - École d'été du 24 au 31 août 2019

Contact

Participer à Mathinfoly

La période de candidature pour Mathinfoly 2019 est terminée. Si vous souhaitez être informé d'une future édition, inscrivez-vous avec notre formulaire ci-dessous.


Nous n'avons pas pu confirmer votre inscription.
Votre inscription est confirmée.

Inscrivez-vous à notre liste pour recevoir des informations sur Mathinfoly.