Recursive types (subtyping; isomorphism; axiomatization; inference)

Academic Journals

1. Yossi Gil, Yoav Zibin. Randomised algorithms for isomorphisms of simple types. Mathematical Structures in Computer Science (MSCS), 17(3):565-584, June 2007. download
2. Roberto Di Cosmo. A short survey of isomorphisms of types. Mathematical Structures in Computer Science, 15(5):825-838, 2005.
3. Yossi Gil, Yoav Zibin. Efficient algorithms for isomorphisms of simple types. Mathematical Structures in Computer Science (MSCS), 15(5):917-957, October 2005. download
4. Marcelo Fiore. Isomorphisms of generic recursive polynomial types. SIGPLAN Not, 39(1):77-88, 2004. download
5. Vladimir Gapeyev, Michael Y. Levin, Benjamin C. Pierce. Recursive subtyping revealed. J. Funct. Program, 12(6):511-548, 2002.
6. Alexandre Frey. Satisfying subtype inequalities in polynomial space. Theoretical Computer Science, 277(1):105-117, April 2002.
7. Michael Brandt, Fritz Henglein. Coinductive axiomatization of recursive type equality and subtyping. Fundamenta Informaticae, Invited submission to special issue featuring a selection of contributions to the 3d Int'l Conf. on Typed Lambda Calculi and Applications (TLCA), 1997, 33(4):309-338, 1998.
8. Marcelo P. Fiore. A Coinduction Principle for Recursive Data Types Based on Bisimulation. Information and Computation, Conference version: Proc.\ 8th Annual IEEE Symp.\ on Logic in Computer Science (LICS), 1993, pp.\ 110-119, 127:186-198, 1996.
9. F. Cardone, M. Coppo. Type Inference with Recursive Types: Syntax and Semantics. Information and Computation, 92(1):48-80, May 1991.
10. D. MacQueen, G. Plotkin, R. Sethi. An Ideal Model for Recursive Polymorphic Types. Information and Control, 71, 1986.

Book Chapters

1. Sian Jha, Jens Palsberg, Tian Zhao, Fritz Henglein. Efficient Type Matching. In Automatic Program Development-A Tribute to Robert Paige, Springer Netherlands, 2008.
2. Oscar Nierstrasz. Regular Types for Active Objects. In Object-Oriented Software Composition, O. Nierstrasz, D. Tsichritzis (eds.), pp. 99-121, Prentice Hall, 1995.

International Conferences

