

@404

9 years 
campbell 
Update Csemantics README.



@401

9 years 
campbell 
Keep a depends file in the repository for the Csemantics.



@400

9 years 
campbell 
Minor changes for the new version of matita.



@399

9 years 
campbell 
Rearrange executable semantics a little.



@398

9 years 
campbell 
This time actually prove the result I intended.



@393

9 years 
campbell 
A few more details in D3.1.



@392

9 years 
campbell 
Work around cofixpoint unfolding problem. We only use axioms in …



@391

9 years 
campbell 
Comment out daemon and its uses  we don't need the properties of the …



@389

9 years 
campbell 
Sort out minor inconsistency between semantics.



@388

9 years 
campbell 
Tidy up some decidability functions.



@387

9 years 
campbell 
Sort out equality checking of types.



@386

9 years 
campbell 
Whole program equivalence result for the Clight executable and …



@385

9 years 
campbell 
Almost finished whole program equivalence.



@379

9 years 
campbell 
More whole execution equivalence  need ability to unfold cofixpoints …



@378

9 years 
campbell 
More work on equivalence of whole executions.



@366

9 years 
campbell 
Make I/O type safe, removing a discrepancy between the executable and …



@365

9 years 
campbell 
Soundness (really completeness) of Wrong executions.



@321

9 years 
campbell 
Soundness for reactive executions.



@295

9 years 
campbell 
Soundness of terminating whole program execution.



@292

9 years 
campbell 
Update acc 8051 syntax extension patch.
Adds memory spaces to Clight …



@291

9 years 
campbell 
Soundness of behaviour of exec_inf_aux on finite number of steps.



@255

9 years 
campbell 
Really restore matita root.



@254

9 years 
campbell 
Reset matita root.



@253

9 years 
campbell 
Update completeness proof for executable semantics with separate …



@252

9 years 
campbell 
Separate out soundness of exec_step from definition.



@251

9 years 
campbell 
Separate out soundness of exec_expr from definition.



@250

9 years 
campbell 
Begin separating soundness from executable semantics.



@245

9 years 
campbell 
Some progress on wholeexecution soundness.



@239

9 years 
campbell 
More work on soundness and completeness of executable Clight semantics.



@227

9 years 
campbell 
Update notation in an example.



@226

9 years 
campbell 
Some incomplete work on completeness of CexecIO wrt Csem.
Features …



@225

9 years 
campbell 
Missing case in cast.



@211

9 years 
campbell 
Make io_inject definition more straightforward.



@208

9 years 
campbell 
Fix up IO monad syntax.



@192

9 years 
campbell 
matita rev in README



@190

9 years 
campbell 
Minor changes to work with current matita HEAD (r10998).



@189

9 years 
campbell 
Rework monad notation so that it is displayed well in proof mode.



@181

9 years 
campbell 
Sort out some axioms.



@178

9 years 
campbell 
Bring README file up to date.



@177

9 years 
campbell 
Missing cost labels file.



@176

9 years 
campbell 
Remove old executable semantics without I/O.



@175

9 years 
campbell 
Add cost labels, with the semantics that the label is added to the …



@174

9 years 
campbell 
Add a form of nonterminating functional semantics.



@173

9 years 
campbell 
Minor changes for newer versions of matita.



@160

9 years 
campbell 
Patch to acc to parse 8051 memory spaces and output matita terms.



@157

9 years 
campbell 
Make proposed memory spaces semantics more explicit.



@156

9 years 
campbell 
pdata support



@155

9 years 
campbell 
More sensible handling of integer types and pointer casts.



@154

9 years 
campbell 
Minor test case changes



@153

9 years 
campbell 
Use appropriate memory chunks for 8051 pointers.



@152

9 years 
campbell 
Force whd form for memory during execution



@149

9 years 
campbell 
Fill in a few details about 8051 extensions.



@127

9 years 
campbell 
Allow the storage of pointers in suitably large integers.



@126

9 years 
campbell 
Put in real pointer sizes.



@125

9 years 
campbell 
Unify memory space / pointer types.
Implement global variable …



@124

9 years 
campbell 
Initial work on Clight semantics with 8051 memory spaces.



@94

9 years 
sacerdot 
Minor comments.



@82

9 years 
campbell 
Start of document about impact of 8051 memory model on C.



@25

9 years 
campbell 
Simplify the IO monad a little.



@24

9 years 
campbell 
Separate out IOMonad from the rest of the executable semantics.
Start …



@20

9 years 
campbell 
Add resumption monad based version of the executable semantics with …



@17

9 years 
campbell 
Remainder of the statements for the executable semantics (except for …



@16

9 years 
campbell 
Add rest of the expressions to executable Clight semantics.



@15

9 years 
campbell 
Make some definitions more normalization friendly by a little 'nlet …



@14

9 years 
campbell 
Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.



@13

9 years 
campbell 
Minor syntactic changes.



@12

9 years 
campbell 
Make memory model tests more readable.
Update README.



@11

9 years 
campbell 
Fill in some axioms to aid executablity.
Implement global variable …



@10

9 years 
campbell 
Add binary arithmetic libraries, use for integers and identifiers (but …



@9

9 years 
campbell 
Enough of an executable semantics to execute a notquitetrivial …



@5

10 years 
campbell 
Add a few execution steps and calculation of the initial state to the …



@4

10 years 
campbell 
Some experimental work on executable Clight semantics.



@3

10 years 
campbell 
Import workinprogress port of the CompCert? C semantics to matita.
