Modules FTreeAnalysisSig, FTreeAnalysisSpec
[darcs-mirror-isa-launchbury.git] / Launchbury /
drwxr-xr-x   ..
-rw-r--r-- 171 AEnv.thy
-rw-r--r-- 2652 AList-Utils-HOLCF.thy
-rw-r--r-- 3788 AList-Utils-Nominal.thy
-rw-r--r-- 7928 AList-Utils.thy
-rw-r--r-- 6621 Abstract-Denotational-Props.thy
-rw-r--r-- 365 AbstractCorrectness.thy
-rw-r--r-- 4139 AbstractCorrectnessSestoft.thy
-rw-r--r-- 5615 AbstractDenotational.thy
-rw-r--r-- 12423 AbstractTransform.thy
-rw-r--r-- 875 Adequacy.thy
-rw-r--r-- 2278 AnalBinds.thy
-rw-r--r-- 549 Arity-Nominal.thy
-rw-r--r-- 4414 Arity.thy
-rw-r--r-- 7521 ArityAnalysisAbinds.thy
-rw-r--r-- 7807 ArityAnalysisFix.thy
-rw-r--r-- 4196 ArityAnalysisFixProps.thy
-rw-r--r-- 847 ArityAnalysisImpl.thy
-rw-r--r-- 5236 ArityAnalysisImplCorrect.thy
-rw-r--r-- 4564 ArityAnalysisPreImpl.thy
-rw-r--r-- 187 ArityAnalysisSig.thy
-rw-r--r-- 4976 ArityAnalysisSpec.thy
-rw-r--r-- 14837 ArityEtaExpand.thy
-rw-r--r-- 581 ArityEtaExpansionSestoft.thy
-rw-r--r-- 381 ArityStack.thy
-rw-r--r-- 9222 BalancedTraces.thy
-rw-r--r-- 2869 C-Meet.thy
-rw-r--r-- 10392 C-restr.thy
-rw-r--r-- 4209 C.thy
-rw-r--r-- 502 CValue-Nominal.thy
-rw-r--r-- 1068 CValue.thy
-rw-r--r-- 5434 CallArityCorrectEnd2End.thy
-rw-r--r-- 1086 CallArityEtaExpand.thy
-rw-r--r-- 5590 CallFutureCardinality.thy
-rw-r--r-- 9111 CallFutures.thy
-rw-r--r-- 2969 Cardinality-Domain.thy
-rw-r--r-- 3321 CardinalityAnalysis.thy
-rw-r--r-- 30320 CardinalityEtaExpand.thy
-rw-r--r-- 5451 CoCallAnalysisBinds.thy
-rw-r--r-- 9578 CoCallAnalysisImpl.thy
-rw-r--r-- 272 CoCallAnalysisSig.thy
-rw-r--r-- 28884 CoCallCardinality.thy
-rw-r--r-- 13394 CoCallFix.thy
-rw-r--r-- 36467 CoCallGraph-FTree.thy
-rw-r--r-- 1837 CoCallGraph-Nominal.thy
-rw-r--r-- 15226 CoCallGraph.thy
-rw-r--r-- 26337 CoCallImplCorrect.thy
-rw-r--r-- 696 CoCallsFuture.thy
-rw-r--r-- 925 ConstOn.thy
-rw-r--r-- 6080 Correctness-Counterexample.thy
-rw-r--r-- 4030 Correctness.thy
-rw-r--r-- 9667 CorrectnessOriginal.thy
-rw-r--r-- 11856 CorrectnessResourced.thy
-rw-r--r-- 14821 CorrectnessStacked.thy
-rw-r--r-- 5731 CycleCutOff.thy
-rw-r--r-- 4431 DeadCodeRemoval.thy
-rw-r--r-- 11513 DeadCodeRemoval2.thy
-rw-r--r-- 13046 DeadCodeRemoval2Correct.thy
-rw-r--r-- 14833 DeadCodeRemoval2CorrectSestoft.thy
-rw-r--r-- 12069 DeadCodeRemovalCorrect.thy
-rw-r--r-- 3838 Denotational-Related.thy
-rw-r--r-- 5171 Denotational.thy
-rw-r--r-- 1270 DenotationalEquivalences.thy
-rw-r--r-- 19050 Down.thy
-rw-r--r-- 3922 Env-HOLCF.thy
-rw-r--r-- 4576 Env-Nominal.thy
-rw-r--r-- 12704 Env.thy
-rw-r--r-- 2938 EtaExpansion.thy
-rw-r--r-- 1182 EtaExpansionArity.thy
-rw-r--r-- 5663 EtaExpansionSestoft.thy
-rw-r--r-- 5072 EvalHeap.thy
-rw-r--r-- 10324 Everything.thy
-rw-r--r-- 15941 EverythingAdequacy.thy
-rw-r--r-- 39841 FMap-HOLCF.thy
-rw-r--r-- 132 FMap-Heap.thy
-rw-r--r-- 9595 FMap-Join.thy
-rw-r--r-- 3530 FMap-Nominal-HOLCF.thy
-rw-r--r-- 9667 FMap-Nominal-Unused.thy
-rw-r--r-- 4556 FMap-Nominal.thy
-rw-r--r-- 3062 FMap-Unused.thy
-rw-r--r-- 17113 FMap.thy
-rw-r--r-- 9669 FTree-HOLCF.thy
-rw-r--r-- 714 FTree-Nominal-HOLCF.thy
-rw-r--r-- 55283 FTree.thy
-rw-r--r-- 253 FTreeAnalysisSig.thy
-rw-r--r-- 1708 FTreeAnalysisSpec.thy
-rw-r--r-- 22345 FTreeCardinality.thy
-rw-r--r-- 5342 FixRestr.thy
-rw-r--r-- 264 Flag.thy
-rw-r--r-- 6014 FutureCardinality.thy
-rw-r--r-- 1193 HOLCF-Fix-Join-Nominal.thy
-rw-r--r-- 16533 HOLCF-Fix-Join.thy
-rw-r--r-- 9062 HOLCF-Join-Classes.thy
-rw-r--r-- 9421 HOLCF-Join.thy
-rw-r--r-- 8616 HOLCF-Meet-Classes.thy
-rw-r--r-- 7438 HOLCF-Meet.thy
-rw-r--r-- 6250 HOLCF-Set-Nominal.thy
-rw-r--r-- 41387 HOLCF-Set.thy
-rw-r--r-- 759 HOLCF-Top.thy
-rw-r--r-- 6718 HOLCF-Utils.thy
-rw-r--r-- 4048 HSem-Equivalences.thy
-rw-r--r-- 65133 HSem.thy
-rw-r--r-- 667 HasESem.thy
-rw-r--r-- 24412 HeapSemantics.thy
-rw-r--r-- 2495 ImageP.thy
-rw-r--r-- 20112 Indirections.thy
-rw-r--r-- 15048 IteratedFixedPoint.thy
-rw-r--r-- 3507 Iterative.thy
-rw-r--r-- 6036 Launchbury-Unstack.thy
-rw-r--r-- 11834 Launchbury.thy
-rw-r--r-- 10888 LaunchburyAbstractTransformation.thy
-rw-r--r-- 18907 LaunchburyAddBH.thy
-rw-r--r-- 947 LaunchburyAddLog.thy
-rw-r--r-- 12247 LaunchburyCombined-Unstack.thy
-rw-r--r-- 15170 LaunchburyCombined.thy
-rw-r--r-- 24906 LaunchburyCombinedStacked.thy
-rw-r--r-- 15794 LaunchburyCombinedTaggedMap.thy
-rw-r--r-- 12440 LaunchburyLog.thy
-rw-r--r-- 8641 LaunchburyMoreFree.thy
-rw-r--r-- 2779 LaunchburyNoBH.thy
-rw-r--r-- 16228 LaunchburyStacked.thy
-rw-r--r-- 3640 LaunchburyUnBH.thy
-rw-r--r-- 7015 List-Interleavings.thy
-rw-r--r-- 6363 LookAheadSim.thy
-rw-r--r-- 876 Mono-Nat-Fun.thy
-rw-r--r-- 104 NewStuff.thy
-rw-r--r-- 6810 NoCardinalityAnalysis.thy
-rw-r--r-- 9335 Nominal-HOLCF.thy
-rw-r--r-- 13888 Nominal-Utils.thy
-rw-r--r-- 290 Pointwise.thy
-rw-r--r-- 629 ROOT-Submission-Adequacy
-rw-r--r-- 13115 RedsImprovesArityAnalysis.thy
-rw-r--r-- 36817 RemoveTaggedMapIndirection.thy
-rw-r--r-- 20373 ResourcedAdequacy.thy
-rw-r--r-- 4795 ResourcedDenotational.thy
-rw-r--r-- 4971 Sestoft.thy
-rw-r--r-- 5305 SestoftConf.thy
-rw-r--r-- 9684 SestoftCorrect.thy
-rw-r--r-- 2193 SestoftGC.thy
-rw-r--r-- 5400 SestoftNU.thy
-rw-r--r-- 207 Set-Cpo-Nominal.thy
-rw-r--r-- 2131 Set-Cpo.thy
-rw-r--r-- 11723 Substitution.thy
-rw-r--r-- 25519 Terms.thy
-rw-r--r-- 5426 TransformTools.thy
-rw-r--r-- 4064 TrivialArityAnal.thy
-rw-r--r-- 3475 Unused.thy
-rw-r--r-- 1603 Value-Meet.thy
-rw-r--r-- 360 Value-Nominal.thy
-rw-r--r-- 1938 Value.thy
-rw-r--r-- 23672 ValueSimilarity.thy
-rw-r--r-- 175 Vars.thy
drwxr-xr-x - document