|
|
|
|
| LEADER |
02906nam a2200241 a 4500 |
| 001 |
502167 |
| 005 |
20171111225929.0 |
| 008 |
970718s1997 gw a b 101 0 eng |
| 020 |
|
|
|a 3540633790 (softcover : alk. paper)
|
| 050 |
|
|
|a QA76.9.A96
|b I577 1997
|
| 082 |
|
|
|2 21
|a 004/.01/5113
|
| 111 |
2 |
|
|a TPHOLs '97
|c Murray Hill, N.J.)
|d (1997 :
|
| 245 |
1 |
|
|a Theorem proving in higher order logics :
|b 10th International Conference, TPHOLs '97, Murray Hill, NJ, USA, August 19-22, 1997 :proceedings /
|c Elsa L. Gunter, Amy Felty, (eds.).
|
| 260 |
1 |
|
|a Berlin ;
|b Springer,
|c c1997.
|a New York :
|
| 300 |
1 |
|
|a viii, 337 p. :
|b ill. ;
|c 24 cm.
|
| 500 |
1 |
|
|a Proceedings of the tenth International Conference on Theorem Proving in Higher Order Logics.
|
| 504 |
1 |
|
|a Includes bibliographical references and index.
|
| 505 |
1 |
|
|a An Isabelle-based theorem prover for VDM-SL / Sten Agerholm and JacobFrost -- Executing formal specifications by translation to higher orderlogic programming / James H. Andrews -- Human-style theorem provingusing PVS / Myla Archer and Constance Heitmeyer -- A hybrid approach toverifying liveness in a symmetric multi-processor / Albert J. Camilleri-- Formal verification of concurrent programs in LP and in COQ : acomparative analysis / Boutheina Chetali and Barbara Heyd -- Invitedpaper : ML programming in constructive type theory / Robert L.Constable --Possibly infinite sequences in theorem provers : acomparative study / Marco Devillers, David Griffioen, and Olaf Muller-- Proof normalization for a first-order formulation of higher-orderlogic / Gilles Dowek --Using a PVS embedding of CSP to verifyauthentication protocols / Bruno Dutertre and Steve Schneider --Verifying the accuracy of polynomial approximations in HOL / JohnHarrison -- A full formalisation of [pi]-calculus theory in thecalculus of constructions / Daniel Hirschkoff -- Invited paper :rewriting, decision procedures and lemma speculation for automatedhardware verification / Deepak Kapur -- Refining reactive systems inHOL using action systems / Thomas Langbacka and Joakim von Wright --On formalization of bicategory theory / Takahisa Mohri --Towards anobject-oriented progification language / Wolfgang Naraschewski --Invited paper : verification for robust specification / Doron Peled --Atheory of structured model-based specifications in Isabelle/HOL /Thomas Santen -- Proof presentation for Isabelle / Martin Simons --Derivation and use of induction schemes in higher-order logic / KonradSlind --Higher order quotients and their implementation in Isabelle HOL/ Oscar Slotosch -- Type classes and overloading in higher-order logic/ Markus Wenzel -- A comparative study of Coq and HOL / Vincent Zammit.
|
| 650 |
1 |
|
|a Automatic theorem proving
|
| 700 |
1 |
|
|a Gunter, Elsa L.
|
| 700 |
1 |
|
|a Felty, Amy
|
| 711 |
2 |
|
|a TPHOLs '97
|c Murray Hill, N.J.)
|d (1997 :
|
| 952 |
|
|
|a GrThPMO
|b 59afe5bb6c5ad17d7e5a03b0
|c 952a
|d 9528
|e -
|t 1
|x m
|z Books
|
