Code

Delay monad interface and model#147

Code

Draft

Ryuji-Kawakami wants to merge 30 commits intoaffeldt-aist:masteraffeldt-aist/monae:masterfrom Ryuji-Kawakami:delaypullRyuji-Kawakami/monae:delaypullCopy head branch name to clipboard

+2,260-83

Commits

Commits on Dec 3, 2024

• add delay monad

  Ryuji-Kawakami

  committed
  d284233

  Copy full SHA for d284233

Commits on Dec 9, 2024

• arrange the format of programs in example_delay.v

  Ryuji-Kawakami

  committed
  bdc9234

  Copy full SHA for bdc9234

• modify the format of programs in example_delaystate.v

  Ryuji-Kawakami

  committed
  c6a760e

  Copy full SHA for c6a760e

Commits on Dec 23, 2024

• modify the parametric morphisms definition by using pointwise relation

  Ryuji-Kawakami

  committed
  eb81166

  Copy full SHA for eb81166

Commits on Jan 2, 2025

• change the space around commas and colons

  Ryuji-Kawakami

  committed
  ccb11a7

  Copy full SHA for ccb11a7

• remove some unnecessary Parentheses and spaces

  Ryuji-Kawakami

  committed
  8cbd01c

  Copy full SHA for 8cbd01c

• replace fact and exp function using ssrnal library

  Ryuji-Kawakami

  committed
  b27e099

  Copy full SHA for b27e099

Commits on Jan 3, 2025

• remove importing ssrnat and use the notation for factorial

  Ryuji-Kawakami

  committed
  0ba600d

  Copy full SHA for 0ba600d

• replace n + 1 and S n for n.+1

  Ryuji-Kawakami

  committed
  5f6b886

  Copy full SHA for 5f6b886

• renaming Bisim to strongBisim

  Ryuji-Kawakami

  committed
  d8eb6a3

  Copy full SHA for d8eb6a3

• replace Oeq for wBisim and wBisim for wBisims

  Ryuji-Kawakami

  committed
  195c405

  Copy full SHA for 195c405

• change the notation for wBisim and wBisims

  Ryuji-Kawakami

  committed
  68226d5

  Copy full SHA for 68226d5

• instance the delay monad from wBisim laws

  Ryuji-Kawakami

  committed
  f126c23

  Copy full SHA for f126c23

Commits on Jan 9, 2025

• replace the tactics case : _ = _ ... for have [|] := ...

  Ryuji-Kawakami

  committed
  985f389

  Copy full SHA for 985f389

• change the indent in example_delay.v and remove the lemma expE_aux

  Ryuji-Kawakami

  committed
  315a614

  Copy full SHA for 315a614

• remove the example section in hierarchy and mondify the proof in parametric morphism definition for while

  Ryuji-Kawakami

  committed
  56d0f75

  Copy full SHA for 56d0f75

• replace the tactics case: _ < _ for have [|] := ltnP _ _

  Ryuji-Kawakami

  committed
  488f345

  Copy full SHA for 488f345

Commits on Jan 11, 2025

• change the indent in delay_monad_model.v

  Ryuji-Kawakami

  committed
  335c00e

  Copy full SHA for 335c00e

Commits on Jan 12, 2025

• change the indents

  Ryuji-Kawakami

  committed
  e2071bb

  Copy full SHA for e2071bb

• change function definitions to use the projection function

  Ryuji-Kawakami

  committed
  d97ca57

  Copy full SHA for d97ca57

Commits on Jan 14, 2025

• share typed_store_universe

  garrigue

  committed
  e45028a

  Copy full SHA for e45028a

Commits on Jan 15, 2025

• modify the proof for factorial to be shorter

  Ryuji-Kawakami

  committed
  46f5a9c

  Copy full SHA for 46f5a9c

• add the deprecated warning for strongBisim_eq axiom

  Ryuji-Kawakami

  committed
  4d9abaa

  Copy full SHA for 4d9abaa

• add the typed universe file

  Ryuji-Kawakami

  committed
  bddf8dd

  Copy full SHA for bddf8dd

• take in the typed_store_universe.v file

  Ryuji-Kawakami

  committed
  c0182d9

  Copy full SHA for c0182d9

• add the definition of recursion using while operater

  Ryuji-Kawakami

  committed
  1b5584b

  Copy full SHA for 1b5584b

Commits on Jan 16, 2025

• remove the wBisims part

  Ryuji-Kawakami

  committed
  dba404c

  Copy full SHA for dba404c

• give the proof of partial correctness when terminates

  Ryuji-Kawakami

  committed
  8dbd70a

  Copy full SHA for 8dbd70a

Commits on Jan 17, 2025

• give the proof of partial correctness

  Ryuji-Kawakami

  committed
  c92c0b3

  Copy full SHA for c92c0b3

Commits on Feb 4, 2025

• add the example of bubble sort using partial correctness

  Ryuji-Kawakami

  committed
  89fbf83

  Copy full SHA for 89fbf83