%%%  Kiel Bibliography 
%%   
%    Last change 09-21-90 
&%    Jens Dustin Redmer



@TECHREPORT{ FvKL,
    AUTHOR =  {Martin Fr"anzle and Burghard von Karger and Yassine Lakhneche},
    TITLE  =  {{\em Compiling Specification and Verification}}  ,
    TYPE   =  {Draft} ,
    INSTITUTION = {},
    YEAR   =   {October 26, 1989},
    NOTE   =   {Used in [MF 3]}
       }

@TECHREPORT{ GaNi,
    AUTHOR =   {Anders Gammelgaard and Flemming Nielson },
    TITLE  =   {Reactions to the Kiel Draft ``Compiling Specification and
                Verification''},
    TYPE   =   {Note},
    INSTITUTION = {},
    YEAR   =   {November 16, 1989 },
    NOTE   =   {Used in [MF 3]} 
      }

@TECHREPORT{ JiHo,
    AUTHOR =   {He Jifeng and C.A.R. Hoare },
    TITLE  =   {A Data Refinement Approach to Verification of Compiling 
                Specification },
    TYPE   =   {Draft},
    INSTITUTION = {},
    YEAR   =   {August, 1989 } ,
    NOTE   =   {Used in [MF 3]} 
           }

@techreport{InterimDeliverable,
     KEY    = {DB},
     EDITOR = {Dines {Bj\o rner}},
     TITLE  = {{P}ro{C}o{S} - {ESPRIT} {BRA} 3104 {M}ay 89-{A}pril 90 report : {P}rovably 
{C}orrect {S}ystems},
     INSTITUTION = {ProCoS ID/DTH},
     NUMBER      = {DB 9},
     MONTH       = {May},
     YEAR        = {1990}
     }

@techreport{FinalDeliverable,
     KEY    = {DB},
     EDITOR = {Dines {Bj\o rner}},
     TITLE  = {{P}ro{C}o{S} - {ESPRIT} {BRA} 3104 {F}inal report : {P}rovably 
{C}orrect {S}ystems},
     INSTITUTION = {ProCoS ID/DTH},
     NUMBER      = {},
     MONTH       = {October},
     YEAR        = {1991}
     }

@techreport{DWW1,
     KEY         = {DWW1},
     AUTHOR      = {Debora Weber-Wulff},
     TITLE       = {Trip Report : Visit to {C}omputational {L}ogic, {I}nc., {A}ustin, {T}exas},
     INSTITUTION = {ProCoS},
     ADDRESS     = {Kiel},
     NUMBER      = {DWW 1},
     MONTH       = {February},
     YEAR        = {1990}
     }


%techreport{DWW2,
%     KEY         = {DWW2},
%     AUTHOR      = {Debora Weber-Wulff},
%     TITLE       = {A (v{W})- Grammar for Concrete {PL}$_0$ Syntax and Parser Correctness},
%     INSTITUTION = {ProCoS Kiel},
%     NUMBER      = {DWW 2},
%     MONTH       = {May},
%     YEAR        = {1990}
%     }

@article{ProofMovie,
     AUTHOR      = {Debora Weber-Wulff},
     TITLE       = {Proof Movie - Proving the Add-Assign Compiler
                    with the Boyer-Moore prover},
     JOURNAL     = {Formal Aspects of Computing},
     NOTE        = {To appear}
     }     

@techreport{DWW7,
     AUTHOR      = {Debora Weber-Wulff},
     TITLE       = {Pass Collapsing : An Optimization Method for Compiler Proofs},
     INSTITUTION = {ProCoS Kiel},
     NUMBER      = {DWW 7},
     MONTH       = {September},
     YEAR        = {1991}
     }


@inbook{DWW9,
     AUTHOR      = {Debora Weber-Wulff},
     TITLE       = {A Proven Correct Front-End for PL$_R^0$},
     KEY         = {DB},
     EDITOR      = {Dines {Bj\o rner}},
     SERIES      = {{P}ro{C}o{S} - {ESPRIT} {BRA} 3104 Final report : {P}rovably 
                   {C}orrect {S}ystems},
     PUBLISHER   = {ProCoS ID/DTH},
     VOLUME      = {3},
     NUMBER      = {},
     MONTH       = {March},
     YEAR        = {1992},
     NOTE        = {}
    }


@techreport{KHB3wrongtitle,
    AUTHOR       = {Karl-Heinz Buth and Debora Weber-Wulff},
    TITLE        = {A Proven Correct Front-End for PL$_R^0$},
    INSTITUTION  = {ProCoS Kiel},
    NUMBER       = {KHB 3},
    MONTH        = {February},
    YEAR         = {1991},
    NOTE         = {}
    }