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