LEADER 01146nam--2200397---450- 001 990002021350203316 005 20060601084114.0 035 $a000202135 035 $aUSA01000202135 035 $a(ALEPH)000202135USA01 035 $a000202135 100 $a20040923d1984----km-y0itay0103----ba 101 0 $aita 102 $aIT 105 $a||||||||001yy 200 1 $aCos'è la musica$fHerbert Weinstock$gtraduzione di Lydia Lax 210 $aMilano$cA. Mondadori$d1984 215 $aIX, 416 p.$d18 cm. 225 2 $aOscar saggi$v92 410 0$12001$aOscar saggi$v92 454 1$12001$aWhat music is$939779 461 1$1001-------$12001 606 0 $aMusica$xStoria 676 $a780.9 700 1$aWEINSTOCK,$bHerbert$0450791 702 1$aLAX,$bLydia 801 0$aIT$bsalbc$gISBD 912 $a990002021350203316 951 $aXIII.3.B. 50(Varie coll. 338/92)$b16640/86 L.M.$cVarie coll. 959 $aBK 969 $aUMA 979 $aSIAV8$b10$c20040923$lUSA01$h1150 979 $aCOPAT3$b90$c20050124$lUSA01$h1128 979 $aCOPAT6$b90$c20060601$lUSA01$h0841 996 $aWhat music is$939779 997 $aUNISA LEADER 03128nam 22005535 450 001 9910682569803321 005 20251008165056.0 010 $z9781484292587 010 $a9781484292594 010 $a1484292596 024 7 $a10.1007/978-1-4842-9259-4 035 $a(CKB)5580000000525026 035 $a(DE-He213)978-1-4842-9259-4 035 $a(CaSebORM)9781484292594 035 $a(OCoLC)1373611992 035 $a(OCoLC-P)1373611992 035 $a(Perlego)4515907 035 $a(EXLCZ)995580000000525026 100 $a20230317d2023 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aIntroduction to Dependent Types with Idris $eEncoding Program Proofs in Types /$fby Boro Sitnikovski 205 $a1st ed. 2023. 210 1$aBerkeley, CA :$cApress :$cImprint: Apress,$d2023. 215 $a1 online resource (XVIII, 157 p. 139 illus.) 300 $aIncludes index. 311 08$a9781484292587 311 08$a1484292588 327 $aChapter 1: Formal Systems -- Chapter 2: Classical Mathematical Logic -- Chapter 3: Type Theory -- Chapter 4: Programming in Idris -- Chapter 5: Proving in Idris. 330 $aDependent types are a concept that allows developers to write proof-carrying code. Idris is a programming language that supports dependent types. This book will teach you the mathematical foundations of Idris as well as how to use it to write software and mathematically prove properties. The first part of the book serves as an introduction to the language's underlying theories. It starts by reviewing formal systems and mathematical logical systems as foundational building blocks, then gradually builds up to dependent types. Next, you'll learn type theory for dependent types. Following this, you'll explore the Idris programming language and conclude by exploring the depths of formal systems and type checkers by implementing them. Introduction to Dependent Types with Idris will walk you through simple examples through more advanced techniques, stepping up the difficulty as you gain more knowledge. Every chapter includes a set of exercises based on what it covered to further cement your learning. No specialized knowledge of mathematics is expected beyond the basics, so it is perfect for novices. You will: Understand Lambda calculus and dependent types Gain insight into functional programming Write mathematical proofs with Idris. 606 $aProgramming languages (Electronic computers) 606 $aSoftware engineering 606 $aProgramming Language 606 $aSoftware Engineering 615 0$aProgramming languages (Electronic computers) 615 0$aSoftware engineering. 615 14$aProgramming Language. 615 24$aSoftware Engineering. 676 $a005.13 700 $aSitnikovski$b Boro$4aut$4http://id.loc.gov/vocabulary/relators/aut$0847871 801 0$bOCoLC-P 801 1$bOCoLC-P 906 $aBOOK 912 $a9910682569803321 996 $aIntroduction to Dependent Types with Idris$93287700 997 $aUNINA