Séances de cours associées à Sans titre

Atelier Coq: Introduction au théorème interactif

Introduit Coq, un assistant de théorème interactif basé sur l'isomorphisme de Curry-Howard.

Composition des applications en mathématiques

Explore la composition des applications en mathématiques et l'importance de comprendre leurs propriétés.

Présente le produit cartésien et l'induction pour les épreuves utilisant des entiers et des ensembles.

Types dépendants dans les langages de programmation

Explore les cartes, les opérateurs de type, l'équivalence, les types de première classe, System Fw, Coq, et les défis de la vérification de type dans les langages de programmation.

Fondements de Scala: Modélisation et Systèmes de Type

Couvre les fondements de Scala, y compris la modélisation des types récursifs, des types paramétrés et de la variance.

Intégration de formes différentielles

Couvre l'intégration de formes différentielles sur des variétés lisses, y compris les concepts de formes fermées et exactes.

Fonctions de cartographie et surjections

Explore les fonctions cartographiques, les surjections, les fonctions injectives et surjectives et les fonctions bijectives.

Agent Gitlab pour Kubernetes (agentk)

Couvre la configuration d'un agent Gitlab pour Kubernetes, en mettant l'accent sur l'installation, le contrôle de version et le dépannage.

Tests basés sur la propriété: techniques avancées

Explore les techniques de test logiciel avancées, y compris les tests basés sur les propriétés, pour assurer l'exactitude du code et améliorer la qualité du logiciel.

Homéomorphismes locaux et couvertures

Couvre les concepts d'homéomorphismes locaux et de couvertures en multiples, en mettant l'accent sur les conditions dans lesquelles une carte est considérée comme un homéomorphisme local ou une couverture.

Algorithmes d'approximation

Couvre les algorithmes d'approximation pour les problèmes d'optimisation, la relaxation LP et les techniques d'arrondi aléatoire.

Concevoir des expériences d'apprentissage: projet de classe CS411

Présente le projet de classe CS411, où les élèves conçoivent et testent une leçon en utilisant des théories d'apprentissage.

Preuves : Logique, Mathématiques et Algorithmes

Explore les concepts, les techniques et les applications de la preuve dans la logique, les mathématiques et les algorithmes.

Sans titre Connectez-vous à Mediaspace pour regarder cette vidéo

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.

Sans titre Connectez-vous à Mediaspace pour regarder cette vidéo

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.

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.