Context Navigation

CexecSound.ma

	Rev	Age	Author	Log Message
(edit)	@1244	9 years	campbell	Sort out Clight semantics equivalence proof for new SmallstepExec?.
(edit)	@1224	9 years	sacerdot	Type of programs in common/AST made more dependent. In particular, the …
(edit)	@1139	9 years	campbell	Shift init_data out of generic program record so that it only appears …
(edit)	@1058	10 years	campbell	Evict CompCert? Maps interface in favour of BitVectorTries?.
(edit)	@961	10 years	campbell	Use precise bitvector sizes throughout the front end, rather than …
(edit)	@891	10 years	campbell	Revise proofs affected by recent matita change.
(edit)	@882	10 years	campbell	Fix up fragile proofs for current version of matita.
(edit)	@879	10 years	campbell	Refine "AST" types to include size/signedness information.
(edit)	@797	10 years	campbell	Add error messages wherever the error monad is used. Sticks to …
(edit)	@744	10 years	campbell	Evict Coq-style integers from common/Integers.ma. Make more bitvector …
(edit)	@708	10 years	campbell	Use a more normalize-friendly definition of clight_exec to make the …
(edit)	@700	10 years	campbell	Get Clight semantics going again (except for problems CexecEquiv? that …
(copy)	@694	10 years	campbell	Start moving Clight into common directory.
copied from Deliverables/D3.1/C-semantics/CexecSound.ma:
(edit)	@500	10 years	campbell	Use dependent pointer type to ensure that the representation is always …

Note: See TracRevisionLog for help on using the revision log.