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

Concept

Simply typed lambda calculus

Séances de cours associées (31)

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.

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é.

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.

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.

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.

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.

Lambda Calculus: Syntaxe et Abstractions

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

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: 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.

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.

Type de vérification dans Compiler Frontend

Couvre l'implémentation d'un vérificateur de type dans la façade du compilateur.

Programmation fonctionnelle en Python

Couvre les concepts de programmation fonctionnelle en Python, montrant des listes de filtrage basées sur des critères spécifiques.

Raisonnement automatisé dans la pratique

Explore les systèmes de raisonnement automatisés pratiques comme TPTP, TSTP et CASC, en soulignant l'importance de la cohérence et des développements futurs.

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.

Analyse des noms : Phases de compilation et tableaux de symboles

Explore les phases du compilateur et le rôle des tables de symboles dans le mappage des variables vers les déclarations.

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.

Programmation par flux : conversion de température

Démontre la conversion de température de Fahrenheit en Celsius en utilisant des flux Java et des expressions lambda.

Laboratoire de vérification de type

Se concentre sur la mise en œuvre d'un vérificateur de type pour Amy, couvrant l'analyse des noms et des types, la génération de contraintes de frappe et l'importance de la vérification de type dans la compilation.