|
School of Engineering
and Information Sciences Abstract Nominal techniques, the informal meta-level, and speculations Jamie Gabbay www.gabbay.org.uk Abstract Nominal techniques were originally developed in my PhD thesis as a method for defining inductive datatypes of syntax with binding. Since then I have developed them as a tool for logics and denotations for the informal meta-level of mathematical discourse (the language of a typical computer science paper, for example). The reason this is non-trivial is the same reason that nominal techniques were developed in the first place: handling name-binding. I will argue that, almost by accident, we have created a semantic and logical toolbox that is well-suited to meta-mathematical frameworks and to meta-programming---once we can specify e.g. beta-reduction and give this specification a rigorous but concrete semantics that is independent of functional application, then we are in a good position to at least try fine-tuning the intensional structure and to program both intensionally and extensionally on code. Two papers may illustrate what I have in mind: the lambda-context calculus and permissive-nominal logic. In my talk, I will give some details of what makes these languages "tick", and I will try to flesh out the speculation of the previous two paragraphs on possible future work. |
