Comorphisms.hs revision e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0
{- |
This folder contains various comorphisms (implemented using
the type class 'Logic.Comorphism.Comorphism'), which are then
collected to a logic graph in "Comorphisms.LogicGraph".
The latter is based on the list of logics collected in
The individual comorphisms are on the one hand trivial embeddings:
On the ohter hand, there are a number of real encodings:
"Comorphisms.CASL2PCFOL", "Comorphisms.CASL2TopSort" encodings of subsorting
"Comorphisms.PCFOL2FOL" encoding of partiality
"Comorphisms.Modal2CASL" encoding of Kripke worlds
"Comorphisms.HasCASL2Haskell" translation of executable HasCASL subset to Haskell
"Comorphisms.CspCASL2Modal" unfinished coding of CSP-CASL LTS semantics as Kripke models
"Comorphisms.HasCASL2HasCASL" unfinished mapping of HasCASL subset to HsCASL program blocks
Finally, encodings to the theorem prover Isabelle:
-}
module Comorphisms where