Efficient and Flexible Matching of Recursive Types

Equality and subtyping of recursive types have been studied in the 1990s by Amadio and Cardelli; Kozen, Palsberg, and Schwartzbach; Brandt and Henglein; and others. Potential applications include automatic generation of bridge code for multi-language systems and typebased retrieval of software modules from libraries. In this paper, we present an efficient decision procedure for a notion of type equality that includes unfolding of recursive types, and associativity and commutativity of product types. Advocated by Auerbach, Barton, and Raghavachari, these properties enable flexible matching of types. For two types of size at most n, our algorithm takes O(n) iterations each of which takes O(n) time, for a total of O(n2) time.

• Type: Conference
• Year: 2000
• Where: LICS
• Authors: Jens Palsberg, Tian Zhao
• Keywords: Automated Reasoning, Efficient Decision Procedure, Enable Flexible Matching, LICS 2000, Recursive Types