| Branch: | Revision:

enguard @ master

Name Size
.gitignore 29 Bytes
Makefile 413 Bytes 0 Bytes
_CoqProject 123 Bytes

Latest revisions

# Date Author Comment
a4d0fede 06/22/2017 07:19 PM Christoph Rauch

More work on summand version

  • changed (trv) axiom to more general one
  • temporarily removed (wkn) axiom (provable from the rest)
  • TODO: generalise (cmp) axiom to work with arbitrary summands
  • separate file for summands
  • split isomorphism definition and lemmas into Helpers.v
67b69c1f 06/14/2017 12:15 PM Christoph Rauch

minor: changed definition of strength for M

65264eb4 06/12/2017 06:16 PM Christoph Rauch

added (prj) rule as well and proved for Tr

e0e9616e 06/12/2017 05:53 PM Christoph Rauch

added classes for strong monad/guardedness plus proved axiom for Tr

fe35d738 06/12/2017 04:07 PM Christoph Rauch

work on guardedness axioms and infinite trace state monad

  • removed unnecessary coproduct in definition of guardedness axioms
  • added 'Proper' instance for δ
  • finally formally proved guardedness axioms for M
075f9f42 06/12/2017 01:03 AM Christoph Rauch

cleaned up summands, added (wkn) again; monad instance for M

60fb355a 06/11/2017 01:09 AM Christoph Rauch

working version with dependent types

c21fe57c 06/10/2017 01:15 PM Christoph Rauch

added Makefile.coq to gitignore

91d08fa4 06/10/2017 01:14 PM Christoph Rauch

looking for a way to implement summands

78709e61 05/16/2017 10:50 AM Christoph Rauch

divided work into subdirectories

View all revisions | View revisions

Also available in: Atom