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

Joe Wells jbw at macs.hw.ac.uk
Sat May 26 14:18:49 EDT 2007


                          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

   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 in
   the ULTRA (Useful Logics, Types, Rewriting, and their Automation)
   group[1] in the Computer Science Department[2] in the School of
   Mathematical and Computer Sciences[3] at Heriot-Watt University[4] 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, human organizations, biological components,
       etc.).  Possible Poly* work includes:
          + Applying Poly* to the analysis of existing systems expressed
            in various existing process calculi.  This can include not
            just work on computer systems, but also work on business or
            biological processes.
          + Improving the implementation of algorithms related to Poly*.
            This includes better use of graph visualization tools for
            presenting Poly* types and more compositional and/or more
            efficient analysis algorithms.
          + Improving the theoretical strength of Poly* to encompass the
            power of more existing calculi, such as the
            single-threadedness of Safe Ambients, the different style of
            polymorphism of the polymorphic pi-calculus, the structured
            messages of the spi-calculus, the non-local reduction rules
            of bigraphs, the substitution of entire processes of the
            higher-order pi-calculus, etc.
          + And lots of other things!
     * 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:
          + Extending the MathLang framework to better handle more
            aspects of mathematical text.  This includes ways to connect
            mathematical text with its meaning, typesetting issues,
            document structure issues, informal and formal handling of
            argumentation and proof, etc.
          + Improving existing MathLang implementations.  This includes
            improving integration of MathLang support into the TeXmacs
            scientific WYSIWYG editor and better interfaces to other
            tools (including proof assistants (e.g., Coq, Mizar,
            Isabelle, OMEGA, etc.) and computer algebra systems).
          + Exercising and evaluating the MathLang framework through
            building libraries of computerized mathematical texts.
          + And lots of other things!
     * The idea of Expansion[11] as a fundamental organizing principle
       for obtaining flexible and compositional polymorphic type
       inference for computer software.  Possible work on expansion
       includes:
          + Expanding the scope of the expansion theory.  This includes
            extending it to handle "for all" (∀) quantifiers like those
            of System F, extending it to handle information flow for
            security analysis, and getting a better understanding of the
            semantics of the linearity control already incorporated in
            expansion theory.
          + Further improvement of the core theory, such as the expansion
            algebra, unification algorithms, type inference algorithms,
            and methods for proving subject reduction.
          + Various implementation work using expansion.  This includes
            type inference algorithms, better type error explanation
            methods, better data structures for representing analysis
            results, etc.
          + And lots of other things!
     * 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 expected duration of Ph.D. studentships in the UK is 3 years.  The
   positions will be expected to start around 2007-10-01; alternative
   start dates can be discussed.  Currently, funding is only available for
   EU citizens.  Non-EU-citizens are welcome to apply; they will either
   need their own funding or alternative funding will need to be found.

   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.macs.hw.ac.uk/ultra/
   2.  http://www.macs.hw.ac.uk/cs/
   3.  http://www.macs.hw.ac.uk/
   4.  http://www.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.

   For documents sent by e-mail, please use a public and standard format.
   The best formats are plain text and PDF.  LaTeX is okay if using only
   standard packages.  HTML is okay (if not generated by Microsoft Word).
   PostScript is ill-advised.  Open Document format is undesirable.
   Microsoft Word format is forbidden except where returning a form we
   have supplied in that format.

   For your information, it is helpful if the 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