Table des matières
8 relations: Assistant de preuve, Correspondance de Curry-Howard, Lambda-calcul, Langage formel, Nicolaas Govert de Bruijn, Substitution explicite, Théorie complète, Type dépendant.
- Théorie des types
Assistant de preuve
En informatique (ou en mathématiques assistées par informatique), un assistant de preuve est un logiciel permettant la vérification de preuves mathématiques, soit sur des théorèmes au sens usuel des mathématiques, soit sur des assertions relatives à l'exécution de programmes informatiques.
Voir Automath et Assistant de preuve
Correspondance de Curry-Howard
La correspondance de Curry-Howard, appelée également isomorphisme de Curry-de Bruijn-Howard, correspondance preuve/programme ou correspondance formule/type, est une série de résultats à la frontière entre la logique mathématique, l'informatique théorique et la théorie de la calculabilité.
Voir Automath et Correspondance de Curry-Howard
Lambda-calcul
Le lambda-calcul (ou λ-calcul) est un système formel inventé par Alonzo Church dans les années 1930, qui fonde les concepts de fonction et d'application.
Voir Automath et Lambda-calcul
Langage formel
Un langage formel, en mathématiques, en informatique et en linguistique, est un ensemble de mots.
Voir Automath et Langage formel
Nicolaas Govert de Bruijn
Nicolaas Govert de Bruijn, né le à La Haye et mort le à Nuenen, est un mathématicien néerlandais, professeur émérite de l'université de technologie d'Eindhoven.
Voir Automath et Nicolaas Govert de Bruijn
Substitution explicite
Ms est la notation d'une substitution explicite Un calcul de substitutions explicites est une extension du lambda-calcul dans lequel la substitution est intégrée au calcul au même titre que le sont l'abstraction ou l'application, alors que dans le lambda-calcul, la substitution fait partie de la métathéorie, c'est-à-dire qu'elle est définie en dehors de la théorie du lambda-calcul.
Voir Automath et Substitution explicite
Théorie complète
En logique mathématique, une théorie complète est une théorie qui est équivalente à un ensemble maximal cohérent de propositions; ceci signifie qu'elle est cohérente et que toute extension propre ne l'est plus.
Voir Automath et Théorie complète
Type dépendant
En Informatique et en Logique, un type dépendant est un type qui peut dépendre d'une valeur définie dans le langage typé.
Voir Automath et Type dépendant
Voir aussi
Théorie des types
- Automath
- Calcul des constructions
- Conversion de type
- Correspondance de Curry-Howard
- Couple (mathématiques)
- Duck typing
- Inférence de types
- Lambda cube
- Lambda-calcul simplement typé
- New Foundations
- Polymorphisme (informatique)
- Principe de substitution de Liskov
- Principe ouvert/fermé
- Programmation orientée prototype
- Sûreté du typage
- Signature de type
- Structure (mathématiques)
- Système F
- Système U (mathématiques)
- Théorie des types
- Théorie des types homotopiques
- Trait (programmation)
- Type énuméré
- Type abstrait
- Type algébrique de données
- Type algébrique généralisé
- Type dépendant
- Type produit
- Type récursif
- Type somme
- Type unité
- Type vide
- Unification
- Uplet
- Variable (informatique)
- Void