Towards High-Level Deductive Program Synthesis based on Type Theory

Published in the Proceedings of the Tenth Knowledge-Based Software Engineering Conference (KBSE'95), Boston, Massachusetts, USA, November 12-15, 1995. IEEE Computer Society, 1995.

---

Authors

Harald Rueß

Abstract

Through 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. Moreover, notions of type-theory permit reuse not only of programs but also of whole developments within this framework.

gzipped postscript or postscript

BibTeX Entry

@inproceedings{Ruess:KBSE96
	TITLE = {Towards High-Level Deductive Program Synthesis Based on Type Theory},
	AUTHOR = {Harald Rue{\ss}},
	BOOKTITLE = {Proceedings of the Tenth Knowledge-Based Software Engineering Conference (KBSE'95)},
        LOCATION = {Boston, MA},
	MONTH = {November},
	YEAR = 1995,
	PAGES = {174--183},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	PUBLISHER = {IEEE Computer Society},
        NOTE = {ISBN 0-8186-7204-8}
}

---

Harald Ruess: ruess@csl.sri.com