000 03302nam a22005295i 4500
001 978-3-319-10542-0
003 DE-He213
005 20200420220222.0
007 cr nn 008mamaa
008 141203s2014 gw | s |||| 0|eng d
020 _a9783319105420
_9978-3-319-10542-0
024 7 _a10.1007/978-3-319-10542-0
_2doi
050 4 _aQA76.9.L63
050 4 _aQA76.5913
050 4 _aQA76.63
072 7 _aUM
_2bicssc
072 7 _aUYF
_2bicssc
072 7 _aCOM051000
_2bisacsh
072 7 _aCOM036000
_2bisacsh
082 0 4 _a005.1015113
_223
100 1 _aNipkow, Tobias.
_eauthor.
245 1 0 _aConcrete Semantics
_h[electronic resource] :
_bWith Isabelle/HOL /
_cby Tobias Nipkow, Gerwin Klein.
264 1 _aCham :
_bSpringer International Publishing :
_bImprint: Springer,
_c2014.
300 _aXIII, 298 p. 87 illus., 1 illus. in color.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
505 0 _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.
520 _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.
650 0 _aComputer science.
650 0 _aProgramming languages (Electronic computers).
650 0 _aComputer logic.
650 0 _aMathematical logic.
650 1 4 _aComputer Science.
650 2 4 _aLogics and Meanings of Programs.
650 2 4 _aProgramming Languages, Compilers, Interpreters.
650 2 4 _aMathematical Logic and Formal Languages.
700 1 _aKlein, Gerwin.
_eauthor.
710 2 _aSpringerLink (Online service)
773 0 _tSpringer eBooks
776 0 8 _iPrinted edition:
_z9783319105413
856 4 0 _uhttp://dx.doi.org/10.1007/978-3-319-10542-0
912 _aZDB-2-SCS
942 _cEBK
999 _c51964
_d51964