LEADER 03531nam 2200625 450 001 9910557461103321 005 20230125181957.0 024 3 $a9780262317870 035 $a(CKB)2670000000528186 035 $a(SSID)ssj0001453548 035 $a(PQKBManifestationID)11825445 035 $a(PQKBTitleCode)TC0001453548 035 $a(PQKBWorkID)11491666 035 $a(PQKB)10595659 035 $a(CaBNVSL)mat06712486 035 $a(IDAMS)0b00006481ff4d7a 035 $a(IEEE)6712486 035 $a(OCoLC)872996245$z(OCoLC)881288988 035 $a(OCoLC-P)872996245 035 $a(MaCbMITP)9153 035 $a(MiAaPQ)EBC5966536 035 $a(oapen)https://directory.doabooks.org/handle/20.500.12854/78523 035 $a(PPN)258830824 035 $a(EXLCZ)992670000000528186 100 $a20151229d2013 uy 101 0 $aeng 135 $aur|n||||||||| 181 $ctxt 182 $cc 183 $acr 200 10$aCertified programming with dependent types $ea pragmatic introduction to the Coq proof assistant /$fAdam Chlipala 210 $aCambridge$cThe MIT Press$d2013 210 1$aCambridge, Massachusetts :$cMIT Press,$d[2013] 210 2$a[Piscataqay, New Jersey] :$cIEEE Xplore,$d[2013] 215 $a1 PDF (xii, 424 pages) 225 1 $aThe MIT Press 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a0-262-02665-1 311 $a0-262-31787-7 320 $aIncludes bibliographical references (pages [413]-417) and index. 330 $aThe technology of mechanized program verification can play a supporting role in many kinds of research projects in computer science, and related tools for formal proof-checking are seeing increasing adoption in mathematics and engineering. This book provides an introduction to the Coq software for writing and checking mathematical proofs. It takes a practical engineering focus throughout, emphasizing techniques that will help users to build, understand, and maintain large Coq developments and minimize the cost of code change over time. Two topics, rarely discussed elsewhere, are covered in detail: effective dependently typed programming (making productive use of a feature at the heart of the Coq system) and construction of domain-specific proof tactics. Almost every subject covered is also relevant to interactive computer theorem proving in general, not just program verification, demonstrated through examples of verified programs applied in many different sorts of formalizations. The book develops a unique automated proof style and applies it throughout; even experienced Coq users may benefit from reading about basic Coq concepts from this novel perspective. The book also offers a library of tactics, or programs that find proofs, designed for use with examples in the book. Readers will acquire the necessary skills to reimplement these tactics in other settings by the end of the book. All of the code appearing in the book is freely available online. 606 $aAutomatic theorem proving$xComputer programs 606 $aComputer programming 610 $aComputer programming / software engineering 615 0$aAutomatic theorem proving$xComputer programs. 615 0$aComputer programming. 676 $a005.1 700 $aChlipala$b Adam$f1981-$01207696 801 0$bCaBNVSL 801 1$bCaBNVSL 801 2$bCaBNVSL 906 $aBOOK 912 $a9910557461103321 996 $aCertified programming with dependent types$92786198 997 $aUNINA LEADER 01182nam a2200301 i 4500 001 991003271389707536 007 cr cn||||||||| 008 080129s2002 caua s 001 0 eng d 020 $a9780120839711 020 $a0120839717 035 $ab13658517-39ule_inst 040 $aDip.to Matematica$beng 082 04$a515.43$222 100 1 $aBear, Herbert Stanley$054344 245 12$aA primer of Lebesgue integration$h[e-book] /$cH. S. Bear 250 $a2nd ed. 260 $aSan Diego :$bAcademic Press,$cc2002 300 $axi, 164 p. :$bill. ;$c24 cm 500 $aIncludes index 650 0$aLebesgue integral 856 40$3ScienceDirect$uhttp://www.sciencedirect.com/science/book/9780120839711$zAn electronic book accessible through the World Wide Web; click for information 856 42$zPublisher description$uhttp://catdir.loc.gov/catdir/description/els031/2001092385.html 856 41$zTable of contents$uhttp://www.loc.gov/catdir/toc/els031/2001092385.html 907 $a.b13658517$b03-03-22$c29-01-08 912 $a991003271389707536 996 $aPrimer of Lebesgue integration$9924333 997 $aUNISALENTO 998 $ale013$b29-01-08$cm$d@ $e-$feng$gcau$h2$i0 LEADER 01582nam a2200313 i 4500 001 991003747649707536 008 080625r19951924nyu 000 0 eng 020 $a0899419550 035 $ab13745669-39ule_inst 040 $aDip.to Studi Giuridici$bita 041 1 $aenglat$hlat 100 1 $aGentili, Alberico,$d1552-1608$0242044 240 10$aDe legationibus libri tres.$lEnglish & Latin$953918 245 10$aDe legationibus libri tres /$cby Alberico Gentili 246 35$aThree books on embassies 260 $aBuffalo, N.Y. :$bW.S. Hein,$c1995 300 $a2 v. ;$c26 cm 500 $aPubblicazione originale: New York : Oxford University Press, 1924. (The classics of international law ; no. 12) (Publications of the Carnegie Endowment for International Peace, Division of International Law) 505 0 $aV. 1. La riproduzione fotografica dell'ed. 1594. - V. 2.: Three books on embassies / by Gordon J. Laing 650 4$aDiritto internazionale 830 0$aClassics of international law ;$vno. 12 830 0$aPublications of the Carnegie Endowment for International Peace, Division of International Law 907 $a.b13745669$b28-01-14$c25-06-08 912 $a991003747649707536 945 $aLE027 F/A II P CIL01.12$cV. 1$g1$i2027000211043$lle027$o-$pE80.86$q-$rn$so $t0$u0$v0$w0$x0$y.i14848909$z03-10-08 945 $aLE027 F/A II P CIL01.12$cV. 2$g1$i2027000211036$lle027$o-$pE76.82$q-$rn$so $t0$u0$v0$w0$x0$y.i14848910$z03-10-08 996 $aDe legationibus libri tres$953918 997 $aUNISALENTO 998 $ale027$b25-06-08$cm$da $e-$feng$gnyu$h0$i0