Browsing by Author "Slind, Konrad"

Now showing 1 - 8 of 8
  • Thumbnail Image
    Item
    Open Access
    An Implementation of higher order logic
    (1990) Slind, Konrad; Birtwistle, Graham M.
  • Thumbnail Image
    Item
    Open Access
    COMPLETION AS A DERIVED RULE OF INFERENCE
    (1990-10-01) Slind, Konrad
    A simple first step in the investigation of term rewriting systems in higher order logic is to just insert the first order completion algorithm unchanged into the more complicated logic. This paper presents the details of how this is done in Mike Gordon's HOL system, an implementation of Church's Simple Type Theory. We present completion as a derived rule of inference, not (as usual) as an ad hoc procedure. The completion rule presented here is easily adaptable to other natural deduction logics with equality.
  • Thumbnail Image
    Item
    Open Access
    HOL90 USER GUIDE
    (1992-08-01) Slind, Konrad
    No Abstract
  • Thumbnail Image
    Item
    Open Access
    AN IMPLEMENTATION OF HIGHER ORDER LOGIC
    (1991-01-01) Slind, Konrad
    In this thesis, we present an LCF-style implementation of Higher Order Logic. This is a re-implementation of Mike Gordon's hol88 system. We present the implementation in detail, and to a much lower level than previously. We formally specify the primitive algorithms of the implementation and make a start on proving the correctness of the implementation by verifying one of these algorithms. To augment the power of the theorem prover, we also integrate methods of proof from the field of Term Rewriting Systems into our implementation. This significantly enhances the equality reasoning capability of the system. Finally, we establish a formal link between circuit verification and chip production.
  • Thumbnail Image
    Item
    Open Access
    JADE virtual time implementation manual
    (1986-09-01) Unger, Brian W; Cleary, John; Lomow, Greg; Xining, Li; Zhonge, Xiao; Slind, Konrad
    No Abstract
  • Thumbnail Image
    Item
    Open Access
    Monitoring distributed systems
    (1985-11-01) Joyce, Jeffrey; Lomow, Greg; Slind, Konrad; Unger, Brian W
    The monitoring of distributed systems involves the collection, interpretation, and display of information concerning the interactions among concurrently executing processes. This information and its display can support the debugging, testing, performance evaluation, and dynamic documentation of distributed systems. General problems associated with monitoring are outlined in this paper, and the architecture of a general purpose, extensible, distributed monitoring system is presented. Three approaches to the display of process interactions are described: sequential textual traces, animated graphical traces, and a third which combines aspects of textual and graphical views to display a systems's evolution versus inter-process communication events. The roles that each of these types of tracing fulfill in monitoring and debugging distributed systems are identified and compared. Monitoring tools for collecting communication statistics, deadlock detection, controlling the non-deterministic execution of distributed systems, and the use of protocol specifications in monitoring are also described. Our discussion is based on experience in the development and use of a monitoring system within a distributed programming environment called Jade. The Jade environment was developed within the Computer Science Department of the University of Calgary and is now being used to support teaching and research within a number of university and research organisations.
  • Thumbnail Image
    Item
    Open Access
    OBJECT LANGUAGE EMBEDDING IN STANDARD ML OF NEW JERSEY
    (1991-12-01) Slind, Konrad
    Compiler support for user-defined parsers and prettyprinters has been added to SML/NJ. The notions of quotation and antiquotation and their implementation in terms of frag lists are explained. For prettyprinting, the 1980 TOPLAS algorithm of Oppen is now used by the compiler, and has been made available for users.
  • Thumbnail Image
    Item
    Open Access
    The TIPC user's manual
    (1987-02-01) Unger, Brian W; Slind, Konrad
    This manual documents the Tipc inter-process communication protocol, which supports the implementation of Virtual Time [Jefferson 85] systems. Tipc can be used to write distributed simulations, as well as, other distributed applications. Tipc was developed in the Jade environment [Jade 85], and, to a large extent, depends on Jade. This document should be self-contained in that a user shouldn't have to refer to other sources of information to get a Tipc program to run. However, if you are interested in the implementation of Tipc, see [Xiao et al. 86]. The original plan for the implementation of Tipc is presented in [Cleary et al. 85]. A discussion of potential optimisations in the implementations appear in [West et al.87]. For those who know the Jade IPC protocol (Jipc), Tipc was designed to mimic Jipc as closely as possible. Tipc can be viewed as Jipc augmented with facilities for handling time. Specifically, Tipc has a few extra parameters to some subroutine calls and an asynchronous send primitive. Currently, Tipc is accessible only from the C programming language. Preliminary ideas for a prolog version are described in [Li & Unger 87].