Browsing by Author "Graham, B."

Now showing 1 - 4 of 4
  • Thumbnail Image
    ItemOpen Access
    THE ARCHITECTURE OF HENDERSON'S SECD MACHINE
    (1989-01-01) Simpson, T.; Birtwistle, G.; Hermann, M.; Graham, B.
    We explain and document the architecture of an eager SECD machine devised by Henderson. A software interpreter for this architecture has been in use for two years and has been well tested. Expansion of the interpreter leads to the detailed specifications of an architecture in VLSI. Such an SECD chip has been layed out and fabricated.
  • Thumbnail Image
    ItemOpen Access
    A COMPILER FOR LISPKIT TARGETTED ATHENDERSON'S SECD MACHINE
    (1989-01-01) Simpson, T.; Birtwistle, G.; Hermann, M.; Graham, B.
    Long term research plans at Calgary are focussed on system verification. We have been working on hardware verification for some time, and this work will culminate in the verification of an SECD chip in 1989. The chip has been fabricated. We describe a compiler and its associated workbench, written in Franz Lisp, which takes Lispkit source code for Henderson's SECD machine. The compiler has been in operation for two years and has been well tested but not verified.
  • Thumbnail Image
    ItemOpen Access
    THE SECD MACHINE ON A CHIP
    (1989-06-01) Birtwistle, G.; Graham, B.; Joyce, J.; Williams, S.; Brinsmead, M.; Keefe, M.; Kroeker, W.; Liblong, B.; Vollmerhaus, W.
    We describe work completed on the design, informal specification, and layout of a custom SECD machine. The chip contains around 25,000 transistors excluding memory cells. The work is part of a long term project which aims to support specification based VLSI design, build a library of cell and sub-system specifications, and investigate algorithms for transforming from specifications to other views.
  • Thumbnail Image
    ItemOpen Access
    VERIFYING SECD IN HOL
    (1991-01-01) Graham, B.; Birtwistle, G.
    This paper describes some of the work done at Calgary on the design of an SECD chip and its verification using the Cambridge HOL proof assistant. The chip is a physical realization of Henderson's variant of Landin's abstract architecture to execute the lambda calculus. The machine uses closures and includes explicit machine instructions to assist recursion. The complete proof, which goes from an abstract specification down to the transistor level, is far too involved to be covered in a single paper. In this paper, we discuss the SECD architecture and design and trace through a portion of the proof of correctness of one sequence of the microcode.