The Expressiveness of Simple and Second-Order Type Structures

Abstract

Typed lambda (?`-) calculi provtde convement mathematical settings in which to investigate the effects of type structure on the function definmon mechamsm m programming languages. Lambda expressaons mtm~c programs that do not use while loops or carcular function definitions. Two typed ?`-calculi are investigated, the sunply typed ?`-calculus, whose types are similar to Pascal types, and the second-order typed ?,-calculus, which has a type abstractaon mechamsm simdar to that of modern data abstraction languages such as ALPHARD. Two related questions are considered for each calculus: