forked from spechub/Hets
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Comorphisms.hs
66 lines (40 loc) · 1.62 KB
/
Comorphisms.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
{- |
Module : $Id$
Description : various encodings
Copyright : (c) Uni Bremen 2005-2007
License : GPLv2 or higher, see LICENSE.txt
Maintainer : [email protected]
Stability : provisional
Portability : non-portable (existential types)
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
"Comorphisms.LogicList".
The individual comorphisms are on the one hand trivial embeddings:
"Comorphisms.CASL2CoCASL"
"Comorphisms.CASL2CspCASL"
"Comorphisms.CASL2HasCASL"
"Comorphisms.CASL2Modal"
"Comorphisms.Prop2CASL"
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.CFOL2IsabelleHOL"
"Comorphisms.CoCFOL2IsabelleHOL"
"Comorphisms.PCoClTyCons2IsabelleHOL"
unfinished translation of HasCASL subset to Isabelle
"Comorphisms.Haskell2IsabelleHOLCF"
-}
module Comorphisms where