This area constitutes the mathematical foundation of information science (informatics). It includes type theory, mathematical logic (for computer science), program theory, program verification, theory on algorithm, information theory, coding theory, cryptology, and so on.

In the area of abstract theory of programming languages and mathematical logic, our education and research are carried out based on type theory and lambda-calculus, because they lie in the core of the programming languages and have close relationship with intuitionistic logic and substructural logic.

Program theory and formal verification enable us to apply such abstract theories mentioned above to actual computer programs. Besides the abstract theories, we need appropriate algorithms, data structures, and verification frameworks so as to use computers for verifying that the behavior of a program satisfies its specification.

On the other hand, among theories on algorithm, we focus on computation models and systems for efficient algorithms. Our education and research include also coding theory and cryptology which are fundamentals for reliable and secure network communications, and deal with algebra, theory of random numbers, computational complexity, information theory, cryptographic protocols, and so on. Those subjects are treated as discrete mathematics in a broad sense.

We are doing education and research for those subjects mentioned above.