

@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

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

10 years 
campbell 
Some experimental work on executable Clight semantics.



@3

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