アイブーストアプリ

入学希望の方 修了生の方 企業・研究者の方 教職員・学生 //--> Sitemap Access Japanese About GSISMessage from the DeanIntroduction to GSISGSIS guide bookOrganizationSNSJournal: Interdisciplinary Information SciencesContactsFacultyLaboratories by DepartmentComputer and Mathematical SciencesSystem Information SciencesHuman-Social Information SciencesApplied Information SciencesLaboratories by Specialized Subject GroupColaborative LaboratoriesPromotion OfficeAdmissionEntrance ExaminationCurriculum and Qualifications for ApplicationResearch StudentDormitoryFor StudentsSyllabus / Time table / Student HandbookNoticeInternational StudentsScholarshipDormitoryAdmission fee / Tuition fee waiverHandbook for International StudentsJapanese Language ProgramCounseling servicesEmergency InformationInternal Access Only Home Faculty Laboratories by Department Logic for Information Science Computer and Mathematical Sciences Logic for Information Science A13 Prof. Keisuke Nakano       Assis. Prof. Kazuyuki Asada       Assis. Prof. Kentaro Kikuchi     Lab's Web page KeywordsProgramming Language Theory, Formal Language Theory, Theorem Proving Filling a gap between humans and computers  Our ultimate goal is to fill a gap between humans and computers on programming. A human-readable description may put a burden on computers due to inefficient execution, while a computer-oriented (well-tuned) description may put a burden on humans due to knotty development. Our goals are to derive a well-tuned program from a human-readable description and to certify that well-tuned complicated programs work as humans intend.   Our research focuses on formal tree language theory that can deal with abstracted computations.  Specifically, we study a theory of tree automata and transducers to develop a framework which enables to automatically derive efficient programs and statically check properties desired by programmers.  Additionally, we use a proof assistant tool to certify the correctness of our theory.   We also study semantics of programming languages. This gives a kind of program abstraction which keeps all the semantical properties of programs. Through the abstraction and mathematical analysis, we clarify the essence of a target programming language. We apply denotational, operational, axiomatic, and categorical semantics to a theoretical design of programming languages and program verification.  Experimental result that illustrates effect of a program transformation based on formal tree language theory (where both time and space efficiency are improved in comparison with an existing implementation)  Coinductive formalization of validity of toss juggling patterns and its certification in the Coq proof assistant FacultyLaboratories by DepartmentComputer and Mathematical SciencesSystem Information SciencesHuman-Social Information SciencesApplied Information SciencesLaboratories by Specialized Subject GroupColaborative LaboratoriesPromotion Office GSIS: Graduate School of Information Sciences, Tohoku University 6-3-09 Aoba, Aramaki-aza Aoba-ku, Sendai, 980-8579, Japan Phone.+81-22-795-5813 Fax. +81-22-795-5815 Contacts is-www-admin,is.tohoku.ac.jp --> About GSIS Message from the DeanIntroduction to GSISGSIS guide bookOrganizationSNSJournal: Interdisciplinary Information SciencesContacts Faculty Laboratories by DepartmentComputer and Mathematical SciencesSystem Information SciencesHuman-Social Information SciencesApplied Information SciencesLaboratories by Specialized Subject GroupColaborative LaboratoriesPromotion Office Admission Entrance ExaminationCurriculum and Qualifications for ApplicationResearch StudentDormitory For Students Syllabus / Time table / Student HandbookNoticeInternational StudentsScholarshipDormitoryAdmission fee / Tuition fee waiverHandbook for International StudentsJapanese Language ProgramCounseling servicesEmergency InformationInternal Access Only About this Website Link © 2016 Graduate School of Information Sciences, Tohoku University About GSIS Message from the DeanIntroduction to GSISGSIS guide bookOrganizationSNSJournal: Interdisciplinary Information SciencesContacts Faculty Laboratories by DepartmentComputer and Mathematical SciencesSystem Information SciencesHuman-Social Information SciencesApplied Information SciencesLaboratories by Specialized Subject GroupColaborative LaboratoriesPromotion Office Admission Entrance ExaminationCurriculum and Qualifications for ApplicationResearch StudentDormitory For Students Syllabus / Time table / Student HandbookNoticeInternational StudentsScholarshipDormitoryAdmission fee / Tuition fee waiverHandbook for International StudentsJapanese Language ProgramCounseling servicesEmergency InformationInternal Access Only Sitemap Access Japanese no cache