Knowledge-Based Software Engineering Conference (1995)

Boston, Massachusetts

Nov. 12, 1995 to Nov. 15, 1995

ISSN: 1068-3062

ISBN: 0-8186-7204-8

pp: 174

H. Ruess , 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.

INDEX TERMS

type theory; programming theory; formal specification; inference mechanisms; knowledge based systems; high-level deductive program synthesis; type theory; divide et impera program scheme; knowledge-assisted refinement process; executable programs; requirement specifications; programming knowledge; mathematical theories; mathematical proofs; language

CITATION

H. Ruess,
"Towards high-level deductive program synthesis based on type theory",

*Knowledge-Based Software Engineering Conference*, vol. 00, no. , pp. 174, 1995, doi:10.1109/KBSE.1995.490133