HOME > Detail View

Detail View

Higher order logic theorem proving and its applications : 7th international workshop, Valletta, Malta, September 19-22, 1994 : proceedings

Higher order logic theorem proving and its applications : 7th international workshop, Valletta, Malta, September 19-22, 1994 : proceedings (Loan 1 times)

Material type
단행본
Personal Author
Melham, T. F. (Tom F.) Camilleri, Juanito.
Title Statement
Higher order logic theorem proving and its applications : 7th international workshop, Valletta, Malta, September 19-22, 1994 : proceedings / Thomas F. Melham, Juanito Camilleri (eds.).
Publication, Distribution, etc
Berlin ;   New York :   Springer-Verlag ,   c1994.  
Physical Medium
ix, 470 p. : ill. ; 24 cm.
Series Statement
Lecture notes in computer science ; 859
ISBN
3540584501 (acid-free paper) 9783540584506
Bibliography, Etc. Note
Includes bibliographical references.
Subject Added Entry-Topical Term
Automatic theorem proving -- Congresses.
000 01062camuu2200277 a 4500
001 000045453810
005 20080716095508
008 940816s1994 gw a b 101 0 eng d
010 ▼a 94035140
020 ▼a 3540584501 (acid-free paper)
020 ▼a 9783540584506
035 ▼a (KERIS)REF000013960037
040 ▼a DLC ▼c DLC ▼d DLC ▼d 211009
050 0 0 ▼a QA76.9.A96 ▼b H54 1994b
082 0 0 ▼a 004/.01/5113 ▼2 22
090 ▼a 004.015113 ▼b H638 ▼c 7
245 0 0 ▼a Higher order logic theorem proving and its applications : ▼b 7th international workshop, Valletta, Malta, September 19-22, 1994 : proceedings / ▼c Thomas F. Melham, Juanito Camilleri (eds.).
260 ▼a Berlin ; ▼a New York : ▼b Springer-Verlag , ▼c c1994.
300 ▼a ix, 470 p. : ▼b ill. ; ▼c 24 cm.
440 0 ▼a Lecture notes in computer science ; ▼v 859
504 ▼a Includes bibliographical references.
650 0 ▼a Automatic theorem proving ▼v Congresses.
700 1 ▼a Melham, T. F. ▼q (Tom F.)
700 1 ▼a Camilleri, Juanito.
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 7 Accession No. 121173264 Availability Available Due Date Make a Reservation Service B M

Contents information

Table of Contents

LCF examples in HOL.- A graphical tool for proving UNITY progress.- Reasoning about a class of linear systems of equations in HOL.- Towards a HOL theory of memory.- Providing tractable security analyses in HOL.- Highlighting the lambda-free fragment of Automath.- First-order automation for higher-order-logic theorem proving.- Symbolic animation as a proof tool.- Datatypes in L2.- A formal theory of undirected graphs in higher-order logc.- Mechanical verification of distributed algorithms in higher-order logic.- Tracking design changes with formal verification.- Weak systems of set theory related to HOL.- Interval-semantic component models and the efficient verification of transaction-level circuit behavior.- An interpretation of Noden in HOL.- Reasoning about real circuits.- Binary decision diagrams as a HOL derived rule.- Trustworthy tools for trustworthy programs: A verified verification condition generator.- S: A machine readable specification notation based on higher order logic.- An engineering approach to formal digital system design.- Generating designs using an Algorithmic Register Transfer Language with formal semantics.- A HOL formalisation of the Temporal Logic of Actions.- Studying the ML module system in HOL.- Towards a mechanically supported and compositional calculus to design distributed algorithms.- Simplifying deep embedding: A formalised code generator.- Automating verification by functional abstraction at the system level.- A parameterized proof manager.- Implementational issues for verifying RISC-pipeline conflicts in HOL.- Specifying instruction-set architectures in HOL: A primer.- Representing higher-order logic proofs in HOL.


Information Provided By: : Aladin

New Arrivals Books in Related Fields

김종원 (2020)