Professor Rob Nederpelt， Professor Herman Geuvers-Type Theory and Formal Proof_ An Introduction-Cambridge University Press (2014).pdf

《Professor Rob Nederpelt， Professor Herman Geuvers-Type Theory and Formal Proof_ An Introduction-Cambridge University Press (2014).pdf》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、TYPETHEORYANDFORMALPROOFTypetheoryisafast-evolvingfieldatthecrossroadsoflogic,computerscienceandmathematics.Thisgentlestep-by-stepintroductionisidealforgraduatestu-dentsandresearcherswhoneedtounderstandtheinsandoutsofthemathematicalmachinery,theroleoflogica

2、lrulestherein,theessentialcontributionofdefinitionsandthedecisivenatureofwell-structuredproofs.Theauthorsbeginwithuntypedlambdacalculusandproceedtoseveralfun-damentaltypesystems,includingthewell-knownandpowerfulCalculusofConstructions.Thebookalsocoversthees

3、senceofproofcheckingandproofdevelopment,andtheuseofdependenttypetheorytoformalisemathematics.Theonlyprerequisiteisabasicknowledgeofundergraduatemathematics.Carefullychosenexamplesillustratethetheorythroughout.Eachchapterendswithasummaryofthecontent,somehis

4、toricalcontext,suggestionsforfurtherreadingandaselectionofexercisestohelpreadersfamiliarisethemselveswiththematerial.RobNederpeltwasLecturerinLogicforComputerScienceuntilhisretire-ment.CurrentlyheisaguestresearcherintheFacultyofMathematicsandComputerScienc

5、eatEindhovenUniversityofTechnology,theNetherlands.HermanGeuversisProfessorinTheoreticalInformaticsattheRadboudUniversityNijmegen,andProfessorinProvingwithComputerAssistanceatEindhovenUniversityofTechnology,bothintheNetherlands.TYPETHEORYANDFORMALPROOFAnInt

6、roductionROBNEDERPELTEindhovenUniversityofTechnology,TheNetherlandsHERMANGEUVERSRadboudUniversityNijmegen,andEindhovenUniversityofTechnology,TheNetherlandsUniversityPrintingHouse,CambridgeCB28BS,UnitedKingdomCambridgeUniversityPressispartoftheUniversityofC

7、ambridge.ItfurtherstheUniversity’smissionbydisseminatingknowledgeinthepursuitofeducation,learningandresearchatthehighestinternationallevelsofexcellence.www.cambridge.orgInformationonthistitle:www.cambridge.org/9781107036505©RobNederpeltandHermanGeuvers2014

8、Thispublicationisincopyright.Subjecttostatutoryexceptionandtotheprovisionsofrelevantcollectivelicensingagreements,noreproductionofanypartmaytakeplacewithoutthewrittenpermissionofCambridgeUniversityPress.First