TY  - BOOK
AU  - Timoshenko, S.
AU  - Young, D.H.
TI  - Théorie des Constructions
U1  - 624.176  
PY  - 1945///
CY  - París - Francia
PB  - Librairie Polytechnique Charles Béranger
KW  - FRANCIA
N1  - Sala general / a domicilio
N2  - L'objet de cette thèse est la méta-théorie du Calcul des Constructions Inductives (CCI), c'est à dire les Calcul des Constructions étendu par des types et des prédicats inductifs. Le Calcul des Constructions a été présenté en 1985 par Thierry Coquand. Il s'agit d'un lambda-calcul typé qui, à travers l'isomorphisme dit de Curry-Howard, peut-être vu comme un formalisme logique. Ce système qui étend à la fois la logique d'ordre superieur de Church et les systèmes de Martin-Löf est particulièrement expressif du point de vue algorithmique et peut facilement être mis en oeuvre sur ordinateur
ER  -