META-AMPHION: synthesis of efficient domain-specific program synthesis systems

AMPHION is a real-world knowledge-based software engineering (KBSE) system whose program synthesis subsystem is based on deductive synthesis. AMPHION has a domain-independent generic architecture that is specialized to a domain through a declarative theory. Program synthesis has been made efficient and automatic through manual tuning of theorem-proving strategies and tactics, and careful formulation of domain theories. The META-AMPHION system is being developed to empower domain experts to develop, maintain, and evolve their own AMPHION applications. META-AMPHION is intended to be the knowledge-based analogue of application-generator generator technology. The paper describes technology for automatically transforming declarative domain theories into efficient domain-specific program synthesis systems