### 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

- Computer science/Programming languages/Lambda calculi
- Computer science/Programming languages/Type systems
- Computer science/Semantics and reasoning
- Mathematics/Order

### Related publications

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

### Session Transport

- HOL_Basics_Base
- Binary_Relation_Functions
- Binary_Relations_Order_Base
- Binary_Relations_Lattice
- Functions_Base
- HOL_Syntax_Bundles_Lattices
- Predicates_Lattice
- Function_Relators
- Predicates_Order
- Predicates
- Functions_Monotone
- Binary_Relations_Reflexive
- Binary_Relations_Symmetric
- Binary_Relations_Transitive
- Binary_Relations_Order
- Binary_Relations_Antisymmetric
- Binary_Relations_Injective
- Binary_Relations_Irreflexive
- Binary_Relations_Left_Total
- Binary_Relations_Right_Unique
- Binary_Relations_Surjective
- Binary_Relation_Properties
- Preorders
- Partial_Equivalence_Relations
- Equivalence_Relations
- Partial_Orders
- Restricted_Equality
- LBinary_Relations
- Functions_Injective
- Functions_Inverse
- Functions_Bijection
- Functions_Surjective
- Function_Properties
- LFunctions
- Order_Functions_Base
- Order_Functors_Base
- Galois_Base
- Galois_Relator_Base
- Order_Equivalences
- Half_Galois_Property
- Galois_Property
- Galois_Connections
- Galois_Equivalences
- Galois_Relator
- Galois
- Closure_Operators
- Order_Functions
- Order_Functors
- Orders
- HOL_Basics
- HOL_Mem_Of
- HOL_Syntax_Bundles_Relations
- HOL_Alignment_Binary_Relations
- HOL_Syntax_Bundles_Functions
- HOL_Alignment_Functions
- HOL_Syntax_Bundles_Orders
- HOL_Alignment_Orders
- HOL_Alignments
- HOL_Algebra_Alignment_Orders
- HOL_Algebra_Alignment_Galois
- HOL_Algebra_Alignments
- HOL_Syntax_Bundles_Base
- HOL_Syntax_Bundles_Groups
- HOL_Syntax_Bundles
- Transport_Base
- Transport_Bijections
- Transport_Compositions_Agree_Base
- Transport_Compositions_Agree_Monotone
- Transport_Compositions_Agree_Galois_Property
- Transport_Compositions_Agree_Galois_Connection
- Transport_Compositions_Agree_Galois_Equivalence
- Transport_Compositions_Agree_Galois_Relator
- Transport_Compositions_Agree_Order_Equivalence
- Transport_Compositions_Agree
- Transport_Compositions_Generic_Base
- Transport_Compositions_Generic_Galois_Property
- Transport_Compositions_Generic_Monotone
- Transport_Compositions_Generic_Galois_Connection
- Transport_Compositions_Generic_Galois_Equivalence
- Transport_Compositions_Generic_Galois_Relator
- Transport_Compositions_Generic_Order_Base
- Transport_Compositions_Generic_Order_Equivalence
- Transport_Compositions_Generic
- Transport_Compositions
- Reflexive_Relator
- Monotone_Function_Relator
- Transport_Functions_Base
- Transport_Functions_Monotone
- Transport_Functions_Galois_Property
- Transport_Functions_Galois_Connection
- Transport_Functions_Order_Base
- Transport_Functions_Galois_Equivalence
- Transport_Functions_Relation_Simplifications
- Transport_Functions_Galois_Relator
- Transport_Functions_Order_Equivalence
- Transport_Functions
- Transport_Identity
- Transport
- Transport_Natural_Functors_Base
- Transport_Natural_Functors_Galois
- Transport_Natural_Functors_Galois_Relator
- Transport_Natural_Functors_Order_Base
- Transport_Natural_Functors_Order_Equivalence
- Transport_Natural_Functors
- Transport_Rel_If
- Transport_Prototype
- Transport_Syntax
- Transport_Dep_Fun_Rel_Examples
- Transport_Lists_Sets_Examples
- Transport_Partial_Quotient_Types
- Transport_Typedef_Base
- Transport_Typedef
- Transport_Via_Partial_Galois_Connections_Equivalences_Paper

### Depends on

- Unification Utilities for Isabelle/ML

### Auto-related entries

- Properties of Orderings and Lattices
- Kleene Algebras with Domain
- Binary Multirelations
- Relation Algebra

## Cite

×

Transport-AFP

    @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