Theorem Proving in Higher Order Logics : 9th International Conference, TPHOLs'96, Turku, Finland, August 26 - 30, 1996, Proceedings

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 submiss...

Full description

Corporate Author: SpringerLink (Online service)
Other Authors: Wright, Joakim von (Editor), Grundy, Jim (Editor), Harrison, John (Editor)
Format: eBook
Language:English
Published: Berlin, Heidelberg Springer Berlin Heidelberg 1996, 1996
Edition:1st ed. 1996
Series:Lecture Notes in Computer Science
Subjects:
Online Access:
Collection: Springer Book Archives -2004 - Collection details see MPG.ReNa
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 VDM-SL 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 alpha-conversion -- 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 high-level 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 higher-order logic -- Higher-order 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 639-2 
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 up-to-date report on the state of the art in this increasingly active field