Recent developments in meta-logics and logical frameworks have lead to a new notion of syntax appropriate for specifying computations on such data structures as programs, formulas, proofs, types, and lambda- terms. New meta-programming languages and computer systems have already been designed around these new approaches to syntax. Semantics of meta programs seem to be best explained using combinations of proof theoretic concepts, Kripke models, realizability, and logical relations. This award supports further research into intuitutionistic, constructive, and linear logics. Much of this research is inspired by topics in computational logic, logic programming, and meta-programming. Theoretical results of this work will be applied to issues of programming language design so that logical principles of syntax can be made directly accessible to programmers and system builders and to keep a practical and experimental focus to this proposed research.
