

@3505

6 years 
piccolo 



@3504

6 years 
sacerdot 
Last commit destroyed my changes: undone.



@3503

6 years 
piccolo 



@3502

6 years 
sacerdot 
Tentative final statement and proof for Vm.ma.



@3501

6 years 
sacerdot 
Final static_dynamic statement committed.



@3500

6 years 
sacerdot 
Nicer statements.



@3499

6 years 
sacerdot 
Nicer statement.



@3498

6 years 
sacerdot 
Much nicer statement.



@3497

6 years 
piccolo 
prova finale statico dinamico



@3496

6 years 
sacerdot 
Termination hypothesis greatly simplified.



@3495

6 years 
piccolo 



@3494

6 years 
piccolo 



@3493

6 years 
piccolo 



@3492

6 years 
sacerdot 
…



@3491

6 years 
piccolo 



@3490

6 years 
piccolo 



@3489

6 years 
sacerdot 
Second daemon closed.



@3488

6 years 
sacerdot 
One proof repaired.



@3487

6 years 
sacerdot 
No more i_act.
Note: we do not ask anywhere that no transitions to an …



@3486

6 years 
piccolo 



@3485

6 years 
piccolo 
partial measurable static dynamic



@3484

6 years 
sacerdot 
Simulation generalized to two different abstract_status.



@3483

6 years 
sacerdot 
…



@3482

6 years 
sacerdot 
No more daemons, all code repaired.



@3481

6 years 
sacerdot 
Restored more code claimed to be broken.



@3480

6 years 
sacerdot 
Restored code claimed to be no longer working.



@3479

6 years 
sacerdot 
Repaired.



@3478

6 years 
piccolo 
fixed costlabels



@3467

7 years 
piccolo 
slides



@3465

7 years 
piccolo 



@3464

7 years 
piccolo 
static_dinamic in place



@3463

7 years 
piccolo 



@3458

7 years 
piccolo 



@3457

7 years 
piccolo 



@3449

7 years 
piccolo 
clean up



@3448

7 years 
piccolo 



@3447

7 years 
piccolo 
correctness proof in place



@3446

7 years 
piccolo 
Correctness proof, closed all cases except the big lemma one



@3445

7 years 
piccolo 
correctness proof finished with a big open lemma



@3416

7 years 
piccolo 



@3414

7 years 
piccolo 



@3413

7 years 
sacerdot 
…



@3412

7 years 
sacerdot 
…



@3411

7 years 
piccolo 
new statement of correctness theorem in place



@3410

7 years 
piccolo 
we just realized that correctness theorem is wrong in the way it is …



@3409

7 years 
piccolo 



@3408

7 years 
piccolo 



@3407

7 years 
sacerdot 
Added get_element_append_r1.



@3406

7 years 
piccolo 



@3405

7 years 
piccolo 
closed some daemons



@3404

7 years 
piccolo 



@3403

7 years 
piccolo 



@3402

7 years 
piccolo 



@3401

7 years 
sacerdot 
More goals closed, but some are false.



@3400

7 years 
piccolo 



@3399

7 years 
piccolo 
call case not absorbing



@3398

7 years 
piccolo 
state relation with stack relation uptaded



@3397

7 years 
piccolo 
partial commit



@3396

7 years 
piccolo 
correctness proof in developping



@3394

7 years 
piccolo 
Added abstract language and procedure to add call post labelled



@3391

7 years 
piccolo 
Definition of well formed trace is in the operational semantics



@3390

7 years 
piccolo 
Patched simulation proof, changed definition of silent trace



@3389

7 years 
piccolo 
Ended simulation proof



@3388

8 years 
piccolo 
partial commit



@3387

8 years 
piccolo 
unified notation



@3386

8 years 
sacerdot 
Something that seems to be working after all.



@3385

8 years 
sacerdot 
…



@3384

8 years 
sacerdot 
Bug found?? We think so.



@3383

8 years 
sacerdot 
Simple simulation conditions and statements added.
The complex ones …



@3382

8 years 
sacerdot 
The simulation statement.



@3381

8 years 
sacerdot 
Pen&paper style hypotheses and statements for the staticdynamic …



@3380

8 years 
piccolo 
Added definition of measurable trace



@3379

8 years 
sacerdot 
Semantics completed.



@3378

8 years 
sacerdot 
 Stuff common to both languages is now in Common.ma
 object …



@3377

8 years 
sacerdot 
 emit l removed
+ io l1 l2
The semantics has been changed so that …



@3376

8 years 
sacerdot 
Semantics fixed: the value of the anonymous variable was corrupted by …



@3375

8 years 
sacerdot 
Imp language and its labelledSOS.
 The language has function calls …



@3374

8 years 
piccolo 



@3373

8 years 
sacerdot 
…



@3372

8 years 
piccolo 
Added new implementation of labelling approach based on LTS and …
