Isomorphisms of Types from ?-calculus to information retrieval and language design
This is a book about isomorphisms 0/ types, arecent difficult research topic in type theory that turned out to be able to have valuable practical applications both for programming language design and far more human centered information retrieval in software libraries. By means of a deep study of th...
| Main Author: | |
|---|---|
| Format: | eBook |
| Language: | English |
| Published: |
Boston, MA
Birkhäuser
1995, 1995
|
| Edition: | 1st ed. 1995 |
| Series: | Progress in Theoretical Computer Science
|
| Subjects: | |
| Online Access: | |
| Collection: | Springer Book Archives -2004 - Collection details see MPG.ReNa |
Table of Contents:
- 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