

@2954

9 years 
tranquil 
resolved circular dependency for ERTLptr's semantics



@2952

9 years 
tranquil 
* corrected all backend premains to not pass any arguments to the …



@2949

9 years 
sacerdot 
Some advance/repairing in ERTLptrToLTLProof. In particular, we know …



@2946

9 years 
tranquil 
main novelties:
* there is an inbuilt stack_usage nat in joint …



@2944

9 years 
sacerdot 
Some progress.



@2942

9 years 
sacerdot 
Many changes:
1. Coloured graphs are now specified in terms of …



@2940

9 years 
sacerdot 
1. StatusSimulationHelper? changed to allow to use status_rel that …



@2938

9 years 
sacerdot 
1. proof of "all eliminable are eliminable" completed
2. the notion of …



@2930

9 years 
sacerdot 
More progress. Some useless parameters have been removed from the …



@2922

9 years 
sacerdot 
Progress: proof of "eliminable statements can be eliminated" almost …



@2898

9 years 
piccolo 
1) simplification of cond and seq case for StatusSimulationHelper? …



@2889

9 years 
sacerdot 
It works very nice!



@2888

9 years 
tranquil 
backtracked some partial changes



@2887

9 years 
tranquil 
Corrected bug where eliminable statements where not eliminated. …



@2883

9 years 
piccolo 
partial commit



@2868

9 years 
sacerdot 
Pretty printing of ERTL and ERTLptr code.



@2863

9 years 
piccolo 
Added new invariant to good_if
Generalized version of cond case for …



@2855

9 years 
piccolo 
little bug fixed in TranslateUtils?.



@2851

9 years 
piccolo 
partial commit



@2849

9 years 
piccolo 
partial commit



@2845

9 years 
piccolo 
ERTLptr to LTL correctness proof started



@2844

9 years 
piccolo 
Stupid bug fixed



@2824

9 years 
tranquil 
* moved sum on lists notation to extranat
* used sum on lists to …



@2819

9 years 
sacerdot 
Proof obligation closed.



@2818

9 years 
sacerdot 
"Repaired", using non computational daemons.



@2808

9 years 
tranquil 
added local_stacksize to joint internal functions to accomodate for …



@2806

9 years 
tranquil 
new b_graph_translate obligations



@2796

9 years 
tranquil 
* added global notation for existence in Type[1] (\exists[1] x.P)
* in …



@2783

9 years 
piccolo 
modified joint_closed_internal_function definition (added condition on …



@2774

9 years 
sacerdot 
1. the compiler now outputs both the stack cost model and the max …



@2741

9 years 
sacerdot 
File used only by untrusted code.
Implemented in Matita to exploit …



@2739

9 years 
sacerdot 
The graph colouring algorithm takes in input also the function.



@2700

9 years 
sacerdot 
1. exponential function dropped in favour of standard library
2. …



@2697

9 years 
sacerdot 
Compiler fixed to include the ERTLptrToLTL pass.



@2694

9 years 
tranquil 
completed ERTLptrToLTL



@2693

9 years 
sacerdot 
1. Stuff moved to correct places.
2. ERTLptr pass added



@2691

9 years 
sacerdot 
ERTLtoERTLptr* moved to the proper place



@2688

9 years 
tranquil 
* in Arithmeticcs.ma: commented include that breaks script in latest …



@2681

9 years 
tranquil 
* improvements to the graph translation function
* fixed passes up to LTL



@2675

9 years 
tranquil 
* a generic graph program transformation



@2674

9 years 
tranquil 
* another change in block definition
* RTLabs > RTL and ERTL > …



@2666

9 years 
piccolo 
bug fixed in blocks.ma



@2663

9 years 
piccolo 
some minor modifications to ERTLtoERTLptr



@2662

9 years 
piccolo 
Towards a very generalized lemma that summarizes all of Paolo's results.



@2645

9 years 
sacerdot 
1. some broken backend files repaires, several still to go
2. the …



@2638

9 years 
piccolo 
Backend fixes for last Garnier's commit that removes the regions from …



@2604

9 years 
piccolo 
ERTLtoERTLptr in place.



@2601

9 years 
sacerdot 
Extraction to ocaml is now working, with a couple of bugs left.
One …



@2592

9 years 
piccolo 
main lemma of ERTLptr in place



@2590

9 years 
piccolo 
added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc …



@2570

9 years 
piccolo 
ERTLtoERTLptr in place



@2566

9 years 
piccolo 
ERTL to ERTLptr pass implemented up to a few things to be
left to the …
