L'objectif de cette UE est double.
D'une part cette UE apporte des connaissances en informatique théorique et fondamentale, à travers l'étude des langages rationnels et algébriques, des automates à états finis et à pile, illustrés de preuves de théorèmes de rationalité ou non, d'algébricité ou non, ainsi que de minimisation des états. L'UE prépare ainsi au module de modèles de calculs qui introduira les machines de Turing en M1.
D'autre part, des TP permettent d'illustrer les concepts théoriques, en montrant l'implémentation et le fonctionnement pratique des automates introduits de manière formelle. Les TP sont effectués à l'aide de l'assitant à la preuve Coq, qui permet, en adéquation avec le module logique classique, d'implémenter les automates et les grammaires avec le langage Gallina, puis de faire des preuves d'équivalences entre automates et grammaires.
Une introduction à l'analyse lexicale et syntaxique permettra également de préparer au module de compilation en M1.
