Title :
Towards high-level deductive program synthesis based on type theory
Author_Institution :
Ulm Univ., Germany
Abstract :
Using the example of the divide et impera program scheme we present a knowledge-assisted refinement process based on type theory that yields executable programs from given requirement specifications. Programming knowledge is described in terms of precise mathematical theories and proofs, and programs and knowledge about programs is expressed in the same language and are developed using the same techniques
Keywords :
formal specification; inference mechanisms; knowledge based systems; programming theory; type theory; divide et impera program scheme; executable programs; high-level deductive program synthesis; knowledge-assisted refinement process; language; mathematical proofs; mathematical theories; programming knowledge; requirement specifications; type theory; Art; Calculus; Concrete; Humans; Logic programming; Mathematical programming; Production; Programming profession; Software libraries; Writing;
Conference_Titel :
Knowledge-Based Software Engineering Conference, 1995 .Proceedings., 10th
Conference_Location :
Boston, MA
Print_ISBN :
0-8186-7204-8
DOI :
10.1109/KBSE.1995.490133
