CiteULike Search Register Log in
CiteULike is a free online bibliography manager. Register and you can start organising your references online.

Martin-Löf's Type Theory

by: B. Nordström, K. Petersson, J. M. Smith

X Abstract

ion b 2 B [x 2 A] ([x]b) 2 (x 2 A)B We will write repeated abstractions as [x 1 ; x 2 ; : : : ; xn ]b and also exclude the 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]b is 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 a of type A, then we get an object of type B[x / a]; the explanation is by fi-conversion:...

View the full article here:

CiteSeerX Beta

This article has been bookmarked 3 times, initially on 2006-02-10.

2009-03-28 Group Lambda the Ultimate
Group functional programming
2006-02-10 User kontakte
Privacy Statement | Terms & Conditions
CiteULike organises scholarly (or academic) papers or literature and provides bibliographic (which means it makes bibliographies) for universities and higher education establishments. It helps undergraduates and postgraduates. People studying for PhDs or in postdoctoral (postdoc) positions. The service is similar in scope to EndNote or RefWorks or any other reference manager like BibTeX, but it is a social bookmarking service for scientists and humanities researchers.