summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2018-05-18Make named theorem collections of state monad more fine-grainedThomas Bauereiss
2018-05-18Add lemmas about monadic Boolean connectivesThomas Bauereiss
2018-05-18use correct inequality for strings.Robert Norton
2018-05-18Add sail_valuesAuxiliary rw theorems to computeLibRamana Kumar
2018-05-18Improve sail-heap dependencies in the HolmakefileRamana Kumar
2018-05-18Avoid split_on_char function that was introduced in OCaml 4.04. Use Util vers...Robert Norton
2018-05-17changes to for testing FreeBSD boot on MIPS: allowing loading raw file in oca...Robert Norton
2018-05-17Merge branch 'cheri-mono' into sail2Brian Campbell
2018-05-17Clean up MIPS for HOL4 a littleBrian Campbell
2018-05-17Use an intermediate base_monad type alias in Lem,Brian Campbell
2018-05-16Add handwritten script to HolmakefileBrian Campbell
2018-05-16More targeted gitignore for HOL4Brian Campbell
2018-05-16Termination proofs and lemmata for sail_values holRamana Kumar
2018-05-15Make all of Sail HOL libraries, not just the base heapBrian Campbell
2018-05-11Add snapshot of generated Isabelle theoriesThomas Bauereiss
2018-05-11Merge branch 'sail2' into cheri-monoThomas Bauereiss
2018-05-10RISC-V in HOL4Brian Campbell
2018-05-10Clean up HOL library properlyBrian Campbell
2018-05-09Fix an issue with C compilationAlasdair Armstrong
2018-05-09Add tests for Isabelle->OCaml generation for CHERI and AArch64Thomas Bauereiss
2018-05-09Run ARM built-in tests for Lem backend (via OCaml)Thomas Bauereiss
2018-05-07HOL script generation for library and CHERIBrian Campbell
2018-05-04Add back purely sequential Lem generationThomas Bauereiss
2018-05-03Flow typing and l-expression changes for ASL parserAlasdair Armstrong
2018-05-03Work in progress on the coq backendBrian Campbell
2018-04-24Add some explanations to free monad documentationThomas Bauereiss
2018-04-20Make building of Isabelle heap image optionalThomas Bauereiss
2018-04-19Fix minor typo.Prashanth Mundkur
2018-04-19more nuanced discussion of generating HOL4 and CoqPeter Sewell
2018-04-18Add generated PDF of documentation draft --- comments welcomeThomas Bauereiss
2018-04-18Add first draft of Isabelle library documentationThomas Bauereiss
2018-04-18Add a simple Hoare logic for sequential reasoning to the libraryThomas Bauereiss
2018-04-18Add some lemmas about bitvectorsThomas Bauereiss
2018-04-13Add a few more generated file to gitignoreBrian Campbell
2018-04-11Fix neq_range in flow.sailAlasdair Armstrong
2018-04-10Porting some minisail changes to sail2 branchAlasdair Armstrong
2018-04-06Add integer comparisons to overloads in flow typing libraryAlasdair Armstrong
2018-04-06Update sail.tex for wip latex outputAlasdair Armstrong
2018-04-05Fix precedence printing and update aarch64 specAlasdair Armstrong
2018-04-05Add generic prelude library that pulls in various basic sailAlasdair Armstrong
2018-04-03Added test cases for builtinsAlasdair Armstrong
2018-03-22Fix C compilation for CHERI and MIPSAlasdair Armstrong
2018-03-22Tune Lem pretty-printingThomas Bauereiss
2018-03-14Make partiality more explicit in library functions of Lem shallow embeddingThomas Bauereiss
2018-03-14Add address to Write_tag outcomeThomas Bauereiss
2018-03-14Use sets instead of lists for Lem nondeterminism monadThomas Bauereiss
2018-03-13Polymorphic option types now compile to CAlasdair Armstrong
2018-03-12ELF loading for C backendAlasdair Armstrong
2018-03-07Make union types consistent in the ASTAlasdair Armstrong
2018-03-05Add Print outcome to prompt monad for debugging and tracingThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:01:15 +0000