| Copyright | (c) Uni Bremen 2005-2007 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | non-portable (existential types) |
| Safe Haskell | Safe-Inferred |
Comorphisms
Description
This folder contains various comorphisms (implemented using
the type class Comorphism), which are then
collected to a logic graph in Comorphisms.LogicGraph.
The latter is based on the list of logics collected in
Comorphisms.LogicList.
The individual comorphisms are on the one hand trivial embeddings:
On the other hand, there are a number of real encodings:
Comorphisms.CASL2PCFOL, Comorphisms.CASL2TopSort encodings of subsorting
Comorphisms.CASL2SubCFOL encoding of partiality
Comorphisms.Sule2SoftFOL translating a CASL subset to SoftFOL
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.CspCASL2IsabelleHOL unfinished coding of CSP-CASL in IsabelleHOL
Comorphisms.HasCASL2HasCASL unfinished mapping of HasCASL subset to HasCASL program blocks
Finally, encodings to the theorem prover Isabelle:
Comorphisms.CoCFOL2IsabelleHOL
Comorphisms.PCoClTyCons2IsabelleHOL unfinished translation of HasCASL subset to Isabelle