[FOM] Martin-Lof predicativity

[Steve Stevenson]

>> Per Martin-Löf, An intuitionistic theory of types: Predicative  
>> part. In
>> H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium `73,  
>> pages
>> 73-118. North-Holland, 1975.


This is the standard starting point for all the current work in types  
in programming languages. ML, OCaml, Haskell, etc are all based on  
these ideas.

best regards,

steve
--------
D. E. Stevenson, Department of Computer Science
Director, Institute for Modeling and Simulation Applications
Clemson University, Clemson, SC 29634-0974
864.656.5880 http://www.cs.clemson.edu/~steve