@INPROCEEDINGS { AUTHOR = "Pierre-Evariste Dagand and Nicolas Tabareau and {\'E}ric Tanter", TITLE = "Partial Type Equivalences for Verified Dependent Interoperability", BOOKTITLE = "21st International Conference on Functional Programming (ICFP)", PAGES = "298-310", MONTH = "Sep", YEAR = "2016", ADDRESS = "Nara, Japan", PUBLISHER = "ACM Press", }