K Development Plan

principle:

• splitting into multiple components; gluing together
• text representation as universal interface; in-memory communication is also possible but optional
• multiple implementations for each component
  • reference implementation: reference model, support full features, executable but not necessarily scalable, easy to experiment new ideas
  • optimized implementation: robust and scalable, may not support full features, may have different implementations for different purposes

components:

• kore definition
  • syntax for text representation as universal interface; should be easy to parse
• ml prover
  • check satisfiability for kore term (like z3)
• rewriting engine
  • given semantics and term, rewrite n-steps
• frontend
  • desugar or translate from any string into kore term

todo:

• kore
  • design syntax of text representation: Grigore, Everett, Lucas, Cosmin, ...
• ml prover
  • implement reference implementation in maude: Xiaohong, Everett
  • implement optimized implementation in ?: TBD
• rewriting engine
  • implement reference implementation in maude: Grigore, Everett
  • develop kale-backend as optimized implementation; add symbolic execution: TBD
  • maintain java-backend: Daejun, Manasvi
• frontend
  • implement printing kore text representation: TBD
  • split parser/compilation pipelines; at least for e-kore and kore: TBD