Mercurial > hg > Papers > 2023 > soto-master
directory /Paper/src/ @ 28:423f59b098ac
| name | size | permissions |
|---|---|---|
| [up] | drwxr-xr-x | |
 agda/
|
drwxr-xr-x | |
|
bt_impl/
|
drwxr-xr-x | |
|
bt_verif/
|
drwxr-xr-x | |
|
cbc/
|
drwxr-xr-x | |
|
dpp-verif/
|
drwxr-xr-x | |
|
while_loop_impl/
|
drwxr-xr-x | |
|
while_loop_verif/
|
drwxr-xr-x | |
 AgdaBasics.agda
|
24 | -rw-r--r-- |
|
AgdaBool.agda
|
52 | -rw-r--r-- |
|
AgdaDebug.agda
|
799 | -rw-r--r-- |
|
AgdaElem.agda
|
160 | -rw-r--r-- |
|
AgdaElemApply.agda
|
72 | -rw-r--r-- |
|
AgdaFunction.agda
|
28 | -rw-r--r-- |
|
AgdaId.agda
|
103 | -rw-r--r-- |
|
AgdaImplicitId.agda
|
149 | -rw-r--r-- |
|
AgdaImport.agda
|
361 | -rw-r--r-- |
|
AgdaInstance.agda
|
220 | -rw-r--r-- |
|
AgdaInterface.agda
|
756 | -rw-r--r-- |
|
AgdaLambda.agda
|
105 | -rw-r--r-- |
|
AgdaModusPonens.agda
|
88 | -rw-r--r-- |
|
AgdaNPushNPop.agda
|
749 | -rw-r--r-- |
|
AgdaNPushNPopProof.agda
|
3256 | -rw-r--r-- |
|
AgdaNat.agda
|
54 | -rw-r--r-- |
|
AgdaNot.agda
|
54 | -rw-r--r-- |
|
AgdaParameterizedModule.agda
|
240 | -rw-r--r-- |
|
AgdaPattern.agda
|
54 | -rw-r--r-- |
|
AgdaPlus.agda
|
62 | -rw-r--r-- |
|
AgdaProduct.agda
|
165 | -rw-r--r-- |
|
AgdaProp.agda
|
24 | -rw-r--r-- |
|
AgdaPushPop.agda
|
1140 | -rw-r--r-- |
|
AgdaPushPopProof.agda
|
501 | -rw-r--r-- |
|
AgdaRecord.agda
|
131 | -rw-r--r-- |
|
AgdaRecordProj.agda
|
161 | -rw-r--r-- |
|
AgdaSingleLinkedStack.agda
|
3259 | -rw-r--r-- |
|
AgdaStack.agda
|
295 | -rw-r--r-- |
|
AgdaStackDS.agda
|
324 | -rw-r--r-- |
|
AgdaStackImpl.agda
|
926 | -rw-r--r-- |
|
AgdaStackSomeState.agda
|
492 | -rw-r--r-- |
|
AgdaStackTest.agda
|
755 | -rw-r--r-- |
|
AgdaTree.agda
|
991 | -rw-r--r-- |
|
AgdaTreeDebug.agda
|
307 | -rw-r--r-- |
|
AgdaTreeDebugReturnNode4.agda
|
338 | -rw-r--r-- |
|
AgdaTreeImpl.agda
|
731 | -rw-r--r-- |
|
AgdaTreeProof.agda
|
2055 | -rw-r--r-- |
|
AgdaTreeTest.agda
|
185 | -rw-r--r-- |
|
AgdaTypeClass.agda
|
66 | -rw-r--r-- |
|
AgdaWhere.agda
|
157 | -rw-r--r-- |
|
CodeSegment.agda
|
124 | -rw-r--r-- |
|
CodeSegments.agda
|
240 | -rw-r--r-- |
|
DataSegment.agda
|
99 | -rw-r--r-- |
|
Equiv.agda
|
72 | -rw-r--r-- |
|
Exec.agda
|
204 | -rw-r--r-- |
|
Goto.agda
|
102 | -rw-r--r-- |
|
Maybe.agda
|
92 | -rw-r--r-- |
|
MetaCodeSegment.agda
|
180 | -rw-r--r-- |
|
MetaDataSegment.agda
|
186 | -rw-r--r-- |
|
MetaMetaCodeSegment.agda
|
1188 | -rw-r--r-- |
|
MetaMetaDataSegment.agda
|
424 | -rw-r--r-- |
|
ModelChecking.agda
|
19050 | -rw-r--r-- |
|
Nat.agdai
|
4743 | -rw-r--r-- |
|
NatAdd.agda
|
98 | -rw-r--r-- |
|
NatAddSym.agda
|
317 | -rw-r--r-- |
|
PushPopType.agda
|
259 | -rw-r--r-- |
|
Reasoning.agda
|
627 | -rw-r--r-- |
|
RedBlackTree.agda
|
13843 | -rw-r--r-- |
|
SingleLinkedStack.cbc
|
2949 | -rw-r--r-- |
|
Stack.cbc
|
634 | -rw-r--r-- |
|
ThreePlusOne.agda
|
178 | -rw-r--r-- |
|
agda-dpp-impl.agda
|
2248 | -rw-r--r-- |
|
agda-dpp-modelcheck.agda
|
2542 | -rw-r--r-- |
|
agda-func.agda
|
66 | -rw-r--r-- |
|
agda-func.agdai
|
8625 | -rw-r--r-- |
|
agda-hoare-interpret.agda
|
431 | -rw-r--r-- |
|
agda-hoare-prog.agda
|
315 | -rw-r--r-- |
|
agda-hoare-rule.agda
|
1279 | -rw-r--r-- |
|
agda-hoare-satisfies.agda
|
856 | -rw-r--r-- |
|
agda-hoare-soundness.agda
|
3559 | -rw-r--r-- |
|
agda-hoare-term.agda
|
621 | -rw-r--r-- |
|
agda-hoare-while.agda
|
460 | -rw-r--r-- |
|
agda-hoare-whileprog.agda
|
870 | -rw-r--r-- |
|
agda-hoare-write.agda
|
866 | -rw-r--r-- |
|
agda-mcg.agda
|
284 | -rw-r--r-- |
|
agda-mdg.agda
|
327 | -rw-r--r-- |
|
agda-pattern.agda
|
86 | -rw-r--r-- |
|
agda-plus.agda
|
64 | -rw-r--r-- |
|
agda-rewrite.agda
|
127 | -rw-r--r-- |
|
agda-term.agda
|
763 | -rw-r--r-- |
|
agda-term.agdai
|
28321 | -rw-r--r-- |
|
agda-term1.agda
|
234 | -rw-r--r-- |
|
agda-term2.agda
|
296 | -rw-r--r-- |
|
agda-term3.agda
|
396 | -rw-r--r-- |
|
atomicImpl.cbc
|
279 | -rw-r--r-- |
|
atomicInterface.h
|
313 | -rw-r--r-- |
|
atton-master-meta-sample.agda
|
2207 | -rw-r--r-- |
|
atton-master-sample.agda
|
874 | -rw-r--r-- |
|
axiom-taut.agda
|
336 | -rw-r--r-- |
|
cbc-agda.agda
|
699 | -rw-r--r-- |
|
cbc-agda.agdai
|
13408 | -rw-r--r-- |
|
cbc-condition.agda
|
326 | -rw-r--r-- |
|
cbc-hoare-SoundnessC.agda
|
174 | -rw-r--r-- |
|
cbc-hoare-loop.agda
|
849 | -rw-r--r-- |
|
cbc-hoare-loophelper.agda
|
396 | -rw-r--r-- |
|
cbc-hoare-prim.agda
|
243 | -rw-r--r-- |
|
cbc-hoare-soundness.agda
|
514 | -rw-r--r-- |
|
cbc-hoare-while.agda
|
344 | -rw-r--r-- |
|
cbc-hoare.agda
|
781 | -rw-r--r-- |
|
cg1.cbc
|
88 | -rw-r--r-- |
|
codeGearExample.cbc
|
184 | -rw-r--r-- |
|
cong.agda
|
78 | -rw-r--r-- |
|
context.c
|
752 | -rw-r--r-- |
|
context.h
|
1160 | -rw-r--r-- |
|
context1.c
|
748 | -rw-r--r-- |
|
context2.c
|
1122 | -rw-r--r-- |
|
contextContinuation.cbc
|
425 | -rw-r--r-- |
|
createCPUWorker.cbc
|
867 | -rw-r--r-- |
|
createTaskManager.cbc
|
2119 | -rw-r--r-- |
|
cuLaunchKernel.cbc
|
942 | -rw-r--r-- |
|
cudaTwice.cu
|
178 | -rw-r--r-- |
|
env.agda
|
174 | -rw-r--r-- |
|
env.agdai
|
14128 | -rw-r--r-- |
|
escape_agda.rb
|
776 | -rw-r--r-- |
|
ex_cbc
|
127 | -rw-r--r-- |
|
ex_code1
|
332 | -rw-r--r-- |
|
ex_code2
|
306 | -rw-r--r-- |
|
ex_stack.cbc
|
371 | -rw-r--r-- |
|
ex_stub
|
416 | -rw-r--r-- |
|
excbc.cbc
|
88 | -rw-r--r-- |
|
executorInterface.h
|
341 | -rw-r--r-- |
|
factrial.cbc
|
366 | -rw-r--r-- |
|
function.agda
|
81 | -rw-r--r-- |
|
gears-while.agda
|
2144 | -rw-r--r-- |
|
gears.agda
|
174 | -rw-r--r-- |
|
gencontext.c
|
1108 | -rw-r--r-- |
|
go
|
2234608 | -rw-r--r-- |
|
go.go
|
1341 | -rw-r--r-- |
|
goto.cbc
|
82 | -rw-r--r-- |
|
initContext.c
|
565 | -rw-r--r-- |
|
interface.cbc
|
422 | -rw-r--r-- |
|
iterateCall.cbc
|
3331 | -rw-r--r-- |
|
iteratePargoto.cbc
|
100 | -rw-r--r-- |
|
iteratorInterface.h
|
389 | -rw-r--r-- |
|
metaCodeGearExample.cbc
|
397 | -rw-r--r-- |
|
metaCreateTask.cbc
|
1507 | -rw-r--r-- |
|
nat.agda
|
55 | -rw-r--r-- |
|
openMP.c
|
68 | -rw-r--r-- |
|
parGotoCreateTask.cbc
|
145 | -rw-r--r-- |
|
putSynchronizedQueue.cbc
|
716 | -rw-r--r-- |
|
queueInterface.h
|
465 | -rw-r--r-- |
|
record.agda
|
61 | -rw-r--r-- |
|
redBlackTreeTest.agda
|
8037 | -rw-r--r-- |
|
semaphoreInterface.h
|
229 | -rw-r--r-- |
|
sendTask.cbc
|
1152 | -rw-r--r-- |
|
singleLinkedQueue.cbc
|
1009 | -rw-r--r-- |
|
singleLinkedQueueTest.cbc
|
163 | -rw-r--r-- |
|
singleLinkedQueueTest_script.cbc
|
355 | -rw-r--r-- |
|
singleLinkedStackInterface.cbc
|
498 | -rw-r--r-- |
|
sound-conv.agda
|
387 | -rw-r--r-- |
|
sound-impl.agda
|
91 | -rw-r--r-- |
|
sound-loop.agda
|
299 | -rw-r--r-- |
|
sound-looppsem.agda
|
313 | -rw-r--r-- |
|
sound-pcom.agda
|
189 | -rw-r--r-- |
|
sound-psemcom.agda
|
209 | -rw-r--r-- |
|
stack-product.agda
|
5339 | -rw-r--r-- |
|
stack-subtype-sample.agda
|
9939 | -rw-r--r-- |
|
stack-subtype.agda
|
3302 | -rw-r--r-- |
|
stack.agda
|
6569 | -rw-r--r-- |
|
stack.agdai
|
66884 | -rw-r--r-- |
|
stackImpl.agda
|
1544 | -rw-r--r-- |
|
stackTest.agda
|
5317 | -rw-r--r-- |
|
stackTest.agdai
|
60228 | -rw-r--r-- |
|
stackimpl.cbc
|
959 | -rw-r--r-- |
|
stub.cbc
|
379 | -rw-r--r-- |
|
stubCodeGear.cbc
|
643 | -rw-r--r-- |
|
subtype.agda
|
1935 | -rw-r--r-- |
|
sync_dequeue.c
|
546 | -rw-r--r-- |
|
sync_enqueue.c
|
762 | -rw-r--r-- |
|
synchronizedQueue.h
|
206 | -rw-r--r-- |
|
taskManagerInterface.cbc
|
640 | -rw-r--r-- |
|
term1.agda
|
463 | -rw-r--r-- |
|
term2.agda
|
196 | -rw-r--r-- |
|
term3.agda
|
293 | -rw-r--r-- |
|
termination.agda
|
189 | -rw-r--r-- |
|
termination.agdai
|
10648 | -rw-r--r-- |
|
tree.agda
|
429 | -rw-r--r-- |
|
twice.c
|
424 | -rw-r--r-- |
|
while-test.agda
|
138 | -rw-r--r-- |
|
workerRun.cbc
|
360 | -rw-r--r-- |
|
zero.agda
|
99 | -rw-r--r-- |