- Author:
- Roberto Di Cosmo
No abstract available.
Cited By
Levy P (2017). Contextual isomorphisms, ACM SIGPLAN Notices, 52:1, (400-414), Online publication date: 11-May-2017.- Levy P Contextual isomorphisms Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, (400-414)
- Castagna G, Gesbert N and Padovani L (2009). A theory of contracts for Web services, ACM Transactions on Programming Languages and Systems, 31:5, (1-61), Online publication date: 1-Jun-2009.
- Ruehr F Tips on teaching types and functions Proceedings of the 2008 international workshop on Functional and declarative programming in education, (79-90)
- Castagna G, Gesbert N and Padovani L (2008). A theory of contracts for web services, ACM SIGPLAN Notices, 43:1, (261-272), Online publication date: 14-Jan-2008.
- Castagna G, Gesbert N and Padovani L A theory of contracts for web services Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (261-272)
- Di Cosmo R, Pottier F and Rémy D Subtyping recursive types modulo associative commutative products Proceedings of the 7th international conference on Typed Lambda Calculi and Applications, (179-193)
- Asperti A, Guidi F, Coen C, Tassi E and Zacchiroli S A content based mathematical search engine Proceedings of the 2004 international conference on Types for Proofs and Programs, (17-32)
- Fiore M (2004). Isomorphisms of generic recursive polynomial types, ACM SIGPLAN Notices, 39:1, (77-88), Online publication date: 1-Jan-2004.
- Fiore M Isomorphisms of generic recursive polynomial types Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (77-88)
- Zibin Y, Gil J and Considine J (2003). Efficient algorithms for isomorphisms of simple types, ACM SIGPLAN Notices, 38:1, (160-171), Online publication date: 15-Jan-2003.
- Zibin Y, Gil J and Considine J Efficient algorithms for isomorphisms of simple types Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (160-171)
- Herrmann C and Lengauer C A transformational approach which combines size inference and program optimization Proceedings of the 2nd international conference on Semantics, applications, and implementation of program generation, (199-218)
- Wan Z, Taha W and Hudak P (2001). Real-time FRP, ACM SIGPLAN Notices, 36:10, (146-156), Online publication date: 1-Oct-2001.
- Wan Z, Taha W and Hudak P Real-time FRP Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, (146-156)
- Gil J (2001). Subtyping arithmetical types, ACM SIGPLAN Notices, 36:3, (276-289), Online publication date: 1-Mar-2001.
- Gil J Subtyping arithmetical types Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (276-289)
- Delahaye D A tactic language for the system Coq Proceedings of the 7th international conference on Logic for programming and automated reasoning, (85-95)
- Fischer B (2000). Specification-Based Browsing of Software Component Libraries, Automated Software Engineering, 7:2, (179-200), Online publication date: 1-May-2000.
- Spławski Z and Urzyczyn P (1999). Type fixpoints, ACM SIGPLAN Notices, 34:9, (102-113), Online publication date: 1-Sep-1999.
- Spławski Z and Urzyczyn P Type fixpoints Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, (102-113)
- Taha W and Sheard T (1997). Multi-stage programming with explicit annotations, ACM SIGPLAN Notices, 32:12, (203-217), Online publication date: 1-Dec-1997.
- Sheard T (1997). A type-directed, on-line, partial evaluator for a polymorphic language, ACM SIGPLAN Notices, 32:12, (22-35), Online publication date: 1-Dec-1997.
- Taha W and Sheard T Multi-stage programming with explicit annotations Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, (203-217)
- Sheard T A type-directed, on-line, partial evaluator for a polymorphic language Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, (22-35)
Index Terms
- Isomorphisms of types: from λ-calculus to information retrieval and language design
Recommendations
Review of Isomorphisms of Types:: from λ-calculus to information retrieval and language design by Roberto Di Cosmo (Birkhauser, 1995)
The λ-calculus is an elegant computational model used extensively in the formal semantics of programming languages. It was first described by Alonzo Church in 1932, as a foundation of mathematics based not on sets, but directly on functions. λ-calculus was, ...
Isomorphisms of generic recursive polynomial types
POPL '04This paper gives the first decidability results on type isomorphism for recursive types, establishing the explicit decidability of type isomorphism for the type theory of sums and products over an inhabited generic recursive polynomial type. The ...
On isomorphisms of intersection types
The study of type isomorphisms for different λ-calculi started over twenty years ago, and a very wide body of knowledge has been established, both in terms of results and in terms of techniques. A notable missing piece of the puzzle was the ...
Reviews
Gunther W. Schmidt
The author presents a theory of isomorphisms of types using several variations of the well-known typed lambda-calculus, up to a second-order lambda-calculus with explicit pairs and unit type. This theory turns out to have valuable applications in programming language design and information retrieval systems for functional software libraries. The first three chapters introduce the basic concepts used in the book, such as explicit and implicit typing, the Curry-Howard isomorphism, basic notation in category theory, confluence, and strong normalization. Chapter 4 deals with first-order isomorphic types, including the decidability of isomorphisms in several variations of an explicitly typed first-order lambda-calculus. In the same manner, chapter 5 deals with second-order isomorphic types. Chapter 6 has a twofold purpose. Isomorphisms of an ML-style language (with implicit typing) are investigated and related to the results of chapter 5. It also presents an implementation of a search algorithm in a software library system based on the theory above. This algorithm is implemented in CAML. This book is for both theoreticians and practitioners. It contains an extensive bibliography and several detailed indices. Except for the description of CAML, the book is self-contained. It may be used as a supplementary book for graduate courses on lambda-calculi . The book is a valuable contribution to the theory of typed lambda-calculi. It is one of the few that combines the theoretical and practical aspects of isomorphic types in a comprehensive way.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.