Home >

news Help

Publication Information


Title
Japanese: 
English:Unification Modulo Isomorphisms between Dependent Types for Type-based Library Search 
Author
Japanese: 瀧本 哲史, 森口 草介, 渡部 卓雄.  
English: Satoshi Takimoto, Sosuke Moriguchi, Takuo Watanabe.  
Language English 
Journal/Book name
Japanese: 
English: 
Volume, Number, Page         (to appear)
Published date Oct. 12, 2025 
Publisher
Japanese: 
English: 
Conference name
Japanese: 
English:10th ACM SIGPLAN International Workshop on Type-Driven Development (TyDe 2025) 
Conference site
Japanese: 
English: 
Abstract Type-based library search allows developers to efficiently find reusable software components by their type signatures, as exemplified by tools like Hoogle. This capability is especially important in interactive theorem provers (ITPs), where reusing existing proofs can greatly accelerate development. Previous type-based library search tools for ITPs, such as SearchIsos and Loogle, support only a subset of desirable search flexibilities, including argument reordering, currying/uncurrying, generalisation, and the inclusion of extra premises. However, none can handle all these flexibilities simultaneously, resulting in missed relevant matches. In this work, we propose a type-based library search method based on equational unification modulo a set of type isomorphisms for dependent product/sum types, enabling all the desired search flexibilities. We present a semi-algorithm for this equational unification and provide a prototype implementation to demonstrate the feasibility of our approach.

©2007 Institute of Science Tokyo All rights reserved.