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

Catégorie

Sémantique des langages de programmation

Séances de cours associées (23)

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.

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.

Lambda Calculus: Syntaxe et Abstractions

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

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.

Programmation fonctionnelle: concepts et mise en œuvre

Couvre les concepts et la mise en œuvre de la programmation fonctionnelle dans Scala, mettant l'accent sur les fonctions, les données immuables et l'abstraction des données.

Atelier Coq: Introduction au théorème interactif

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

La sémantique musicale : problèmes et perspectives

Explore la sémantique musicale, discute des inférences déclenchées par différents éléments musicaux et propose un cadre pour comprendre le sens de la musique.

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.

Type Règles : Progrès et préservation

Couvre Amyli, un petit langage fonctionnel, tapez des règles et de la solidité.

Fondements du logiciel

Couvre les bases de l'induction, de la syntaxe, de la syntaxe abstraite vs. concrète et de la sémantique opérationnelle pour les booléens.

Exemple de sémantique de boucle

Explore la sémantique des boucles, démontrant comment calculer systématiquement la signification d'une boucle while.

La sémantique relationnelle des boucles

Explore la sémantique relationnelle des boucles dans les programmes et l'interprétation mathématique des structures de boucles.

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.

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.

Une introduction à l'iris: logique de séparation simultanée d'ordre supérieur

Introduit Iris, un cadre logique pour raisonner sur la sécurité et l'exactitude des programmes impératifs d'ordre supérieur simultanés, en mettant l'accent sur ses caractéristiques et applications uniques.

Sémantique opérationnelle : Amyli Language

Couvre le langage Amyli, y compris la syntaxe abstraite, la représentation de programme et la sémantique opérationnelle.

Synthèse de haut niveau: circuits élastiques formellement vérifiés

Présente le développement d'un compilateur de synthèse de haut niveau vérifié pour les circuits élastiques.

Le calcul Lambda et la sécurité des types: un aperçu Connectez-vous à Mediaspace pour regarder cette vidéo

Fournit un aperçu du calcul lambda, de la sécurité de type et de l'inférence de type dans les langages de programmation.

Hoare Logic: Fondements et applications Connectez-vous à Mediaspace pour regarder cette vidéo

Couvre Hoare Logic, ses fondements, ses applications et son importance dans la vérification des programmes.

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.