[TYPES/announce] PhD Studentships: Logics, Types, & Rewriting for Software & Mathematics @ Heriot-Watt, Scotland, UK
Joe Wells
jbw at macs.hw.ac.uk
Thu Jun 1 11:37:45 EDT 2006
Ph.D. Student Positions
ULTRA group (Useful Logics, Types, Rewriting, and their Automation)
Computer Science Department
School of Mathematical and Computer Sciences
Heriot-Watt University
Edinburgh, Scotland, UK
The HTML version of this posting can be found at:
http://www.macs.hw.ac.uk/~jbw/phd-student-ad.html
Description of the Positions
Several Ph.D. student positions are available in areas involving
research into the theories of logics, types, and rewriting and their
applications in reasoning about computer systems and mathematics. The
positions are at Heriot-Watt University[1] in the ULTRA (Useful
Logics, Types, Rewriting, and their Automation) group[2] in the
Computer Science Department[3] in the School of Mathematical and
Computer Sciences[4] at Heriot-Watt University in Edinburgh[5], the
capital of Scotland[6]. The Ph.D. supervisors will be either
Fairouz Kamareddine[7] and/or Joe Wells[8].
Possible specific research topics include further development of any
one of the following:
* The Poly*[9] polymorphic retargetable type system for process and
mobility calculi, aimed at the goal of supporting modular
reasoning and compositional analysis for systems involving
mobility and concurrency (such systems can include combinations of
hardware, software, people, etc.).
* The MathLang[10] framework for computerizing mathematical text
where the computerization remains as close as possible to the
original language in which the mathematical text was written, and
yet acts as a formal structured style which can be used in
mathematical software systems (e.g., computer algebra systems,
theorem provers, etc.).
* The idea of Expansion[11] as a fundamental organizing principle
for obtaining flexible and compositional polymorphic type
inference for computer software.
* The use of Type Error Slicing[12] as a superior user interface for
explaining type errors to users of new programming languages with
advanced (and complicated!) type systems.
* Any other reasonable idea which builds on work we have already
started.
It will be helpful to have interests (or possibly even competence) in
1 or more of the following background knowledge areas:
* Formal calculi for reasoning about the meaning of systems
(including computer programs) such as the lambda calculus, the pi
calculus, and the numerous other calculi they have inspired that
deal with aspects of concurrency, mobility, modules, components,
linking & loading, resource usage, staged compilation, classes &
objects, etc.
* Methods for analyzing specific systems (e.g., specific computer
programs) represented by individual terms of such formal calculi.
* Formal calculi for representing mathematical texts, including
those aspects related to how actual practicing mathematicians
(i.e., not mathematical logicians) construct and present
mathematics.
* Type systems for the kinds of formal calculi mentioned above,
especially those with features similar to intersection, union,
dependent, and singleton types.
* Rewriting theories, especially those with higher-order features
(the lambda calculus is the canonical example, but this also
includes higher-order rewriting (HOR), systems with explicit
substitutions, combinators, etc.).
* Constraint solving and unification.
* Programming languages especially suitable for use for any of the
above.
The usual duration of Ph.D. studentships in the UK is 3 years. The
positions are available immediately.
The Ph.D. students will probably collaborate on 1 or more of the
following activities. The specific activities will be matched to their
strengths.
* Designing languages/calculi for representing various aspects of
such things as computer programs, concurrent systems, mathematical
texts, etc.
* Developing theories for reasoning about such a calculus as a whole
as well as individual terms written in the calculus.
* Developing new type systems for such calculi with useful
properties.
* Developing analysis algorithms for the new type systems.
* Proving various properties of the above items.
* Making software systems incorporating the new calculi, theories,
type systems, and algorithms.
* Publishing scientific reports on the work done.
References
1. http://www.hw.ac.uk/
2. http://www.macs.hw.ac.uk/ultra/
3. http://www.macs.hw.ac.uk/cs/
4. http://www.macs.hw.ac.uk/
5. http://www.geo.ed.ac.uk/home/tour/edintour.html
6. http://www.geo.ed.ac.uk/home/scotland/scotland.html
7. http://www.macs.hw.ac.uk/~fairouz/
8. http://www.macs.hw.ac.uk/~jbw/
9. http://www.macs.hw.ac.uk/DART/software/PolyStar/
10. http://www.macs.hw.ac.uk/~fairouz/talks/talks2005/mathlang-general-talk.pdf
11. http://www.macs.hw.ac.uk/~jbw/papers/#Car+Wel:ITRS-2004
12. http://www.macs.hw.ac.uk/ultra/compositional-analysis/type-error-slicing/
Contact Information
Inquiries can be directed to Fairouz Kamareddine at:
web: http://www.macs.hw.ac.uk/~fairouz/
e-mail: fairouz at macs.hw.ac.uk
fax: +44 131 451 8179
Inquiries can be directed to Joe Wells at:
web: http://www.macs.hw.ac.uk/~jbw/
e-mail: jbw at macs.hw.ac.uk
fax: +44 131 451 8179
Applying for the Positions
Please contact Fairouz Kamareddine and/or Joe Wells for full details
on how to apply. We will want to see your curriculum vitae, as well as
2 (or even 3 if possible) recommendation letters (preferably written
by people familiar with your academic and research abilities, but a
letter from an industry source is better than no letter at all). We
will expect recommendation letters to be sent directly by their
authors and will need contact details for the letter authors. You
should probably already have a master's degree or equivalent
experience. It can be helpful to write a brief statement about why
your research interests are a good match for the ULTRA group. If you
already have research publications (this is not required), it can be
helpful to send 1 (or even 2) of them. There will also be official
Heriot-Watt application forms to fill out. Please convert Microsoft
Word documents to a public, standard, and non-proprietary format. PDF
is good, plain text is good, LaTeX is okay (if using only standard
packages), HTML is okay (if not generated by Microsoft Word),
PostScript is sometimes okay, Open Document format is undesirable,
Microsoft Word format will not be accepted.
For your information, it is helpful if writers of recommendation
letters provide details of:
* the capacity in which they know the candidate,
* the candidate's skills, abilities and performance in relation to
the post applied for,
* the candidate's record including details of the candidate's
role(s) and service dates,
* their view of the candidate's suitability for the post as a whole,
in light of the attached details and their knowledge of the
candidate's experience and abilities,
* any further relevant information which would assist us in choosing
the right candidate.
More information about the Types-announce
mailing list