Transport via Partial Galois Connections and Equivalences

Kevin Kappelmann 📧

October 11, 2023

Abstract

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.

License

BSD License

Topics

Related publications

  • Kappelmann, K. (2023). Transport via Partial Galois Connections and Equivalences. ArXiv. https://doi.org/10.48550/ARXIV.2303.05244

Session Transport

Depends on

Auto-related entries

Cite

× 
@article{Transport-AFP,
  author  = {Kevin Kappelmann},
  title   = {Transport via Partial Galois Connections and Equivalences},
  journal = {Archive of Formal Proofs},
  month   = {October},
  year    = {2023},
  note    = {\url{https://isa-afp.org/entries/Transport.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest