POSTDOCTORAL RESEARCH ASSOCIATE IN METAPROGRAMMMING LANGUAGES at the UNIVERSITY OF CAMBRIDGE COMPUTER LABORATORY Cambridge, UK We are seeking a postdoctoral Research Associate to work on implementing an exciting new approach to representing, computing and reasoning about syntactical structures that involve variable-binding. START DATE: 1 January 2001, or as soon as possible thereafter. SALARY: 16,775--25,213 GBP per year, depending on age and qualifications. DURATION: 3 years. THE PROJECT: People who create software systems that manipulate syntactical structures (interpreters, compilers, proof checkers, proof assistants, etc) agree that dealing with variable-binding constructs, renaming of bound variables, capture-free substitution, etc, is very often a nightmare. Despite the efforts of many smart people, no clear winner has emerged from the different approaches to this problem that have been proposed so far---name-carrying terms, de Bruijn nameless terms, higher order abstract syntax. We have a new approach to this long-standing problem based on some simple mathematics to do with permuting variables. We think it is very exciting because our way of representing abstract syntax modulo renaming of bound names seems to integrate very well with the inductive data types and pattern-matching facilities of existing functional programming languages commonly used for metaprogramming activities, such as ML or Haskell. Roughly speaking, we are aiming to extend those languages so that the user can write syntax-manipulating code using explicitly named bound variables and be notified by the language's static type system if their code descends below the level of abstraction that identifies pieces of syntax up to renaming bound variables. Can our new approach be implemented efficiently? Does it result in a programming style that's useful for metaprogramming and that aids refining and reasoning about such programs? That's what we aim to find out. The project is called "FreshML: A Fresh Approach to Name Binding in Metaprogramming Languages" and is funded by the UK EPSRC and Microsoft Research. It is led by Andrew Pitts in collaboration with Mike Gordon at the Cambridge University Computer Laboratory and Simon Peyton Jones at the Cambridge Laboratory of Microsoft Research. See the FreshML web page at <www.cl.cam.ac.uk/users/amp12/freshml/> for more details. THE JOB: We are looking for an experienced hacker (in the best sense of the word) to design and implement a new language, FreshML, embodying our new approach to binding. You need to have enough brain-power to understand the FreshML type system and dynamic semantics, and you will have an opportunity to contribute to them---but the main areas where we need your help are in the design of a programming language to embody the type system, an implementation to demonstrate its practicality, and significant examples of its use. You should hold a PhD or equivalent qualification and have experience with the implementation of typed functional programming languages such as ML or Haskell. Experience with systems for machine-assisted reasoning or with programming language theory will be advantageous. THE ENVIRONMENT: You will be based in the Cambridge University Computer Laboratory (currently located in central Cambridge, but which will move to purpose-built accommodation on the west side of the city during late summer 2001). Further details of the Computer Laboratory can be found at <www.cl.cam.ac.uk>. The FreshML project involves the Laboratory's Theory and Semantics research group <www.cl.cam.ac.uk/Research/TSG/> and the Automated Reasoning research group <www.cl.cam.ac.uk/Research/HVG/>. It also involves collaboration with the Programming Principles & Tools group at Microsoft Research Cambridge <research.microsoft.com/ppt/>. HOW TO APPLY: Send a full CV, names of at least two referees, and a brief statement saying how you think you fit the post, what you expect to contribute, and what you hope to get out of the job, to: Ms Caroline Bean Cambridge University Computer Laboratory Pembroke Street Cambridge CB2 3QG, UK email: Caroline.Bean@cl.cam.ac.uk tel: +44 1223 334607 fax: +44 1223 334611 ENQUIRIES about this job should be directed to: Andrew Pitts, Cambridge University Computer Laboratory, Pembroke Street, Cambridge CB2 3QG, UK (email: Andrew.Pitts@cl.cam.ac.uk, tel: +44 1223 334629). CLOSING DATE FOR APPLICATIONS: 1 December 2000