|
Scheda bibliografica proveniente da importazione di metadati da altro sistema |
Tipo: |
Testo a stampa, Risorsa analitica |
É contributo di: |
Optimization techniques |
Titolo: |
Induction principles formalized in the calculus of constructions |
Pubblicazione: |
Berlin ; Heidelberg ; New York : Springer, 1975 |
Descrizione fisica: |
276-286 |
Titolo uniforme: |
Optimization techniques |
Numeri standard: |
DOI 10.1007/3-540-17660-8_62 |
Sommario o abstract: |
The Calculus of Constructions is a higher-order formalism for writing constructive proofs in a natural deduction style, inspired from work of de Bruijn [2,3], Girard [12], Martin-L+Âf[14] and Scott [18]. The calculus and its syntactic theory were presented in Coquand's thesis [7], and an implementation by the author was used to mechanically verify a substantial number of proofs demonstrating the power of expression of the formalism [9]. The Calculus of Constructions is proposed as a foundation for the design of programming environments where programs are developed consistently with formal specifications. The current paper shows how to define inductive concepts in the calculus |
Altra responsabilità: |
G. + Huet |
Classificazione Dewey: |
519.7 ed.22 Programmazione |
Lingua della pubblicazione: |
Inglese |
Paese di pubblicazione: |
Germania ; Stati Uniti d'America |
Codice identificativo: |
IT/ItRC/00017620 |
data di importazione: |
01-01-2014 |
|
Full text |