Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Concept

Isabelle (logiciel)

Séances de cours associées (31)

Introduction aux scripts de preuve: bases de Ltac Connectez-vous à Mediaspace pour regarder cette vidéo

Présente les bases du script de preuve en Coq, en se concentrant sur le langage Ltac et ses tactiques pour gérer efficacement les preuves.

Polymorphisme dans Coq: Structures de données et fonctions Connectez-vous à Mediaspace pour regarder cette vidéo

Couvre le polymorphisme dans Coq, en se concentrant sur les structures de données et les fonctions telles que les listes, la longueur et l'ajout.

WireGuard : protocole cryptographique pour les VPN Connectez-vous à Mediaspace pour regarder cette vidéo

Explore le protocole WireGuard, un remplacement VPN moderne pour IPsec et OpenVPN, en se concentrant sur les tunnels cryptés et les propriétés de sécurité.

Transport optimal : théorie et applications Connectez-vous à Mediaspace pour regarder cette vidéo

Explore les multiplicateurs de Lagrange, les théorèmes minimax et les sous-ensembles convexes dans la théorie du transport optimal.

Introduction à Coq: Expressions arithmétiques et évaluateurs Connectez-vous à Mediaspace pour regarder cette vidéo

Couvre les bases de Coq, en se concentrant sur les expressions arithmétiques, l'évaluation et les techniques de preuve.

Sémantique à grande échelle : définition d'expressions et de commandes arithmétiques Connectez-vous à Mediaspace pour regarder cette vidéo

Couvre la définition d'un langage de programmation simple et sa sémantique à grande échelle, y compris les expressions arithmétiques et les commandes impératives.

Techniques de programmation logique: Recherche et unification automatisées de preuves Connectez-vous à Mediaspace pour regarder cette vidéo

Couvre les concepts de programmation logique, en se concentrant sur la recherche de preuve automatisée et les techniques d'unification dans Coq.

Constructions universelles : modèles de consensus et de mémoire partagée Connectez-vous à Mediaspace pour regarder cette vidéo

Explore l'universalité, les objets de consensus, les modèles de mémoire partagée et l'implémentation de file d'attente FIFO.

Propositions inductives : comprendre l’évaluation dans Coq Connectez-vous à Mediaspace pour regarder cette vidéo

Couvre les propositions inductives en Coq, en se concentrant sur les règles dévaluation pour les expressions arithmétiques et leurs applications dans la définition des fonctions partielles et non déterministes.

Conformité des composants normaux Connectez-vous à Mediaspace pour regarder cette vidéo

Explore la conformité des composants normaux à travers les bords et l'importance de la continuité pour les composants génériques.

Théorème des mathématiques Prover Connectez-vous à Mediaspace pour regarder cette vidéo

Introduit le Mathgraph Theorem Prover, montrant son approche unique pour représenter des propositions et organiser des graphiques pour la logique de premier ordre.