@INPROCEEDINGS{BasinFriedrich96,
AUTHOR = "David Basin and Stefan Friedrich",
TITLE =  "Modeling a Hardware Synthesis Methodology in Isabelle",
BOOKTITLE = {Theorem Proving in Higher Order Logics (TPHOLs'96)},
YEAR = 1996,
PUBLISHER = "Springer-Verlag",
SERIES = "LNCS",
VOLUME = "1125",
ADDRESS = "Turku, Finland",
MONTH = "August",
PAGES = "33-50",
ABSTRACT =  { 
    Formal Synthesis is a methodology developed at Kent
    for combining circuit design and verification.  We
    have reinterpreted this methodology in Isabelle's
    theory of higher-order logic so that circuits are
    synthesized using higher-order resolution.  Our
    interpretation simplifies and extends Formal
    Synthesis both conceptually and in implementation.
    It also supports integration of this development
    style with other synthesis methodologies and leads
    to techniques for developing new classes of
    circuits, e.g., recursive descriptions of parameterized circuits. },
}