Subject: Research Associateship in Metaprogramming Languages
From: Andrew Pitts (Andrew.Pitts@cl.cam.ac.uk)
Date: Wed Nov 01 2000 - 06:51:08 EST
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
This archive was generated by hypermail 2b28 : Wed Nov 01 2000 - 13:21:47 EST