



LEADER 
03707nmm a2200421 u 4500 
001 
EB000659810 
003 
EBX01000000000000000512892 
005 
00000000000000.0 
007 
cr 
008 
140122  eng 
020 


a 9783540706410

100 
1 

a Wright, Joakim von
e [editor]

245 
0 
0 
a Theorem Proving in Higher Order Logics
h Elektronische Ressource
b 9th International Conference, TPHOLs'96, Turku, Finland, August 26  30, 1996, Proceedings
c edited by Joakim von Wright, Jim Grundy, John Harrison

250 


a 1st ed. 1996

260 


a Berlin, Heidelberg
b Springer Berlin Heidelberg
c 1996, 1996

300 


a VIII, 447 p
b online resource

505 
0 

a Translating specifications in VDMSL to PVS  A comparison of HOL and ALF formalizations of a categorical coherence theorem  Modeling a hardware synthesis methodology in isabelle  Inference rules for programming languages with side effects in expressions  Deciding cryptographic protocol adequacy with HOL: The implementation  Proving liveness of fair transition systems  Program derivation using the refinement calculator  A proof tool for reasoning about functional programs  Coq and hardware verification: A case study  Elements of mathematical analysis in PVS  Implementation issues about the embedding of existing high level synthesis algorithms in HOL  Five axioms of alphaconversion  Set theory, higher order logic or both?  A mizar mode for HOL  Stålmarck’s algorithm as a HOL derived rule  Towards applying the composition principle to verify a microkernel operating system  A modular coding of UNITY in COQ  Importing mathematics from HOL into Nuprl  A structure preserving encoding of Z in isabelle/HOL  Improving the result of highlevel synthesis using interactive transformational design  Using lattice theory in higher order logic  Formal verification of algorithm W: The monomorphic case  Verification of compiler correctness for the WAM  Synthetic domain theory in type theory: Another logic of computable functions  Function definition in higherorder logic  Higherorder annotated terms for proof search  A comparison of MDG and HOL for hardware verification  A mechanisation of computability theory in HOL.

653 


a Logic Design

653 


a Mathematical Logic and Formal Languages

653 


a Software engineering

653 


a Mathematical logic

653 


a Software Engineering

653 


a Artificial Intelligence

653 


a Mathematical Logic and Foundations

653 


a Artificial intelligence

653 


a Logic design

653 


a Logics and Meanings of Programs

653 


a Computer logic

700 
1 

a Grundy, Jim
e [editor]

700 
1 

a Harrison, John
e [editor]

710 
2 

a SpringerLink (Online service)

041 
0 
7 
a eng
2 ISO 6392

989 


b SBA
a Springer Book Archives 2004

490 
0 

a Lecture Notes in Computer Science

856 


u https://doi.org/10.1007/BFb0105392?nosfx=y
x Verlag
3 Volltext

082 
0 

a 005.131

520 


a This book constitutes the refereed proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOL '96, held in Turku, Finland, in August 1996. The 27 revised full papers included together with one invited paper were carefully selected from a total of 46 submissions. The topics addressed are theorem proving technology, proof automation and decision procedures, mechanized theorem proving, extensions of higher order logics, integration of external tools, novel applications, and others. All in all, the volume is an uptodate report on the state of the art in this increasingly active field
