Isomorphisms of Types

1 Introduction.- 1.1 What is a type?.- 1.2 Types in mathematical logic.- 1.3 Types for programming.- 1.4 Exploring typed ?-calculi.- 1.5 The typed ? -calculi used in this work.- 1.6 The Curry-Howard Isomorphism.- 1.7 Using types to classify and retrieve software.- 1.8 When are two types equal?.- 1.9 Isomorphisms and the lambda calculus.- 2 Confluence Results.- 2.1 Introduction.- 2.2 Extensionality.- 2.3 Overview.- 2.4 Confluence.- 2.5 Weak normalization.- 2.6 Decidability and conservative extension results.- 2.7 Other related works.- 3 Strong normalization results.- 3.1 Normalization without ?2 on gentop n.f.’s.- 3.2 Normalization without ?top and SPtop.- 4 First-Order Isomorphic Types.- 4.1 Rewriting types.- 4.2 From ?1???? to the classical ?1??.- 4.3 Using finite hereditary permutations.- 4.4 The complete theories of ?1??? and ?1???.- 5 Second-Order Isomorphic Types.- 5.1 Towards completeness.- 5.2 Characterizing canonical terms.- 5.3 Completeness for isomorphisms.- 5.4 Decidability of the equational theory.- 5.5 The complete theories of ?2??? and ?2???.- A Properties of n-tuples.- B Technical lemmas.- C Miscellanea.- 6 Isomorphisms for ML.- 6.1 Introduction.- 6.2 Isomorphisms of types in ML-style languages.- 6.3 Completeness and conservativity results.- 6.4 Deciding ML isomorphism.- 6.5 Adding isomorphisms to the ML type-checker.- 6.6 Conclusion.- 6.7 Some technical Lemmas.- 6.8 Completeness.- 6.9 Conservativity.- 7 Related Works, Future Perspectives.- 7.1 Equational matching of types.- 7.2 Using equational unification.- 7.3 Extending the paradigm.- 7.4 Future work and perspectives.- Citation Index.