Transport via Partial Galois Connections and Equivalences

TL;DR

This paper introduces a new framework for transporting programs across different type representations using partial Galois connections and equivalences, applicable within simple type theory and formalized in Isabelle/HOL.

Contribution

It generalizes previous transport approaches by introducing partial Galois connections and equivalences, suitable for simple type theory and formalized in Isabelle/HOL.

Findings

Framework formalized in Isabelle/HOL

Closure properties under various type constructions proven

Prototype implementation provided

Abstract

Multiple types can represent the same concept. For example, lists and trees can both represent sets. Unfortunately, this easily leads to incomplete libraries: some set-operations may only be available on lists, others only on trees. Similarly, subtypes and quotients are commonly used to construct new type abstractions in formal verification. In such cases, one often wishes to reuse operations on the representation type for the new type abstraction, but to no avail: the types are not the same. To address these problems, we present a new framework that transports programs via equivalences. Existing transport frameworks are either designed for dependently typed, constructive proof assistants, use univalence, or are restricted to partial quotient types. Our framework (1) is designed for simple type theory, (2) generalises previous approaches working on partial quotient types, and (3) is based on standard mathematical concepts, particularly Galois connections and equivalences. We introduce the notion of partial Galois connections and equivalences and prove their closure properties under (dependent) function relators, (co)datatypes, and compositions. We formalised the framework in Isabelle/HOL and provide a prototype. This is the extended version of "Transport via Partial Galois Connections and Equivalences", 21st Asian Symposium on Programming Languages and Systems, 2023.