source: src/RTLabs @ 3128

Name Size Rev Age Author Last Change
../
test 1226   10 years campbell Adjust pretty printers for change in program records, try a test of each.
RTLabs_classified_system.ma 1.2 KB 3031   8 years campbell Tidy up RTLabs preclassified_system definitions.
RTLabsExecToTrace.ma 1.4 KB 3096   8 years tranquil preliminary work on closing correctness.ma
debug.ma 1.8 KB 2601   8 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
RTLabsToRTLAxiom.ma 2.1 KB 3096   8 years tranquil preliminary work on closing correctness.ma
CostSpec.ma 3.2 KB 2601   8 years sacerdot Extraction to ocaml is now working, with a couple of bugs left. One …
RTLabs_syntax.ma 3.7 KB 2992   8 years campbell Add "only one return" invariant to RTLabs functions.
CostMisc.ma 3.8 KB 2313   9 years campbell RTLabs cost checker correct.
CostInj.ma 5.2 KB 3022   8 years campbell Make a couple of tests monadic for easier inversion.
import.ma 10.1 KB 2645   8 years sacerdot 1. some broken back-end files repaires, several still to go 2. the …
RTLabs_abstract.ma 16.0 KB 3031   8 years campbell Tidy up RTLabs preclassified_system definitions.
RTLabs_semantics.ma 17.9 KB 2936   8 years campbell Disable initialisation code generation in Cminor, propogate init data …
CostCheck.ma 27.4 KB 3022   8 years campbell Make a couple of tests monadic for easier inversion.
MeasurableToStructured.ma 30.5 KB 3031   8 years campbell Tidy up RTLabs preclassified_system definitions.
RTLabsToRTL.ma 38.6 KB 3037   8 years tranquil * ADDRESS joint instruction now has also an offset * corrected call to …
RTLabs_partial_traces.ma 101.0 KB 2923   8 years campbell Remove some leftovers.
RTLabs_traces.ma 126.0 KB 3050   8 years piccolo 1) Added general commutation theorem for monads. 2) Added some …
Note: See TracBrowser for help on using the repository browser.