Tohoku University. Research Profiles


Programming Language Theory and Computation Models



Our laboratory conducts leading research on programming language theory and high-level computation models. In particular, we focus on research and application of (general proof methods for) program equivalence, functional programing, and type systems (also known as lightweight formal methods), which are attracting revived interests in recent years. Our Japanese translation of "Types and Programming Languages" (Benjamin C. Pierce, University of Pennsylvania)---compiled in cooperation with engineers from top-level electronics and software companies in Japan---has become the 42nd bestseller (rather exceptional as an academic Publications) among new books in For more information, please see the Web page:

Targeted Application(s)/Industry

Our technology can be used for design and development of software artifacts, especially programming languages and tools including DSL (domain specific languages), as well as application of functional programming, type systems, or formal methods.


Graduate School of Information Sciences

SUMII Eijiro , Professor


Related Information

A Bisimulation-Like Proof Method for Contextual Properties in Untyped lambda-Calculus with References and Deallocation. Eijiro Sumii. Theoretical Computer Science, Elsevier Science, the Netherlands, vol. 411, issues 51-52, pp. 4358-4378, December 2010.

A Bisimulation for Type Abstraction and Recursion. Eijiro Sumii and Benjamin C. Pierce. Journal of the ACM, vol. 54, issue 5, article 26, pp. 1-43, October 2007.