Sémantique preuves et programmation

Domaine : Informatique-Maths applis

Etablissement principal: Univ. PARIS 7

Etablissements cohabilités :

• ENS PARIS
• Univ. PARIS 6
• Univ. PARIS SUD
• POLYTECHNIQUE PALAISEAU
• CNAM PARIS

Programme :

Tronc commun (120h d'enseignement) : Structures syntaxiques pour le calcul - Preuves constructives - Logique et modèles de Herbrand - Récursivité et introduction à la théorie des catégories et des domaines - Sémantique dénotationnelle des langages de programmation - Typage et programmation.

Filière Langage / Filière Modèles Sémantiques / Filière Preuves et Spécifications :

Mots-clés:

• programmation
• ordre logique
• sémantique
• preuve
• spécification
• interprétation abstraite
• lambda
• calcul
• types
• systèmes finis
• théorie des domaines
• logique linéaire
• méthodes de développement de logiciels
• modularité

Responsable de la formation: M. Guy COUSINEAU

Adresse:
2 Place Jussieu Boîte Courrier interne 7024
75251 PARIS cedex 05
Tél : (1) 44 27 57 77 - Fax :(1) 44 27 28 50

Numéro du DEA : 307