Pinned Loading

1. tuura/redfin tuura/redfin Public

   Specification and verification of the REDFIN sequencer

   TeX 1

2. katamaran-project/katamaran katamaran-project/katamaran Public

   Katamaran is a semi-automated separation logic verifier for the Sail specification language. It works on an embedded version of Sail called μSail and verifies separation logic-based contracts of fu…

   Coq 17 4

3. tuura/selective-theory-coq tuura/selective-theory-coq Public

   Selective applicative functors laws and theorems

   Coq 14

4. students-big-brother students-big-brother Public

   Haskell 2

5. redfin-lib redfin-lib Public

   A model of a simple hypothetical RISC architecture with polymorphic semantics

   Haskell 5

6. Equational Reasoning in Coq using Ta... Equational Reasoning in Coq using Tactic Notations

   1

   Tactic Notation

   2

     "`Begin " constr(lhs) := idtac.

   3

   4

   Tactic Notation

   5

     "≡⟨ " tactic(proof) "⟩" constr(lhs) :=