Effective Programming

Jacob Frost

Effective Programming

Jacob Frost

Research output: Book/Report › Ph.D. thesis › Research

Abstract

To investigate the use of VTLoE as a basis for formal derivation of functional programs with effects. As a part of the process, a number of issues central to effective formal programming are considered. In particular it is considered how to develop a proof system suitable for pratical reasoning, how to implement this system in the generic proof assistant Isabelle and finally how to apply the logic and the implementation to programming.

Original language	English

Place of Publication	Kgs. Lyngby, Denmark
Publisher	Technical University of Denmark
Number of pages	170
ISBN (Print)	87-89112-37-7
Publication status	Published - Aug 1996

1 Finished

Effective Programming
Hansen, B. S. & Frost, J.
01/08/1991 → 01/07/1996
Project: Research

Cite this

@phdthesis{3e127137145f40a09c6404916ab6604f,

title = "Effective Programming",

abstract = "To investigate the use of VTLoE as a basis for formal derivation of functional programs with effects. As a part of the process, a number of issues central to effective formal programming are considered. In particular it is considered how to develop a proof system suitable for pratical reasoning, how to implement this system in the generic proof assistant Isabelle and finally how to apply the logic and the implementation to programming.",

author = "Jacob Frost",

year = "1996",

month = aug,

language = "English",

isbn = "87-89112-37-7",

publisher = "Technical University of Denmark",

}

TY - BOOK

T1 - Effective Programming

AU - Frost, Jacob

PY - 1996/8

Y1 - 1996/8

N2 - To investigate the use of VTLoE as a basis for formal derivation of functional programs with effects. As a part of the process, a number of issues central to effective formal programming are considered. In particular it is considered how to develop a proof system suitable for pratical reasoning, how to implement this system in the generic proof assistant Isabelle and finally how to apply the logic and the implementation to programming.

AB - To investigate the use of VTLoE as a basis for formal derivation of functional programs with effects. As a part of the process, a number of issues central to effective formal programming are considered. In particular it is considered how to develop a proof system suitable for pratical reasoning, how to implement this system in the generic proof assistant Isabelle and finally how to apply the logic and the implementation to programming.

M3 - Ph.D. thesis

SN - 87-89112-37-7

BT - Effective Programming

PB - Technical University of Denmark

CY - Kgs. Lyngby, Denmark

ER -