

@321

10 years 
campbell 
Soundness for reactive executions.



@295

10 years 
campbell 
Soundness of terminating whole program execution.



@292

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



@291

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



@255

10 years 
campbell 
Really restore matita root.



@254

10 years 
campbell 
Reset matita root.



@253

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



@252

10 years 
campbell 
Separate out soundness of exec_step from definition.



@251

10 years 
campbell 
Separate out soundness of exec_expr from definition.



@250

10 years 
campbell 
Begin separating soundness from executable semantics.



@245

10 years 
campbell 
Some progress on wholeexecution soundness.



@239

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



@227

10 years 
campbell 
Update notation in an example.



@226

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



@225

10 years 
campbell 
Missing case in cast.



@211

10 years 
campbell 
Make io_inject definition more straightforward.



@208

10 years 
campbell 
Fix up IO monad syntax.



@192

10 years 
campbell 
matita rev in README



@190

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



@189

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



@181

10 years 
campbell 
Sort out some axioms.



@178

10 years 
campbell 
Bring README file up to date.



@177

10 years 
campbell 
Missing cost labels file.



@176

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



@175

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



@174

10 years 
campbell 
Add a form of nonterminating functional semantics.



@173

10 years 
campbell 
Minor changes for newer versions of matita.



@160

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



@157

10 years 
campbell 
Make proposed memory spaces semantics more explicit.



@156

10 years 
campbell 
pdata support



@155

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



@154

10 years 
campbell 
Minor test case changes



@153

10 years 
campbell 
Use appropriate memory chunks for 8051 pointers.



@152

10 years 
campbell 
Force whd form for memory during execution



@149

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



@127

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



@126

10 years 
campbell 
Put in real pointer sizes.



@125

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



@124

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



@94

10 years 
sacerdot 
Minor comments.



@82

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



@25

10 years 
campbell 
Simplify the IO monad a little.



@24

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



@20

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



@17

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



@16

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



@15

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



@14

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



@13

10 years 
campbell 
Minor syntactic changes.



@12

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



@11

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



@10

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



@9

10 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

11 years 
campbell 
Some experimental work on executable Clight semantics.



@3

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