Verwandte Artikel zu Isomorphisms of Types: from ?-calculus to information...
Zu dieser ISBN ist aktuell kein Angebot verfügbar.
Inhaltsangabe
1 Introduction.- 1.1 What is a type?.- 1.2 Types in mathematical logic.- 1.3 Types for programming.- 1.3.1 Imperative languages.- 1.3.2 Limits of static type-checking.- 1.3.3 Functional languages.- 1.3.4 The lambda calculus.- 1.4 Exploring typed ?-calculi.- 1.4.1 Church-style types.- 1.4.2 Curry-style types.- 1.4.3 Explicit polymorphic types.- 1.4.4 Implicit polymorphic types.- 1.5 The typed ? -calculi used in this work.- 1.5.1 The calculus ?2????.- 1.5.2 General notations for terms and substitutions.- 1.6 The Curry-Howard Isomorphism.- 1.7 Using types to classify and retrieve software.- 1.7.1 Object-oriented languages.- 1.7.2 Functional languages.- 1.8 When are two types equal?.- 1.8.1 Isomorphic types.- 1.8.2 Isomorphisms in category theory.- 1.8.3 Digression: Tarski's High School Algebra Problem.- 1.8.4 Isomorphisms in logic.- 1.9 Isomorphisms and the lambda calculus.- 1.9.1 Isomorphisms and invertibility.- 1.9.2 The theories of isomorphisms for typed ?-calculi.- 1.9.3 Soundness.- 2 Confluence Results.- 2.1 Introduction.- 2.2 Extensionality.- 2.2.1 Survey.- 2.3 Overview.- 2.3.1 Weakly confluent reduction.- 2.3.2 Investigating strong normalization.- 2.3.3 A general criterion for confluence.- 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.1.1 Reducibility with parameters.- 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.1.1 Outline of the section.- 5.1.2 Reduction to a subclass of types.- 5.1.3 Reduction to a subclass of terms.- 5.2 Characterizing canonical terms.- 5.2.1 Outline of the section.- 5.2.2 Projection of invertibility over coordinates.- 5.2.3 Reduction of coordinates to ?2??.- 5.2.4 Syntactic characterization of canonical bijections.- 5.3 Completeness for isomorphisms.- 5.3.1 Uniform isomorphisms.- 5.4 Decidability of the equational theory.- 5.5 The complete theories of ?2??? and ?2???.- 5.6 Conclusions.- 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.2.1 A formal setting for valid isomorphisms in ML-like languages.- 6.3 Completeness and conservativity results.- 6.3.1 Completeness.- 6.3.2 Relating Th2xT and ThML.- 6.4 Deciding ML isomorphism.- 6.4.1 An improved decision procedure.- 6.4.2 Equality as unification with variable renamings.- 6.4.3 Dynamic programming.- 6.4.4 Experimental results.- 6.5 Adding isomorphisms to the ML type-checker.- 6.5.1 Type-inference with just (Split).- 6.5.2 What is special in (Split).- 6.5.3 Choosing the right isomorphisms.- 6.5.4 Right isomorphisms in impure context.- 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.1.1 Decomposing the matching problem.- 7.2 Using equational unification.- 7.3 Extending the paradigm.- 7.3.1 Searching through type classes.- 7.3.2 Searching with more powerful specifications.- 7.3.3 Recursive terms and types.- 7.3.4 Other applications of type isomorphisms.- 7.4 Future work and perspectives.- 7.4.1 Design of type systems for functional languages.- 7.4.2 Object retrieval in object-oriented libraries.- 7.4.3 Dynamic composition of software components.- 7.4.4 Representation optimization.- Citation Index.
Die Inhaltsangabe kann sich auf eine andere Ausgabe dieses Titels beziehen.
(Keine Angebote verfügbar)
Buch Finden: Kaufgesuch aufgebenSie finden Ihr gewünschtes Buch nicht? Wir suchen weiter für Sie. Sobald einer unserer Buchverkäufer das Buch bei AbeBooks anbietet, werden wir Sie informieren!
Kaufgesuch aufgeben
