Towards High-Level Deductive Program Synthesis Based on Type Theory

DOI 10.1109/kbse.1995.490133 dblp

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.

BibTeX

@inproceedings{Reuss:ASE95,
  author    = {Harald Reu{\ss}},
  title     = {Towards {High-Level} Deductive Program Synthesis Based on Type Theory},
  booktitle = {ASE},
  pages     = {174--183},
  publisher = {{IEEE} Computer Society},
  year      = {1995},
}

Towards High-Level Deductive Program Synthesis Based on Type Theory

Abstract

Related papers