Lambda-calcul : types et modèles / Jean-Louis Krivine,... [ Livre]

Auteur principal: Krivine, Jean-LouisLangue: Français.Publication : Paris, Milan, Barcelone : Masson, 1990Description : VIII-176 p. ; 25 cmISBN: 2225820910.Collection: Etudes et recherches en informatique, 0763-2770Classification: F 4 1 Logique mathématiqueRésumé: Résumé Le Lambda-calcul a été inventé vers 1930, par A. Church, et a connu en développement considérable. Depuis un quizaine d'années, le lambda-calcul typé tout particulièrement suscite un grand intérêt, à cause de ses rapports étroits avec les langages de programmation, et du lien qu'il établit entre les notions de programme et de preuve en logique intuitionniste : c'est ce qu'on appelle la "correspondance du Curry-Howard". Ce livre est une introduction à certains des aspects que présente maintenant cette théorie : lambda-calcul pur, logique combinatoire, sémantique (modèles) du lambda-calcul, systèmes de types. Tous ces domaines sont abordés dans cet ouvrage d'une façon qui met en lumière leur interdépendance, et l'unité profonde du sujet. Seule une certaine pratique en logique mathématique est requise du lecteur : notion de fonction récursive, et concepts élémentaires du calcul des prédicats et de la théorie des modèles. Sommaire 1. Substitution et bêta-conversion 2. Représentations des fonctions récursives 3. Types avec intersection 4. Typage des termes normalisables 5. Le théorème de Bohm 6. Logique combinatoire 7. Modèles du Lambda calcul 8. Le système F 9. Arithmétique fonctionnelle du second ordre 10. Fonctions représentables dans le système F.Sujet - Nom commun: Mathématiques -- Informatique | Logique symbolique et mathématique | Logique combinatoire | Lambda-calcul
Current location Call number Status Notes Date due Barcode
ENS Rennes - Bibliothèque
Informatique
F 4 1 KRI (Browse shelf) Available F 4 1 Logique mathématique 00001324
ENS Rennes - Bibliothèque
Informatique
F 4 1 KRI (Browse shelf) Available F 4 1 Logique mathématique 00004882

Bibliogr. p. 167-170. Index

Résumé
Le Lambda-calcul a été inventé vers 1930, par A. Church, et a connu en développement considérable.
Depuis un quizaine d'années, le lambda-calcul typé tout particulièrement suscite un grand intérêt, à cause de ses rapports étroits avec les langages de programmation, et du lien qu'il établit entre les notions de programme et de preuve en logique intuitionniste : c'est ce qu'on appelle la "correspondance du Curry-Howard".
Ce livre est une introduction à certains des aspects que présente maintenant cette théorie : lambda-calcul pur, logique combinatoire, sémantique (modèles) du lambda-calcul, systèmes de types.
Tous ces domaines sont abordés dans cet ouvrage d'une façon qui met en lumière leur interdépendance, et l'unité profonde du sujet.
Seule une certaine pratique en logique mathématique est requise du lecteur : notion de fonction récursive, et concepts élémentaires du calcul des prédicats et de la théorie des modèles.
Sommaire
1. Substitution et bêta-conversion
2. Représentations des fonctions récursives
3. Types avec intersection
4. Typage des termes normalisables
5. Le théorème de Bohm
6. Logique combinatoire
7. Modèles du Lambda calcul
8. Le système F
9. Arithmétique fonctionnelle du second ordre
10. Fonctions représentables dans le système F

Powered by Koha