Objectifs pédagogiques
Acquis d'apprentissageÀ l'issue de l'UE, l'élève sera capable de:
- Prouver l'impossibilité de certaines tâches algorithmiques par la théorie de la calculabilité.
- Convertir une preuve mathématique en programme et vice versa par la correspondance de Curry-Howard.
- Programmer ou effectuer des preuves dans le langage Coq.
Compétences de rattachement (et justification)
- BC1.1 – Analyser des systèmes existants de traitement des données, de communication et/ou d’organisation de l’information, en mobilisant les sciences et technologies (mathématiques, physique et informatique) dans un but d’audit ou d’optimisation; Justification : Par les outils de la calculabilité et du typage permettant d'encadrer ce qu'un algorithme peut ou ne peut pas faire.
- BC10.3 – Analyser une résolution par des approches formelles ou mathématiques; Justification : Par l'étude de la logique et sa correspondance avec la programmation.
réparties en:
- Travaux Dirigés :
- Travaux Pratiques :
- Cours magistral :
- Contrôle de connaissance :
Diplôme(s) concerné(s)
UE de rattachement
- MDC_3UE01_TP : Fondamentaux des mathématiques et de l'informatique
Format des notes
Numérique sur 20Pour les étudiants du diplôme Diplôme d'ingénieur
Vos modalités d'acquisition :
Contrôle de connaissances déterminant la note finale
Le rattrapage est autorisé (Note de rattrapage conservée)- le rattrapage est obligatoire si :
- Note initiale < 10
Le coefficient de l'UE est : 0.4
L'UE est évaluée par les étudiants.
Méthodes pédagogiques
Cours magistraux, TD et TPSupport pédagogique multimédia
