Martin-Löf's Type Theory Export

@incollection{nordstrom:mltt, abstract = {ionb 2 B [x 2 A]([x]b) 2 (x 2 A)BWe will write repeated abstractions as [x 1 ; x 2 ; : : : ; xn ]b and also excludethe outermost parentheses when there is no risk of confusion.How do we know that this rule is correct, i.e. how do we know that [x]bis a function of the type (x 2 A)B? By the semantics of function types,we must know that when we apply [x]b of type (x 2 A)B on an object aof type A, then we get an object of type B[x / a]; the explanation is byfi-conversion:...}, author = {Nordstr\"{o}m, B. and Petersson, K. and Smith, J. M.}, booktitle = {The Handbook of Logic in Computer Science}, citeulike-article-id = {500657}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.8084}, keywords = {dependent-types, logic, type-theory}, month = {October}, posted-at = {2009-03-28 23:10:08}, priority = {3}, publisher = {Oxford University Press}, title = {Martin-L\"{o}f's Type Theory}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.8084}, volume = {5}, year = {2000} }

TY - CHAP ID - nordstrom:mltt L3 - citeulike-article-id:500657 N2 - ionb 2 B [x 2 A]([x]b) 2 (x 2 A)BWe will write repeated abstractions as [x 1 ; x 2 ; : : : ; xn ]b and also excludethe outermost parentheses when there is no risk of confusion.How do we know that this rule is correct, i.e. how do we know that [x]bis a function of the type (x 2 A)B? By the semantics of function types,we must know that when we apply [x]b of type (x 2 A)B on an object aof type A, then we get an object of type B[x / a]; the explanation is byfi-conversion:... TI - Martin-Löf's Type Theory PB - Oxford University Press VL - 5 T2 - The Handbook of Logic in Computer Science KW - dependent-types KW - logic KW - type-theory AU - Nordström, B AU - Petersson, K AU - Smith, JM PY - 2000/10// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.8084 ER -