Ò»±¾µÀÎÞÂë

My area of research can be described hierarchically as: mathematical logic, proof theory and the theory of computation, theory of programming languages (computer science), theory of functional programming, lambda calculus/ combinatory logic

Lambda calculus is the study of certain computation rules or programs. From among those programs which can be applied to arguments and return values we single out those whose execution depends only on the fact that some of the data are themselves computation rules of the same sort. It is not obvious that there are any non-trivial examples of such rules. The rich deep structure of the lambda calculus had to be discovered by Church, Bernays, Curry, Kleene and those who followed them. Since then, many distinctions have been made, such as those between applicative and functional programming, and many quite different type systems have evolved.

There is currently a great deal of research into lambda calculus by the programming language, theorem proving and symbolic computing communities. In our work we are interested in the deep structure of pure lambda calculus both with and without types. Roughly speaking our work falls into 6 general categories.

1. Typed lambda calculus and its extensions
2. Evaluation, reduction and conversion strategies
3. Combinators and combinatory algebra
4. Computability of functions and invariants
5. Functional equations and unification
6. Connections to other branches of mathematics such as semigroup theory.