LEADER 04906nam  22007575  450 
001 996465502503316
005 20200706011548.0
010   $a3-540-69526-5
024 7 $a10.1007/BFb0028381
035   $a(CKB)1000000000234694
035   $a(SSID)ssj0000327168
035   $a(PQKBManifestationID)11244020
035   $a(PQKBTitleCode)TC0000327168
035   $a(PQKBWorkID)10298635
035   $a(PQKB)11172942
035   $a(DE-He213)978-3-540-69526-4
035   $a(PPN)155187791
035   $a(EXLCZ)991000000000234694
100   $a20121227d1997      u|             0
101 0 $aeng
135   $aurnn|008mamaa
181   $ctxt
182   $cc
183   $acr
200 10$aTheorem Proving in Higher Order Logics$b[electronic resource] $e10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings /$fedited by Elsa L. Gunter, Amy Felty
205   $a1st ed. 1997.
210  1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1997.
215   $a1 online resource (X, 346 p.) 
225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v1275
300   $aBibliographic Level Mode of Issuance: Monograph
311   $a3-540-63379-0 
327   $aAn Isabelle-based theorem prover for VDM-SL -- Executing formal specifications by translation to higher order logic programming -- Human-style theorem proving using PVS -- A hybrid approach to verifying liveness in a symmetric multi-processor -- Formal verification of concurrent programs in Lp and in Coq: A comparative analysis -- ML programming in constructive type theory -- Possibly infinite sequences in theorem provers: A comparative study -- Proof normalization for a first-order formulation of higher-order logic -- Using a PVS embedding of CSP to verify authentication protocols -- Verifying the accuracy of polynomial approximations in HOL -- A full formalisation of ?-calculus theory in the calculus of constructions -- Rewriting, decision procedures and lemma speculation for automated hardware verification -- Refining reactive systems in HOL using action systems -- On formalization of bicategory theory -- Towards an object-oriented progification language -- Verification for robust specification -- A theory of structured model-based specifications in Isabelle/HOL -- Proof presentation for Isabelle -- Derivation and use of induction schemes in higher-order logic -- Higher order quotients and their implementation in Isabelle HOL -- Type classes and overloading in higher-order logic -- A comparative study of Coq and HOL.
330   $aThis book constitutes the refereed proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs '97, held in Murray Hill, NJ, USA, in August 1997. The volume presents 19 carefully revised full papers selected from 32 submissions during a thorough reviewing process. The papers cover work related to all aspects of theorem proving in higher order logics, particularly based on secure mechanization of those logics; the theorem proving systems addressed include Coq, HOL, Isabelle, LEGO, and PVS.
410  0$aLecture Notes in Computer Science,$x0302-9743 ;$v1275
606   $aArchitecture, Computer
606   $aComputers
606   $aMathematical logic
606   $aLogic design
606   $aSoftware engineering
606   $aComputer logic
606   $aComputer System Implementation$3https://scigraph.springernature.com/ontologies/product-market-codes/I13057
606   $aTheory of Computation$3https://scigraph.springernature.com/ontologies/product-market-codes/I16005
606   $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048
606   $aLogic Design$3https://scigraph.springernature.com/ontologies/product-market-codes/I12050
606   $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029
606   $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X
615  0$aArchitecture, Computer.
615  0$aComputers.
615  0$aMathematical logic.
615  0$aLogic design.
615  0$aSoftware engineering.
615  0$aComputer logic.
615 14$aComputer System Implementation.
615 24$aTheory of Computation.
615 24$aMathematical Logic and Formal Languages.
615 24$aLogic Design.
615 24$aSoftware Engineering.
615 24$aLogics and Meanings of Programs.
676   $a004/.01/5113
702   $aGunter$b Elsa L$4edt$4http://id.loc.gov/vocabulary/relators/edt
702   $aFelty$b Amy$4edt$4http://id.loc.gov/vocabulary/relators/edt
712 12$aTPHOLs '97
906   $aBOOK
912   $a996465502503316
996   $aTheorem Proving in Higher Order Logics$9772309
997   $aUNISA