02001nam 2200553Ia 450 991044981060332120200520144314.01-280-26273-797866102627310-309-54991-4(CKB)1000000000245161(EBL)3377999(SSID)ssj0000279120(PQKBManifestationID)11219283(PQKBTitleCode)TC0000279120(PQKBWorkID)10259549(PQKB)10737892(MiAaPQ)EBC3377999(Au-PeEL)EBL3377999(CaPaEBR)ebr10091297(CaONFJC)MIL26273(OCoLC)923275400(EXLCZ)99100000000024516120051104d2005 uy 0engur|n|---|||||txtccrEngineering research and America's future[electronic resource] meeting the challenges of a global economy /Committee to Assess the Capacity of the U.S. Engineering Research Enterprise, National Academy of Engineering of the National AcademiesWashington, D.C. National Academies Pressc20051 online resource (60 p.)Description based upon print version of record.0-309-09642-1 Includes bibliographical references (p. 31-34).""PREFACE""; ""ACKNOWLEDGMENTS""; ""CONTENTS""; ""EXECUTIVE SUMMARY""; ""ENGINEERING RESEARCH: THE ENGINE OF INNOVATION""; ""ANNOTATED BIBLIOGRAPHY""; ""COMMITTEE BIOGRAPHIES""EngineeringResearchUnited StatesTechnological innovationsUnited StatesElectronic books.EngineeringResearchTechnological innovations620.0072073MiAaPQMiAaPQMiAaPQBOOK9910449810603321Engineering research and America's future2048078UNINA02709oam 2200601 450 99646584820331620210716142137.03-540-48167-210.1007/3-540-48167-2(CKB)1000000000211114(SSID)ssj0000327466(PQKBManifestationID)11245707(PQKBTitleCode)TC0000327466(PQKBWorkID)10301359(PQKB)10139598(DE-He213)978-3-540-48167-6(MiAaPQ)EBC3072208(MiAaPQ)EBC6486374(PPN)155185039(EXLCZ)99100000000021111420210716d1999 uy 0engurnn|008mamaatxtccrTypes for proofs and programs International Workshop, TYPES '98, Kloster Irsee, Germany, March 27-31, 1998 : selected papers /Thorsten Altenkirch, Wolfgang Naraschewski, Bernhard Reus, editors1st ed. 1999.Berlin ;Heidelberg :Springer,[1999]©19991 online resource (VIII, 212 p.) Lecture Notes in Computer Science ;1657Bibliographic Level Mode of Issuance: Monograph3-540-66537-4 Includes bibliographical references.On Relating Type Theories and Set Theories -- Communication Modelling and Context-Dependent Interpretation: An Integrated Approach -- Gröbner Bases in Type Theory -- A Modal Lambda Calculus with Iteration and Case Constructs -- Proof Normalization Modulo -- Proof of Imperative Programs in Type Theory -- An Interpretation of the Fan Theorem in Type Theory -- Conjunctive Types and SKInT -- Modular Structures as Dependent Types in Isabelle -- Metatheory of Verification Calculi in LEGO -- Bounded Polymorphism for Extensible Objects -- About Effective Quotients in Constructive Type Theory -- Algorithms for Equality and Unification in the Presence of Notational Definitions -- A Preview of the Basic Picture: A New Perspective on Formal Topology.Lecture notes in computer science ;1657.Automatic theorem provingCongressesType theoryCongressesAutomatic theorem provingType theory004.015113Altenkirch Thorsten1962-930976Naraschewski Wolfgang1970-1252366Reus Bernhard1965-934969TYPES '98MiAaPQMiAaPQUtOrBLWBOOK996465848203316Types for proofs and programs2903403UNISA