Skip to content

Latest commit

 

History

History
29 lines (22 loc) · 1.2 KB

README.md

File metadata and controls

29 lines (22 loc) · 1.2 KB
Raw

concurrent-slicing, release 0.1

Agda development accompanying the paper Causally consistent dynamic slicing, presented at CONCUR 2016. To typecheck the entire development, compile ConcurrentSlicing.agda. The module structure is summarised in Appendix A of the paper.

Required compiler and libraries

  • Agda, version 2.4.2.3; seems to be a problem with typeclass resolution under 2.5.1.
  • Agda standard library version 0.9.
  • agda-stdlib-ext, version 0.0.3.
  • proof-relevant-pi, version 0.3.

Future to-do items

  • Improvements to names (more conventional or more aligned with paper):

    • ∘ᶠ → ∘, idᶠ → id
    • tgt → fwd ?
    • get/put → app/unapp

  • I made a strategic decision to leave certain aspects of the development unformalised, including:

  • Proc.Ren.Lattice.*-preserves-≃ₑ and *-preserves-∘

  • Ren.Lattice.Properties counterpart to Ren.Properties

  • Transition.Ren.Lattice postulates

  • Transition.Concur.Cofinal.Lattice.Common.ᴬgamma₁