Bernhard Reus - Böcker
Visar alla böcker från författaren Bernhard Reus. Handla med fri frakt och snabb leverans.
2 produkter
2 produkter
496 kr
Skickas inom 10-15 vardagar
This textbook discusses the most fundamental and puzzling questions about the foundations of computing. In 23 lecture-sized chapters it provides an exciting tour through the most important results in the field of computability and time complexity, including the Halting Problem, Rice's Theorem, Kleene's Recursion Theorem, the Church-Turing Thesis, Hierarchy Theorems, and Cook-Levin's Theorem. Each chapter contains classroom-tested material, including examples and exercises. Links between adjacent chapters provide a coherent narrative.Fundamental results are explained lucidly by means of programs written in a simple, high-level imperative programming language, which only requires basic mathematical knowledge. Throughout the book, the impact of the presented results on the entire field of computer science is emphasised. Examples range from program analysis to networking, from database programming to popular games and puzzles. Numerous biographical footnotes about the famous scientists who developed the subject are also included."Limits of Computation" offers a thorough, yet accessible, introduction to computability and complexity for the computer science student of the 21st century.
Types for Proofs and Programs
International Workshop, TYPES '98, Kloster Irsee, Germany, March 27-31, 1998, Selected Papers
Häftad, Engelska, 1999
550 kr
Skickas inom 10-15 vardagar
Thisbookcontainsaselectionofpaperspresentedatthesecondannualworkshop heldundertheauspicesoftheEspritWorkingGroup21900Types. Theworkshop tookplaceinIrsee,Germany,from27to31ofMarch1998andwasattendedby 89researchers. Ofthe25submissions,14wereselectedforpublicationafteraregularref- eeingprocess. The?nalchoicewasmadebytheeditors. Thisvolumeisasequeltotheproceedingsfromthe?rstworkshopofthe workinggroup,whichtookplaceinAussois,France,inDecember1996. The proceedingsappearedinvol. 1512oftheLNCSseries,editedbyChristinePaulin- MohringandEduardoGim'enez. Theseworkshopsare,inturn,acontinuationofthemeetingsorganizedin 1993,1994,and1995undertheauspicesoftheEspritBasicResearchAction 6453 Types for Proofs and Programs. Thoseproceedingswerealsopublished intheLNCSseries,editedbyHenkBarendregtandTobiasNipkow(vol. 806, 1993),byPeterDybjer,BengtNordstr..omandJanSmith(vol. 996,1994)and byStefanoBerardiandMarioCoppo(vol. 1158,1995). TheEspritBRA6453 wasacontinuationoftheformerEspritAction3245Logical Frameworks: - sign,ImplementationandExperiments.Thearticlesfromtheannualworkshops organizedunderthatActionwereeditedbyGerardHuetandGordonPlotkin inthebooksLogical FrameworksandLogicalEnvironments,bothpublishedby CambridgeUniversityPress. Acknowledgments WewouldliketothankIrmgardMignaniandAgnesSzabo-Lackingerforhelping uswithprocessingtheregistrations,andRalphMatthesandMarkusWenzelfor organizationalsupportduringthemeeting. Weareindebtedtotheorganizersof theWorkingGroupTypesandalsotoPeterClote,TobiasNipkowandMartin Wirsingforgivingustheopportunitytoorganizethisworkshopandfortheir support. WewouldalsoliketoacknowledgefundingbytheEuropeanUnion. Thisvolumewouldnothavebeenpossiblewithouttheworkofthereferees. Theyarelistedonthenextpageandwethankthemfortheirinvaluablehelp. June1999 ThorstenAltenkirch WolfgangNaraschewski BernhardReus VI List of Referees PeterAczel PetriMa..enp..a..a ThorstenAltenkirch RalphMatthes GillesBarthe MichaelMendler HenkBarendregt WolfgangNaraschewski UliBerger TobiasNipkow MarcBezem SaraNegri VenanzioCapretta ChristinePaulin-Mohring MarioCoppo HenrikPersson CatarinaCoquand RandyPollack RobertoDiCosmo DavidPym GillesDowek ChristopheRa?alli MarcDymetman AarneRanta Jean-ChristopheFilliatre BernhardReus NeilGhani EikeRitter MartinHofmann GiovanniSambin MonikaSeisenberger FurioHonsell AntonSetzer PaulJackson JanSmith FelixJoachimski FlorianKammuller .. SergeiSoloview JamesMcKinna MakotoTakeyama Sim"aoMelodeSousa SilvioValentini ThomasKleymann MarkusWenzel HansLeiss BenjaminWerner Table of Contents OnRelatingTypeTheoriesandSetTheories...1 PeterAczel CommunicationModellingandContext-DependentInterpretation: AnIntegratedApproach...19 Ren'eAhn,TijnBorghuis Grobner .. BasesinTypeTheory ...33 ThierryCoquand,HenrikPersson AModalLambdaCalculuswithIterationandCaseConstructs...47 Jo..elleDespeyroux,PierreLeleu ProofNormalizationModulo ...62 GillesDowek,BenjaminWerner ProofofImperativeProgramsinTypeTheory...78 Jean-ChristopheFilliatre AnInterpretationoftheFanTheoreminTypeTheory ...93 DanielFridlender ConjunctiveTypesandSKInT...106 JeanGoubault-Larrecq ModularStructuresasDependentTypesinIsabelle ...121 FlorianKammul ..ler MetatheoryofVeri?cationCalculiinLEGO...133 ThomasKleymann BoundedPolymorphismforExtensibleObjects ...149 LuigiLiquori AboutE?ectiveQuotientsinConstructiveTypeTheory ...164 MariaEmiliaMaietti VIII AlgorithmsforEqualityandUni?cationinthePresenceof NotationalDe?nitions...179 FrankPfenning,CarstenSch..urmann APreviewoftheBasicPicture:ANewPerspectiveonFormalTopology. .194 GiovanniSambin,SilviaGebellato On Relating TypeTheories and Set Theories PeterAczel Departments of Mathematics and Computer Science Manchester University petera@cs. man. ac. uk Introduction 1 The original motivation for the work described in this paper was to det- minetheprooftheoreticstrengthofthetypetheoriesimplementedintheproof developmentsystemsLegoandCoq,[12,4]. Thesetypetheoriescombinetheim- 2 predicativetype of propositions , from the calculus of constructions,[5], with theinductivetypesandhierarchyoftypeuniversesofMartin-Lo..f'sconstructive typetheory,[13]. Intuitivelythereisaneasywaytodetermineanupperbound ontheprooftheoreticstrength. Thisistousethe'obvious'types-as-sets- terpretation of these type theories in a strong enough classical axiomatic set theory.