-
Notifications
You must be signed in to change notification settings - Fork 2
/
_CoqProject
67 lines (56 loc) · 1.67 KB
/
_CoqProject
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
-R external/base/ "Shared"
-R external/smpl/theories/ smpl
-I external/smpl/src/
-R theories/ "ProgrammingTuringMachines"
-install none
COQDOCFLAGS = "--charset utf-8 --parse-comments --with-header ./website/header.html --with-footer ./website/footer.html --index indexpage --coqlib https://coq.inria.fr/distrib/V8.8.1/stdlib/"
# Basics
theories/TM/Prelim.v
theories/TM/Relations.v
theories/TM/TM.v
# Basic Machines
theories/TM/Basic/Basic.v
theories/TM/Basic/Null.v
theories/TM/Basic/Mono.v
# Programming combinators
theories/TM/Combinators/Combinators.v
theories/TM/Combinators/Switch.v
theories/TM/Combinators/SequentialComposition.v
theories/TM/Combinators/If.v
theories/TM/Combinators/While.v
theories/TM/Combinators/Mirror.v
# Machine Lifting
theories/TM/Lifting/Lifting.v
theories/TM/Lifting/LiftTapes.v
theories/TM/Lifting/LiftAlphabet.v
# Compound Machines
theories/TM/Compound/TMTac.v
theories/TM/Compound/Multi.v
theories/TM/Compound/WriteString.v
theories/TM/Compound/MoveToSymbol.v
theories/TM/Compound/CopySymbols.v
# Programming
theories/TM/Code/Code.v
theories/TM/Code/CodeTM.v
theories/TM/Code/WriteValue.v
theories/TM/Code/ChangeAlphabet.v
theories/TM/Code/Copy.v
theories/TM/Code/ProgrammingTools.v
# Casees and constructors
theories/TM/Code/CaseNat.v
theories/TM/Code/CaseSum.v
theories/TM/Code/CaseList.v
theories/TM/Code/CaseFin.v
theories/TM/Code/CasePair.v
# Programming case studies
theories/TM/Code/SumTM.v
theories/TM/Code/NatTM.v
theories/TM/Code/ListTM.v
# Abstract Machine simulator
theories/TM/LM/Semantics.v
theories/TM/LM/Alphabets.v
theories/TM/LM/CaseCom.v
theories/TM/LM/LookupTM.v
theories/TM/LM/JumpTargetTM.v
theories/TM/LM/StepTM.v
theories/TM/LM/HaltingProblem.v