LEADER 00826nam0-22003011i-450- 001 990000957100403321 010 $a0-306-39109-0 035 $a000095710 035 $aFED01000095710 035 $a(Aleph)000095710FED01 035 $a000095710 100 $a20000920d1977----km-y0itay50------ba 101 0 $aeng 200 1 $aAdvances in Nuclear Physics$fEdited by Michel Baranger, Erich Vogt 210 $aNew York$cPlenum Press$d1977 610 0 $aFisica nucleare 610 0 $aRadioattivitą 676 $a539.74$a539.752 700 1$aBaranger,$bMichel$044619 702 1$aVogt,$bErich 801 0$aIT$bUNINA$gRICA$2UNIMARC 901 $aBK 912 $a990000957100403321 952 $a34AI-106.008$b10586$fFI1 959 $aFI1 996 $aAdvances in nuclear physics$9186106 997 $aUNINA DB $aING01 LEADER 04012nam 22006735 450 001 9910298989403321 005 20200630053954.0 010 $a3-319-10542-6 024 7 $a10.1007/978-3-319-10542-0 035 $a(CKB)3710000000324994 035 $a(SSID)ssj0001408025 035 $a(PQKBManifestationID)11787282 035 $a(PQKBTitleCode)TC0001408025 035 $a(PQKBWorkID)11339716 035 $a(PQKB)11210506 035 $a(DE-He213)978-3-319-10542-0 035 $a(MiAaPQ)EBC5586501 035 $a(MiAaPQ)EBC6314781 035 $a(Au-PeEL)EBL5586501 035 $a(OCoLC)902703932 035 $a(Au-PeEL)EBL6314781 035 $a(PPN)183148606 035 $a(EXLCZ)993710000000324994 100 $a20141203d2014 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aConcrete Semantics $eWith Isabelle/HOL /$fby Tobias Nipkow, Gerwin Klein 205 $a1st ed. 2014. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2014. 215 $a1 online resource (XIII, 298 p. 87 illus., 1 illus. in color.) 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a3-319-10541-8 327 $aIntroduction -- Programming and Proving -- Case Study: IMP Expressions -- Logic and Proof Beyond Equality -- Isar: A Language for Structured Proofs -- IMP: A Simple Imperative Language -- Compiler -- Types -- Program Analysis -- Denotational Semantics -- Hoare Logic -- Abstract Interpretation -- App. A, Auxiliary Definitions -- App. B, Symbols -- References. 330 $aPart I of this book is a practical introduction to working with the Isabelle proof assistant. It teaches you how to write functional programs and inductive definitions and how to prove properties about them in Isabelle?s structured proof language. Part II is an introduction to the semantics of imperative languages with an emphasis on applications like compilers and program analysers. The distinguishing feature is that all the mathematics has been formalised in Isabelle and much of it is executable. Part I focusses on the details of proofs in Isabelle; Part II can be read even without familiarity with Isabelle?s proof language, all proofs are described in detail but informally. The book teaches the reader the art of precise logical reasoning and the practical use of a proof assistant as a surgical tool for formal proofs about computer science artefacts. In this sense it represents a formal approach to computer science, not just semantics. The Isabelle formalisation, including the proofs and accompanying slides, are freely available online, and the book is suitable for graduate students, advanced undergraduate students, and researchers in theoretical computer science and logic. 606 $aComputer logic 606 $aProgramming languages (Electronic computers) 606 $aMathematical logic 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aProgramming Languages, Compilers, Interpreters$3https://scigraph.springernature.com/ontologies/product-market-codes/I14037 606 $aMathematical Logic and Formal Languages$3https://scigraph.springernature.com/ontologies/product-market-codes/I16048 615 0$aComputer logic. 615 0$aProgramming languages (Electronic computers). 615 0$aMathematical logic. 615 14$aLogics and Meanings of Programs. 615 24$aProgramming Languages, Compilers, Interpreters. 615 24$aMathematical Logic and Formal Languages. 676 $a005.1015113 700 $aNipkow$b Tobias$4aut$4http://id.loc.gov/vocabulary/relators/aut$062010 702 $aKlein$b Gerwin$4aut$4http://id.loc.gov/vocabulary/relators/aut 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910298989403321 996 $aConcrete Semantics$91906162 997 $aUNINA