I have not implemented it myself, and don’t know of anyone else who has either.
I’d guess in terms of how it would be implemented, the best way would be to piggyback off of Coq or some other language from this list. Many of these already have a lot of work put into them, with libraries of definitions and theorems and so on. Then you allow trades between shares in A and B if and only if the trader can exhibit a proof of (A⟹B)∧(B⟹A). Hopefully the language has some reflection ability that allows you to determine which expressions are conjunctions or disjunctions or neither.
I have not implemented it myself, and don’t know of anyone else who has either.
I’d guess in terms of how it would be implemented, the best way would be to piggyback off of Coq or some other language from this list. Many of these already have a lot of work put into them, with libraries of definitions and theorems and so on. Then you allow trades between shares in A and B if and only if the trader can exhibit a proof of (A⟹B)∧(B⟹A). Hopefully the language has some reflection ability that allows you to determine which expressions are conjunctions or disjunctions or neither.