UE Langages et algorithmique / Languages and algorithmics

L'objectif de ce cours est double.
1) Une introduction à l'assistant de preuve Coq, qui fait autorité dans le domaine de la vérification notamment pour des compilateurs et OS certifiés.
2) L'étude des concepts mis en œuvre pour compiler des langages de programmation, notamment les principaux formalismes utilises pour définir leur sémantique. La mise en pratique s'effectue en s'appuyant sur Coq.

- Architecture d'un compilateur et phases de compilation
- Logique typée d'ordre supérieur, règles de déduction
- Récurrence structurelle, récurrence sur une relation inductive
- Pratique de l'assistant à la preuve Coq
- Arbres de syntaxe abstraite
- Sémantique informatique

The objective of this course is twofold.
1) An introduction to the Coq proof assistant, which is authoritative in the field of verification especially for certified compilers and OS.
2) The study of the concepts underlying the compilation of programming languages, in particular the main formalisms used to define their semantics. The practice is based on Coq.

- Compiler architecture and compilation steps
- higher-order typed logic, deduction rules
- structural induction, induction on an inductive relation
- practice of the Coq proof assistant
- abstract syntax trees
- computational and relational semantic

Voir la page complète

A : Cryptographie et Complexité
- Introduire les principes de la cryptographie : clé secrète et clé publique, algorithmes et protocoles
- Comprendre les principes sous-jacents aux crypto-systèmes et à leur utilisation.

B : Graphes et Complexité.
Le cours présente la théorie des graphes. On y présente la théorie des graphes sous plusieurs de ses aspects.

   A -
1. Calculs modulo un entier.
2. Cryptographie à  clé secrète. 
3. Cryptographie à  clé publique.

   B -
0) vocabulaire de base et représentation des graphes.
1) raisonnement sur les graphes (orientés ou non) avec les différentes classes : biparti, planaires, sans circuits, eulérien, hamiltonien
2) présentation d'algorithmes classiques avec leur calcul de complexité : connexité et forte connexité et dfs, Dijkstra et bfs, Kruskal, Flot maximum
3) des exemples de modélisation avec les graphes.
4) un grand nombre de problèmes de décisions en graphe et leur classe de complexité.

A: Cryptography and Complexity
- Introduction to basic principles of cryptography: secret and public jeys, algorithms and protocols
- Understand the principles behind cryptosystems and their uses

B: Graphs and Complexity
We introduce graph theory, with a focus on complexity analysis, Modeling, Reasoning with graphs, and Algorithmic.

   A -
1. Computations modulo an integer.
2. Symmetric-key cryptography.
3. Public-key cryptography.

   B -
0) basic vocabulary and representation of graphs
1) reasoning with graphs (both directed and undirected) and the different classes: bipartite, planar, acyclic, eulerian, hamiltonian.
2) Presentation of classic algorithms and their complexity: connectedness, strong connectedness and DFS, Dijkstra and BFS, Kruskal, max-flow
3) Examples of modelling with graphs
4) A great number of decision problems on graphs and their complexity classes.

Voir la page complète

Comprendre le paradigme de la programmation fonctionnelle dans le langage OCaml, être apte à en reconnaître l'emploi et l'utilisation dans des situations variées y compris avec d'autres langages comme Java ou C .

- Bases de OCaml
- Structures de données et de contrôle récursives
- Mécanisme d'évaluation
- Fonctions d'ordre supérieur
- Modules et foncteurs
- Typage, inférence de types, polymorphisme
- Exceptions, références, types mutables
- Flots et analyse

Understand the paradigm of functional programming in OCaml language, be able to recognize its use in various situations including with other languages such as Java or C.

- OCaml basics
- Recursive data-structures of data and recursive programming
- Evaluation mechanism
- Higher order functions
- Modules and functors
- Typing, type inference, polymorphism
- Exceptions, references, mutable types
- Streams and recursive desce

Voir la page complète