[TYPES/announce] New PhD Studentships: Logics, Types, & Rewriting for Software & Mathematics @ Heriot-Watt, Scotland, UK

[Fairouz Kamareddine]

                          New 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

    Changes since our announcement earlier this year: (1) Additional
    positions have become available.  (2) Additional possible research
    topics have been included.

    Several new 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].

    Available research topics include work on any 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.
        MathLang tries to keep the computerization as close as possible to
        the mathematician's text while at the same time providing a formal
        structure supporting mathematical software systems (e.g., computer
        algebra systems, theorem provers, etc.).  Possible MathLang work
        includes:
           + Building libraries of computerized books of mathematics.
           + Developing bridges between MathLang and proof checkers (e.g.,
             Coq, Mizar, Isabelle, OMEGA, 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, including both theory and implementation.  In general, we
        are interested in the design and implementation of useful and
        elegant type systems and logics which can reason about or extend
        existing programming languages and theorem provers.

    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,
        such as the lambda calculus, higher-order rewriting (HOR), systems
        with explicit substitutions, higher-order abstract syntax (HOAS),
        combinators, etc.
      * Constraint solving and unification.
      * Theorem provers and mathematical reasoning tools.
      * 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 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.