01257nam 2200409 450 9900009369702033160-387-94531-80093697USA010093697(ALEPH)000093697USA01009369720020201d24-c----km-y0itay0103----baengUS||||||||001yyStochastic networksFrank P. Kelly, Ruth J. Williams editorsXXXI, 427 p.24 cmNew YorkSpringerc1995The IMA volumes in mathematics and its applicatrions712001The IMA volumes in mathematics and its applicatrions71Teoria delle code519.82KELLY,Frank P.WILLIAMS,Ruth J.ITsalbcISBD990000936970203316519.82 STO10961 ING519.82BKTECPATTY9020020201USA011055PATTY9020020201USA011100PATTY9020020201USA011101PATTY9020020201USA01110720020403USA011736PATRY9020040406USA011704Stochastic networks82536UNISA01053nam0-22003371i-450-99000573879040332120100713124505.0000573879FED01000573879(Aleph)000573879FED0100057387919990604d1966----km-y0itay50------balatitay---r---00---Tutte le operePublio Virgilio Maroneversione, introduzione e note di Enzio Centrangolocon un saggio di Antonio La PennaFirenzeSansoni©1966CIV, 888 p.23 cmLetteratura latinaVirgilio Marone PublioOpere870.01Vergilius Maro,Publius<70-19 a. C.>7260Cetrangolo,EnzioLa Penna,AntonioITUNINARICAUNIMARCBK990005738790403321P2B-650-VERG.M.-200A-1966ARCH. 12903FLFBCBIB. BAT. 702614723BATFLFBCBATOpera omnia52261UNINA04331nam 22007695 450 99646540700331620200702125154.03-540-45842-510.1007/3-540-45842-5(CKB)1000000000211678(SSID)ssj0000327459(PQKBManifestationID)11265772(PQKBTitleCode)TC0000327459(PQKBWorkID)10301621(PQKB)10491463(DE-He213)978-3-540-45842-5(MiAaPQ)EBC3072895(PPN)155232916(EXLCZ)99100000000021167820121227d2002 u| 0engurnn|008mamaatxtccrTypes for Proofs and Programs[electronic resource] International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000. Selected Papers /edited by Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack1st ed. 2002.Berlin, Heidelberg :Springer Berlin Heidelberg :Imprint: Springer,2002.1 online resource (VIII, 248 p.) Lecture Notes in Computer Science,0302-9743 ;2277Bibliographic Level Mode of Issuance: Monograph3-540-43287-6 Includes bibliographical references at the end of each chapters and index.Collection Principles in Dependent Type Theory -- Executing Higher Order Logic -- A Tour with Constructive Real Numbers -- An Implementation of Type:Type -- On the Logical Content of Computational Type Theory: A Solution to Curry’s Problem -- Constructive Reals in Coq: Axioms and Categoricity -- A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals -- A Kripke-Style Model for the Admissibility of Structural Rules -- Towards Limit Computable Mathematics -- Formalizing the Halting Problem in a Constructive Type Theory -- On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory -- Changing Data Structures in Type Theory: A Study of Natural Numbers -- Elimination with a Motive -- Generalization in Type Theory Based Proof Assistants -- An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument for Higman’s Lemma.Lecture Notes in Computer Science,0302-9743 ;2277Computer logicArchitecture, ComputerMathematical logicProgramming languages (Electronic computers)Artificial intelligenceLogics and Meanings of Programshttps://scigraph.springernature.com/ontologies/product-market-codes/I1603XComputer System Implementationhttps://scigraph.springernature.com/ontologies/product-market-codes/I13057Mathematical Logic and Foundationshttps://scigraph.springernature.com/ontologies/product-market-codes/M24005Mathematical Logic and Formal Languageshttps://scigraph.springernature.com/ontologies/product-market-codes/I16048Programming Languages, Compilers, Interpretershttps://scigraph.springernature.com/ontologies/product-market-codes/I14037Artificial Intelligencehttps://scigraph.springernature.com/ontologies/product-market-codes/I21000Computer logic.Architecture, Computer.Mathematical logic.Programming languages (Electronic computers).Artificial intelligence.Logics and Meanings of Programs.Computer System Implementation.Mathematical Logic and Foundations.Mathematical Logic and Formal Languages.Programming Languages, Compilers, Interpreters.Artificial Intelligence.006.3/33Callaghan Pauledthttp://id.loc.gov/vocabulary/relators/edtLuo Zhaohuiedthttp://id.loc.gov/vocabulary/relators/edtMcKinna Jamesedthttp://id.loc.gov/vocabulary/relators/edtPollack Robertedthttp://id.loc.gov/vocabulary/relators/edtTYPES 2000BOOK996465407003316Types for Proofs and Programs771867UNISA