@article{BasinLFDevSurvey,
AUTHOR = "David Basin",
TITLE = "Logical Framework Based Program Development",
JOURNAL="ACM Computing Surveys",
YEAR=1998,
Volume=30,
Number="3es",
Pages="1--4",
ABSTRACT = {
We propose a methodology for formalizing and using logical frameworks
for program development.  Calculi for
program transformation and synthesis are implemented
in a logic, such as first-order logic, by formally
deriving proof rules.  The derived rules are then applied using
higher-order resolution to simultaneously develop programs with
their correctness proofs and this development is partially automated
by calculus specific  tactics.  We have applied
this approach, using the Isabelle system,
to develop hardware descriptions, and functional and logic programs.
}		  
}