Déduction avec sortes ordonnées et égalités - Université de Lorraine Accéder directement au contenu
Thèse Année : 1995

Déduction avec sortes ordonnées et égalités

Résumé

Non disponible / Not available
Cette thèse est dédiée au développement de langages de spécification formels, de leur sémantique opérationnelle sous forme de systèmes de réécriture décorés et des outils de preuves associés. Nous définissons les logiques Rn et Gn, qui sont des logiques à clauses de Horn égalitaires avec prédicat d'appartenance, adaptées à la spécification et à la programmation polymorphique d'ordre supérieur avec sous-typage dynamique et paramétrique, des fonctions strictes et partielles et une sémantique initiale basée sur la théorie des ensembles. Puis, nous introduisons les termes décorés, qui représentent une structure de données bien adaptées aux spécifications et programmes équationnels types. Ils permettent d'intégrer le raisonnement égalitaire, les fonctions partielles et le typage dynamique de termes
Fichier principal
Vignette du fichier
SCD_T_1995_0182_HINTERMEIER.pdf (8.82 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

tel-01753499 , version 1 (29-03-2018)

Identifiants

  • HAL Id : tel-01753499 , version 1

Citer

Claus Hintermeier. Déduction avec sortes ordonnées et égalités. Informatique [cs]. Université Henri Poincaré - Nancy 1, 1995. Français. ⟨NNT : 1995NAN10182⟩. ⟨tel-01753499⟩
33 Consultations
96 Téléchargements

Partager

Gmail Facebook X LinkedIn More