DocumentCode
296269
Title
Towards high-level deductive program synthesis based on type theory
Author
Rueß, Harald
Author_Institution
Ulm Univ., Germany
fYear
1995
fDate
12-15 Nov 1995
Firstpage
174
Lastpage
183
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Knowledge-Based Software Engineering Conference, 1995 .Proceedings., 10th
Conference_Location
Boston, MA
ISSN
1068-3062
Print_ISBN
0-8186-7204-8
Type
conf
DOI
10.1109/KBSE.1995.490133
Filename
490133
Link To Document