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.

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

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

Older releases: