-
Notifications
You must be signed in to change notification settings - Fork 0
/
README.v
137 lines (107 loc) · 3.5 KB
/
README.v
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
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
Require Import common.prop_as_core.
Require Import common.prop_as_unscoped.
Require stlc.autosubst2.prop_type_safety.
Require stlc.lngen.prop_type_safety.
Require systemf.autosubst2.prop_type_safety.
Require systemf.lngen.prop_type_safety.
Require fsub.autosubst2_dctx.prop_typing.
Require fsub.autosubst2_sctx.prop_typing.
Require fsub.lngen.prop_typing.
Section stlc.
Goal True. idtac "". idtac "". idtac "Simple Typed Lambda Calculus". idtac "". idtac "". Abort.
Section autosubst2.
Goal True. idtac "". idtac "Autosusbt2". idtac "". Abort.
Import stlc.autosubst2.def_as2.
Import stlc.autosubst2.def_extra.
Import stlc.autosubst2.prop_type_safety.
Print typing.
Print step.
Check preservation.
Print Assumptions preservation.
Check progress.
Print Assumptions progress.
End autosubst2.
Section lngen.
Goal True. idtac "". idtac "LNgen". idtac "". Abort.
Import Metalib.Metatheory.
Import stlc.lngen.def_ott.
Import stlc.lngen.def_extra.
Import stlc.lngen.prop_type_safety.
Print typing.
Print step.
Check preservation.
Print Assumptions preservation.
Check progress.
Print Assumptions progress.
End lngen.
End stlc.
Section systemf.
Goal True. idtac "". idtac "". idtac "System F". idtac "". idtac "". Abort.
Section autosubst2.
Goal True. idtac "". idtac "Autosusbt2". idtac "". Abort.
Import systemf.autosubst2.def_as2.
Import systemf.autosubst2.def_extra.
Import systemf.autosubst2.prop_type_safety.
Print typing.
Print step.
Check preservation.
Print Assumptions preservation.
Check progress.
Print Assumptions progress.
End autosubst2.
Section lngen.
Goal True. idtac "". idtac "LNgen". idtac "". Abort.
Import Metalib.Metatheory.
Import systemf.lngen.def_ott.
Import systemf.lngen.def_extra.
Import systemf.lngen.prop_type_safety.
Print typing.
Print step.
Check preservation.
Print Assumptions preservation.
Check progress.
Print Assumptions progress.
End lngen.
End systemf.
Section fsub.
Goal True. idtac "". idtac "". idtac "System F-sub". idtac "". idtac "". Abort.
Section autosubst2_dctx.
Goal True. idtac "". idtac "Autosusbt2 (Double Contexts [Type / Term])". idtac "". Abort.
Import fsub.autosubst2_dctx.def_as2.
Import fsub.autosubst2_dctx.def_extra.
Import fsub.autosubst2_dctx.prop_typing.
Print typing.
Print step.
Check preservation.
Print Assumptions preservation.
Check progress.
Print Assumptions progress.
End autosubst2_dctx.
(* for reference, this is another version using combined context, with plain De Brujin *)
(* https://www.seas.upenn.edu/~plclub/poplmark/vouillon.html *)
Section autosubst2_sctx.
Goal True. idtac "". idtac "Autosusbt2 (Single Context [Type + Term])". idtac "". Abort.
Import fsub.autosubst2_sctx.def_as2.
Import fsub.autosubst2_sctx.def_extra.
Import fsub.autosubst2_sctx.prop_typing.
Print typing.
Print step.
Check preservation.
Print Assumptions preservation.
Check progress.
Print Assumptions progress.
End autosubst2_sctx.
Section lngen.
Goal True. idtac "". idtac "LNgen". idtac "". Abort.
Import Metalib.Metatheory.
Import fsub.lngen.def_ott.
Import fsub.lngen.def_extra.
Import fsub.lngen.prop_typing.
Print typing.
Print step.
Check preservation.
Print Assumptions preservation.
Check progress.
Print Assumptions progress.
End lngen.
End fsub.