Transport via Partial Galois Connections and Equivalences

Kevin Kappelmann 📧

October 11, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This entry contains the accompanying formalisation of the paper "Transport via Partial Galois Connections and Equivalences" (APLAS 2023). It contains a theoretical framework to transport programs via equivalences, subsuming the theory of Isabelle's Lifting package. It also contains a prototype to automate transports using this framework in Isabelle/HOL, but this prototype is not yet ready for production. Finally, it contains a library on top of Isabelle/HOL's axioms, including various relativised concepts on orders, functions, binary relations, and Galois connections and equivalences.


BSD License


Related publications

  • Kappelmann, K. (2023). Transport via Partial Galois Connections and Equivalences. ArXiv.

Session Transport