1. Roberto Di Cosmo, Francois Pottier, Didier Remy. Subtyping recursive types modulo associative commutative products. In Proc. Seventh International Conference on Typed Lambda Calculi and Applications (TLCA 2005), 2005.
2. Vladimir Gapeyev, Benjamin C. Pierce. Regular Object Types. In ECOOP, Pages 151-175, 2003.
3. Yoav Zibin, Joseph Gil, Jeffrey Considine. Efficient Algorithms for Isomorphisms of Simple Types. In Proc. 30th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), SIGPLAN Notices, Vol. 38, No. 1, Pages 160-171, January 2003.
4. Joseph Gil. Subtyping arithmetical types. In POPL, Pages 276-289, 2001.
5. Vladimir Gapeyev, Michael Y. Levin, Benjamin C. Pierce. Recursive subtyping revealed: (functional pearl). In ICFP '00: Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, Pages 221-231, New York, NY, USA, 2000. download
6. Joshua S. Auerbach, Charles Barton, Mark Chu-Carroll, Mukund Raghavachari. Mockingbird: Flexible Stub Compilation from Pairs of Declarations. In ICDCS, Pages 393-402, 1999. download
7. Fritz Henglein, Jakob Rehof. Constraint Automata and the Complexity of Recursive Subtype Entailment. In ICALP, Pages 616-627, July 1998.
8. Michael Brandt, Fritz Henglein. Coinductive Axiomatization of Recursive Type Equality and Subtyping. In TLCA, Pages 63-81, 1997.
9. Fritz Henglein, Jakob Rehof. The Complexity of Subtype Entailment for Simple Types. In Proc.\ 12th Annual IEEE Symposium on Logic in Computer Science (LICS), Warsaw, Poland, Pages 352-361, July 1997.
10. Mart\'\in Abadi, Marcelo P. Fiore. Syntactic Considerations on Recursive Types. In Proc. 1996 IEEE 11th Annual Symp. on Logic in Computer Science (LICS), New Brunswick, New Jersey, June 1996.
11. Pawel Urzyczyn. Positive Recursive Type Assignment. In Proc. Mathematical Foundations of Computer Science (MFCS), Prague, Czech Republic, Lecture Notes in Computer Science, This is an updated version dated January 5, 1996, 1995.
12. Jens Palsberg, Patrick O'Keefe. A Type System Equivalent to Flow Analysis. In Proc. 22nd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL), San Francisco, California, Pages 367-378, acmpubs@acm.org, January 1995.
13. Samson Abramsky, Guy McCusker. Games for Recursive Types. In Theory and Formal Methods, Pages 1-20, 1994.
14. Tatsurou Sekiguchi, Akinori Yonezawa. A Complete Type Inference System for Subtyped Recursive Types. In Proc.\ Int'l Symp.\ Theoretical Aspects of Computer Science (TACS), Sendai, Japan, Masami Hagiya, John C. Mitchell (eds.), Lecture Notes in Computer Science, Volume 789, Pages 667-686, April 1994.
15. Flemming Damm. Subtyping with Union Types, Intersection Types and Recursive Types. In Proc. Theoretical Aspects of Computer Science (TACS), Sendai, Japan, Lecture Notes in Computer Science, Volume 789, Pages 687-706, April 1994.
16. Thierry Coquand. Infinite Objects in Type Theory. In Proc.\ Int'l Workshop on Types for Proofs and Programs (TYPES), Henk Barendregt, Tobias Nipkow (eds.), Lecture Notes in Computer Science (LNCS), Volume 806, Pages 62-78, May 1993.
17. F. Cardone. An Algebraic Approach to the Interpretation of Recursive Types. In Proc. 17th Coll. on Trees in Algebra and Programming (CAAP), Rennes, France, J.-C. Raoult (ed.), Lecture Notes in Computer Science, Vol. 581, Pages 66-85, February 1992.
18. R. Cosmo. Type Isomorphisms in a Type-Assignment Framework. In Proc. 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programmin gLanguages (POPL), Albuquerque, New Mexico, Pages 200-210, January 1992.
19. P. Curien, G. Ghelli. Subtyping + Extensionality: Confluence of $\beta \eta$top Reduction in F$_\leq$. In Proc. Int'l Conf. on Theoretical Aspects of Computer Software (TACS), Sendai, Japan, Lecture Notes in Computer Science, Vol. 526, September 1991.
20. Satish Thatte. Coercive Type Equivalence. In Proc. Conf. on Functional Programming Languages and Computer Architecture (FPCA), Cambridge, Massachusetts, Lecture Notes in Computer Science, Vol. 523, Pages 406-426, August 1991.
21. R. Amadio, L. Cardelli. Subtyping Recursive Types. In Proc. 18th Annual ACM Symposium on Principles of Programming Languages (POPL), Orlando, Florida, Pages 104-118, January 1991.
22. P. Curien, G. Ghelli. Coherence of Subsumption. In Proc. 15th Coll. on Trees in Algebra and Programming (CAAP), Copenhagen, Denmark, A. Arnold (ed.), Lecture Notes in Computer Science (LNCS), Volume 431, Pages 132-146, May 1990.
23. S. Cosmadakis. Computing with Recursive Types. In Proc. 1989 IEEE 4th Annual Symp. on Logic in Computer Science (LICS), Pages 24-38, 1989.
24. N. Mendler. Recursive Types and Type Constraints in Second-Order Lambda Calculus. In Proc. Symp. on Logic in Computer Science (LICS), Pages 30-36, 1987.
25. M. Coppo. A Compeleteness Theorem for Recursively Defined Types. In Proc. ?, Lecture Notes in Computer Science, Pages 120-129, 1985.
26. R. Cartwright. Types as Intervals. In Proc. 12th ACM Symp. on Principles of Programming Languages, Pages 22-36, New Orleans, Louisiana, January 1985.
27. Marvin Solomon. Type definitions with parameters. In POPL '78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, Pages 31-38, New York, NY, USA, January 1978. download

Technical Reports

1. Sian Jha, Jens Palsberg, Tian Zhao, Fritz Henglein. Efficient Type Matching. TOPPS Report D-474 Department of Computer Science, University of Copenhagen (DIKU), 2002.
2. Joshua Auerbach, Charles Barton, Mukund Raghavachari. Type Isomorphisms with Recursive Types. Technical Report IBM Research, No 0, 1998.
3. Alexander Andreev, Sergei Soloviev. A Decison Algorithm for Linear Isomorphism of Types with Complexity $Cn(\log^2(n))$. Research Report BRICS, Aarhus University, Denmark, No 0, November 1996.
4. Hans Lei\ss. Combining Recursive and Dynamic Types. Research Report CIS, Universit\"at M\"unchen, No 92, October 1992.
5. R. Cartwright. Types as Intervals. Research Report Rice University, No 84, 1984.

Miscellaneous

1. Lars Birkedal, Robert Harper. Relational Interpretations of Recursive Types in an Operational Setting (Summary). Manuscript, 1998.
2. Luca Cardelli. Algorithm for subtyping recursive types (in Modula-3). http://research.microsoft.com/research/cambridge/luca/Notes/RecSub.txt, 1993.

Dissertations

1. Clemens Grabmayer. Relating Proof Systems for Recursive Types. PhD Thesis Vrije Universiteit Amsterdam, 2005.

Master's thesis

1. Michael Brandt. Recursive Subtyping: Axiomatizations and Computational Interpretations. Master's theses DIKU, University of Copenhagen, Universitetsparken 1, DK-2100 Copenhagen, Denmark, April 1997.

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.