HOME > Detail View

Detail View

Higher order logic theorem proving and its applications : 6th International Workshop, HUG '93, Vancouver, B.C., Canada, August 11-13, 1993 : proceedings

Higher order logic theorem proving and its applications : 6th International Workshop, HUG '93, Vancouver, B.C., Canada, August 11-13, 1993 : proceedings (Loan 1 times)

Material type
단행본
Personal Author
Joyce, Jeffrey J. , 1960- Seger, Carl-Johan H.
Title Statement
Higher order logic theorem proving and its applications : 6th International Workshop, HUG '93, Vancouver, B.C., Canada, August 11-13, 1993 : proceedings / Jeffrey J. Joyce, Carl-Johan H. Seger, eds.
Publication, Distribution, etc
Berlin ;   New York :   Springer-Verlag ,   c1994.  
Physical Medium
ix, 517 p. : ill. ; 24 cm.
Series Statement
Lecture notes in computer science ; 780
ISBN
3540578269 (Berlin : acid-free paper) 0387578269 (New York : acid-free paper)
General Note
Papers presented at the 1993 HOL User's Group Workshop.  
Includes index.  
Subject Added Entry-Topical Term
Automatic theorem proving -- Congresses.
000 01246camuu2200301 a 4500
001 000045470662
005 20080917163629
008 940202s1994 gw a 101 0 eng
010 ▼a 94001560
020 ▼a 3540578269 (Berlin : acid-free paper)
020 ▼a 0387578269 (New York : acid-free paper)
035 ▼a (KERIS)REF000014724063
040 ▼a DLC ▼c DLC ▼d DLC ▼d 211009
050 0 0 ▼a QA76.9.A96 ▼b H54 1994
082 0 0 ▼a 004/.01/5113 ▼2 22
090 ▼a 004.015113 ▼b H638 ▼c 6
245 0 0 ▼a Higher order logic theorem proving and its applications : ▼b 6th International Workshop, HUG '93, Vancouver, B.C., Canada, August 11-13, 1993 : proceedings / ▼c Jeffrey J. Joyce, Carl-Johan H. Seger, eds.
260 ▼a Berlin ; ▼a New York : ▼b Springer-Verlag , ▼c c1994.
300 ▼a ix, 517 p. : ▼b ill. ; ▼c 24 cm.
440 0 ▼a Lecture notes in computer science ; ▼v 780
500 ▼a Papers presented at the 1993 HOL User's Group Workshop.
500 ▼a Includes index.
650 0 ▼a Automatic theorem proving ▼x Congresses.
700 1 ▼a Joyce, Jeffrey J. , ▼d 1960-
700 1 ▼a Seger, Carl-Johan H.
711 2 ▼a HOL User's Group Workshop ▼n (6th : ▼d 1993 : ▼c Vancouver, B.C.)
945 ▼a KINS

Holdings Information

No. Location Call Number Accession No. Availability Due Date Make a Reservation Service
No. 1 Location Science & Engineering Library/Sci-Info(Stacks2)/ Call Number 004.015113 H638 6 Accession No. 121175837 Availability Available Due Date Make a Reservation Service B M

Contents information

Table of Contents

Program verification using HOL-UNITY.- Graph model of LAMBDA in higher order logic.- Mechanizing a programming logic for the concurrent programming language microSR in HOL.- Reasoning with the formal definition of standard ML in HOL.- HOL-ML.- Structure and behaviour in hardware verification.- Degrees of formality in shallow embedding hardware description languages in HOL.- A functional approach for formalizing regular hardware structures.- A proof development system for the HOL theorem prover.- A HOL package for reasoning about relations defined by mutual induction.- A broader class of trees for recursive type definitions for HOL.- Some theorems we should prove.- Using PVS to prove some theorems of David Parnas.- Extending the HOL theorem prover with a computer algebra system to reason about the reals.- The HOL-Voss system: Model-checking inside a general-purpose theorem-prover.- Linking Higher Order Logic to a VLSI CAD system.- Alternative proof procedures for finite-state machines in higher-order logic.- A formalization of abstraction in LAMBDA.- Report on the UCD microcoded Viper verification project.- Verification of the Tamarack-3 microprocessor in a hybrid verification environment.- Abstraction techniques for modeling real-world interface chips.- Implementing a methodology for formally verifying RISC processors in HOL.- Domain theory in HOL.- Predicates, temporal logic, and simulations.- Formalization of variables access constraints to support compositionality of liveness properties.- The semantics of statecharts in HOL.- Value-passing CCS in HOL.- TPS: An interactive and automatic tool for proving theorems of type theory.- Modelling bit vectors in HOL: The word library.- Eliminating higher-order quantifiers to obtain decision procedures for hardware verification.- Toward a super duper hardware tactic.- A mechanisation of name-carrying syntax up to alpha-conversion.- A HOL decision procedure for elementary real algebra.- AC unification in HOL90.- Server-process restrictiveness in HOL.- Safety in railway signalling data: A behavioural analysis.- On the style of mechanical proving.- From abstract data types to shift registers:.- Verification in higher order logic of mutual exclusion algorithm.- Using Isabelle to prove simple theorems.


Information Provided By: : Aladin

New Arrivals Books in Related Fields

김종원 (2020)