Core-Erlang-Formalization/_CoqProject at master · harp-project/Core-Erlang-Formalization · GitHub

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
-R src CoreErlang

src/Basics.v
src/Syntax.v
src/Induction.v
src/Equalities.v
src/SideEffects.v
src/Scoping.v
src/Auxiliaries.v
src/Maps.v
src/Manipulation.v
src/ScopingLemmas.v
src/Matching.v
src/StrictEqualities.v

src/FrameStack/Frames.v
src/FrameStack/SubstSemanticsLabeled.v
src/FrameStack/SubstSemantics.v
src/FrameStack/Tests/Tests.v
src/FrameStack/Tests/ExceptionTests.v
src/FrameStack/Termination.v
src/FrameStack/LabeledTermination.v
src/FrameStack/SubstSemanticsLabeledLemmas.v
src/FrameStack/SubstSemanticsLemmas.v
src/FrameStack/LogRel.v
src/FrameStack/Compatibility.v
src/FrameStack/CIU.v
src/FrameStack/Examples.v
src/FrameStack/CTX.v
src/FrameStack/Tests/EvalExamples.v
src/FrameStack/SubstSemanticsAutoSolver.v
src/FrameStack/Tests/SubstSemanticsAutoSolverTests.v

src/FrameStack/Vulnerabilities/AtomExhaustion.v
src/FrameStack/Vulnerabilities/AtomExhaustionExamples.v


src/Concurrent/PIDRenaming.v
src/Concurrent/ProcessSemantics.v
src/Concurrent/NodeSemantics.v
src/Concurrent/NodeSemanticsLemmas.v
src/Concurrent/StrongBisim.v
src/Concurrent/WeakBisim.v
src/Concurrent/BarbedBisim.v
src/Concurrent/BisimRenaming.v

src/Concurrent/BisimReductions.v
src/Concurrent/MapPmap.v

src/Concurrent/ClosednessLemmas.v

src/Interpreter/InterpreterAux.v
src/Interpreter/InterpreterAuxLemmas.v
src/Interpreter/StepFunctions.v
src/Interpreter/Scheduler.v
src/Interpreter/Equivalences.v
src/Interpreter/ExampleASTs

src/Symbolic/SymbTheorems.v
src/Symbolic/SymbTactics.v
src/Symbolic/SymbExamples.v

src/BigStep/Syntax.v
src/BigStep/Induction.v
src/BigStep/Equalities.v
src/BigStep/Helpers.v
src/BigStep/Environment.v
src/BigStep/SideEffects.v
src/BigStep/Auxiliaries.v
src/BigStep/ModuleAuxiliaries.v
src/BigStep/FunctionalBigStep.v
src/BigStep/BigStep.v
src/BigStep/Coverage.v
src/BigStep/Tactics.v
src/BigStep/EraseNames.v
src/BigStep/DeterminismHelpers.v
src/BigStep/SemanticsProofs.v
src/BigStep/SemanticsEquivalence.v
src/BigStep/FullEquivalence.v
src/BigStep/WeakEquivalence.v
src/BigStep/WeakEquivalenceExamples.v
src/BigStep/EquivalenceProofs.v

src/BigStep/MapEval.v
src/BigStep/Tests/AutomatedTests.v
src/BigStep/Tests/AutomatedSideEffectTests.v
src/BigStep/Tests/AutomatedExceptionTests.v
src/BigStep/Tests/AutomatedSideEffectExceptionTests.v
src/BigStep/Tests/EvalExamples.v


src/FrameStack/Optimisations/SeqDeadCode.v