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

Catégorie

Théorie des types

Séances de cours associées (32)

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.

Formules logiques et types: comprendre l'isomorphisme de Kerry Howard

Explore l'isomorphisme de Kerry Howard, traduisant des propositions logiques en types et en termes, en mettant l'accent sur la preuve par induction et la préparation à l'examen.

Vérification de type et reconstruction: équations et unification

S'intéresse à la vérification de type, à la reconstruction, aux équations, à l'unification, au système Hindley/Milner, au polymorphisme et aux principaux types.

Lambda Calculus: Syntaxe et Abstractions

Introduit des termes, des abstractions, des applications et des valeurs dans le calcul lambda.

Types dans Lambda Calculus

Couvre les types dans le calcul lambda, y compris la définition des types, la spécification des règles et la preuve de la solidité.

Atelier Coq: Introduction au théorème interactif

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

Programmes de vérification avec l'inox: Comment fonctionne l'inox

Explore le fonctionnement intérieur du cadre Inox, en mettant l'accent sur les transformations de vérification et de contrôle de type dépendant.

Chiffres d'église et conditionnels

Explore les chiffres de l'église et encode les conditionnels en lambda calcul.

Lambda Calculus: Numéros d'église

Explore les chiffres de l'église, les booléens, les paires, la récursion et l'équivalence comportementale dans Lambda Calculus.

Programmation Fonctionnelle Vérifiée : Nicolas Voirol défense de thèse de doctorat publique

Explore la programmation fonctionnelle vérifiée, la vérification formelle, les résolveurs SMT, la vérification de type, les fonctionnalités Scala, l'automatisation et les types dépendants.

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.

Lambda Calculus: Sémantique opérationnelle et stratégies d'évaluation

Couvre la sémantique opérationnelle et les stratégies d'évaluation dans le calcul lambda, y compris redex, les stratégies d'évaluation alternatives et les booléens de l'Église.

Atelier Coq: Types de données inductives et preuves

Couvre la définition d'un type de données inductives dans Coq et la façon de construire des preuves de manière interactive en utilisant des tactiques.

Sémantique dans le traitement du langage informatique: comprendre le sens

Couvre la sémantique des langages de programmation, en se concentrant sur le langage Add et le rôle des règles de réécriture et des machines CK dans la compréhension du sens.

Codage de la récursivité comme auto-application

Explore le calcul lambda, les fonctions d'ordre supérieur et l'encodage récursif des fonctions.

Coq: Vue d'ensemble

Présente Coq et se concentre sur la démonstration du théorème et du _comm étape par étape.

Groupes autosimilaires : Automorphismes d'arbres enracinés

Couvre les groupes autosimilaires et les automorphismes des arbres enracinés, explorant les groupes finis résiduels et les sous-groupes de congruence.

Compilateur de vérification: Approche Spec#

Explore le système de programmation Spec#, en se concentrant sur un compilateur de vérification pour C# 2.0.

Sous-typage et polymorphisme

Explore les règles de sous-typage, les défis et son lien avec diverses formes de polymorphisme dans les langages de programmation.

Analyse de la production d'intrants multirégionaux: EXIOBASE 3

Couvre le calcul d'Economy-Wide Material Flow Analysis pour la Suisse à l'aide d'EXIOBASE 3.