yellowsquid/helium.git - [no description]

Age	Commit message (Expand)	Author
2022-03-08	Migrate to agda-stdlib-2.0-dev.axiomatic	Greg Brown
2022-03-08	Add semantics of Hoare logic assertions.	Greg Brown
2022-03-08	Add semantics of Hoare logic terms.	Greg Brown
2022-03-08	Add Hoare logic assertions	Greg Brown
2022-03-08	Add reference substitution to terms.	Greg Brown
2022-03-08	Separate out Hoare logic terms.	Greg Brown
2022-03-03	Add function to eliminate all calls in expressions	Greg Brown
2022-03-03	Add way to convert function calls to expressions	Greg Brown
2022-02-22	Add if_then_ statements	Greg Brown
2022-02-22	Change stateful expressions to index on expression	Greg Brown
2022-02-21	Replace tup with cons and nil	Greg Brown
2022-02-21	Generalise slice and join into cut and splice.	Greg Brown
2022-02-21	Introduce tuple deconstructor expressions	Greg Brown
2022-02-21	Replace nat indices with fins.	Greg Brown
2022-02-19	Add predicate for being a sliced type.	Greg Brown
2022-02-19	Unalias bit type.	Greg Brown
2022-02-18	Remove declare case of Procedure.	Greg Brown
2022-02-17	Make call and invoke take All instead of tuple.	Greg Brown
2022-02-16	Begin work on axiomatic semantics.	Greg Brown
2022-02-15	Make expressions unable to change state.	Greg Brown
2022-02-15	Remove unnecessary return-type part of Statement	Greg Brown
2022-02-13	Write pseudocode definition of Barrett reduction	Greg Brown
2022-02-13	Define vmla instruction.	Greg Brown
2022-02-13	Extract common code from pseudocode instructions	Greg Brown
2022-02-13	Refactor to group instruction definitions together	Greg Brown
2022-02-13	Finish definition of denotational semantics.	Greg Brown
2022-02-02	Define pseudocode for a number of instructions.	Greg Brown
2022-01-21	Add pseudocode as a data type.	Greg Brown
2022-01-19	Rename pseudocode file.	Greg Brown
2022-01-18	Define the semantics of pseudocode data types.	Greg Brown
2022-01-16	Define ordered algebraic structures.	Greg Brown
2022-01-12	Eliminate even more state from the denotational semantics.	Greg Brown
2022-01-08	Make RawPseudocode contain its own bundles.	Greg Brown
2022-01-07	Add a missing raw algebra.	Greg Brown
2022-01-07	Demonstrate pointwise Vectors inherit algebraic properties.	Greg Brown
2022-01-07	Add some required algebraic types.	Greg Brown
2022-01-07	Introduce semantics for sequences of instructions.	Greg Brown
2022-01-07	Rename ⟦_⟧ to float.	Greg Brown
2021-12-28	Make the denotational semantics total.	Greg Brown
2021-12-27	Introduce Everything.agda to aid in overall compilation.	Greg Brown
2021-12-21	Define execBeats, a wrapper to execute beat-wise instructions.	Greg Brown
2021-12-21	Define semantics of vqdmulh.	Greg Brown
2021-12-21	Define semantics for vmulh.	Greg Brown
2021-12-20	Define vsub.	Greg Brown
2021-12-20	Remove bitstring addition.	Greg Brown
2021-12-20	Extract structures shared by most binary vector operations.	Greg Brown
2021-12-20	Define vmul.	Greg Brown
2021-12-20	Inline and rearrange to make vadd and vhsub look more similar.	Greg Brown
2021-12-20	Define semantics of vhsub.	Greg Brown
2021-12-20	Improve type-checking efficiency.	Greg Brown