LEADER 05358nam 22007575 450 001 996465954203316 005 20231210212159.0 010 $a3-540-70641-0 024 7 $a10.1007/BFb0105392 035 $a(CKB)1000000000548903 035 $a(SSID)ssj0000327167 035 $a(PQKBManifestationID)11268690 035 $a(PQKBTitleCode)TC0000327167 035 $a(PQKBWorkID)10297638 035 $a(PQKB)10060207 035 $a(DE-He213)978-3-540-70641-0 035 $a(PPN)155226037 035 $a(EXLCZ)991000000000548903 100 $a20121227d1996 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] $e9th International Conference, TPHOLs'96, Turku, Finland, August 26 - 30, 1996, Proceedings /$fedited by Joakim von Wright, Jim Grundy, John Harrison 205 $a1st ed. 1996. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1996. 215 $a1 online resource (VIII, 447 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v1125 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-540-61587-3 327 $aTranslating 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. 330 $aThis 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. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v1125 606 $aMathematical logic 606 $aArtificial intelligence 606 $aLogic design 606 $aComputer logic 606 $aSoftware engineering 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 606 $aArtificial Intelligence$3https://scigraph.springernature.com/ontologies/product-market-codes/I21000 606 $aLogic Design$3https://scigraph.springernature.com/ontologies/product-market-codes/I12050 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aMathematical Logic and Foundations$3https://scigraph.springernature.com/ontologies/product-market-codes/M24005 606 $aSoftware Engineering$3https://scigraph.springernature.com/ontologies/product-market-codes/I14029 615 0$aMathematical logic. 615 0$aArtificial intelligence. 615 0$aLogic design. 615 0$aComputer logic. 615 0$aSoftware engineering. 615 14$aMathematical Logic and Formal Languages. 615 24$aArtificial Intelligence. 615 24$aLogic Design. 615 24$aLogics and Meanings of Programs. 615 24$aMathematical Logic and Foundations. 615 24$aSoftware Engineering. 676 $a004/.01/5113 702 $aWright$b Joakim von$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aGrundy$b Jim$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aHarrison$b John$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aTPHOLs '96 906 $aBOOK 912 $a996465954203316 996 $aTheorem Proving in Higher Order Logics$9772309 997 $aUNISA 999 $aautbn agw scala? z 9912102179205606 LEADER 01362nam1 22003373i 450 001 TO00027894 005 20251003044401.0 100 $a20130920d1984 ||||0itac50 ba 101 | $aita 102 $ait 181 1$6z01$ai $bxxxe 182 1$6z01$an 200 1 $aCorso di storia$eper licei e istituti magistrali$fG. Cracco, A. Prandi, F. Traniello 205 $aNuova ed 210 $aTorino$cSEI$dcopyr. 1984 215 $a3 v.$cill.$d24 cm. 463 1$1001TO00027924$12001 $aˆ3: ‰Storia contemporanea$fFrancesco Traniello$v3 606 $aStoria$2FIR$3CFIC003410$9E 676 $a900.71$9GEOGRAFIA, STORIA E DISCIPLINE AUSILIARIE. Educazione$v23 700 1$aCracco$b, Giorgio$f <1934- >$3CFIV022814$4070$0166876 701 1$aTraniello$b, Francesco$3CFIV008769$4070$0156562 701 1$aPrandi$b, Alfonso$3CFIV039169$4070$0159321 801 3$aIT$bIT-000000$c20130920 850 $aIT-BN0095 901 $bNAP 01$cPOZZO LIB.$nVi sono collocati fondi di economia, periodici di ingegneria e scienze, periodici di economia e statistica e altri fondi comprendenti documenti di economia pervenuti in dono. 912 $aTO00027894 950 1$aBiblioteca Centralizzata di Ateneo$bv. 3$cv. 3$d 01POZZO LIB.DONI DEMM 26 967 $m1 977 $a 01 996 $aCorso di storia$9591926 997 $aUNISANNIO