Development: Task List

From Automated Assistance for Formal Reasoning

This article documents the list of current and future development efforts.

[edit] Migration, portability, and maintenance

• Setting up the aartifact system on:
  • BU systems.

[edit] Integration with existing systems

• Isabelle/Isar component:
  • data structure for maintaining proofs of derived expressions/relationships;
  • module for generating proofs that can be submitted directly to Isabelle/Isar for verification.
• Isabelle/Isar library:
  • importing formal facts in existing Isabelle/Isar libraries into aartifact database.

[edit] Other development

• JavaScript validation component:
  • integration of student projects into the system.

• Python library:
  • integration of student projects into the system.

• Documentation:
  • integration with latest release of MediaWiki;
  • installation;
  • build process.