Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Fredrik Nordvall Forsberg <fredrik.nordvall-forsberg@strath.ac.uk>
To: agda@lists.chalmers.se, eutypes@cs.ru.nl,
	types-announce@lists.seas.upenn.edu,
	homotopytypetheory@googlegroups.com, coq-club@inria.fr,
	spls@lists.cent.gla.ac.uk
Subject: [HoTT] PhD studentships at the University of Strathclyde
Date: Mon, 4 Nov 2024 11:03:01 +0000	[thread overview]
Message-ID: <6baf665a-4caf-4d8d-b680-a42a66f8d4ab@strath.ac.uk> (raw)

Dear all,

The Department of Computer and Information Sciences at the University
of Strathclyde is welcoming applications for PhD studentships. At least
four fully funded positions are available for UK home students, and
funding covers tuition fees, a stipend for living expenses, and a
small travel budget. *Unfortunately, the funding provided is not enough
for non-UK tuition fees.*

Applicants in the area of the Mathematically Structured Programming
(MSP) Group are strongly encouraged to apply. Within MSP, we see the
mathematical foundations of computation and programming as
inextricably linked, and study one so as to develop the other. This
reflects the symbiotic relationship between mathematics, logic, and
programming — any attempt to sever this connection will diminish each
component.

For more information about MSP, please see:

     https://msp.cis.strath.ac.uk/

If you are interested in applying, please contact a potential
supervisor as soon as possible, and *before 25th November 2024*.
Potential supervisors in the group are:

* Guillaume Allais: type-driven programming, correct-by-construction
   methodology, implementations of type theory, generic programming,
   proof automation, user experience of interactive compilers.

* Robert Atkey: type theory and computational complexity, resource
   awareness in logic and programming languages, substructural logics,
   applications of mathematical structure to programming language
   design, domain specific languages for specification and verification.

* Neil Ghani: category theory, type theory, functional programming,
   game theory, machine learning.

* Jules Hedges: applications of category theory, type theory,
   functional programming, ... in economics, machine learning,
   statistics, control, ...

* Ross Horne: concurrency and logic, and their applications to
   analysing threats to security and privacy.

* Clemens Kupke: coalgebraic modelling of systems, logical
   verification/model-checking, fixpoint logics and their
   game-theoretic semantics, automata theory and automata learning.

* Conor Mc Bride: dependent type theory, functional programming,
   effects and handlers, programming language design and metatheory,
   and the category theoretic underpinnings of all of the above.

* Jan de Muijnck-Hughes: trustworthy systems using type-driven
   approaches; namely applications of type theory, dependently typed
   functional programming, and programming (& domain specific) language
   design and metatheory.

* Fredrik Nordvall Forsberg: dependent type theory, especially
   homotopy type theory, and its semantics and applications,
   constructive mathematics, categorical semantics of programming
   languages.

Best wishes,
The MSP Group
University of Strathclyde

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/HomotopyTypeTheory/6baf665a-4caf-4d8d-b680-a42a66f8d4ab%40strath.ac.uk.

                 reply	other threads:[~2024-11-04 11:03 UTC|newest]

Thread overview: [no followups] expand[flat|nested]  mbox.gz  Atom feed

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=6baf665a-4caf-4d8d-b680-a42a66f8d4ab@strath.ac.uk \
    --to=fredrik.nordvall-forsberg@strath.ac.uk \
    --cc=agda@lists.chalmers.se \
    --cc=coq-club@inria.fr \
    --cc=eutypes@cs.ru.nl \
    --cc=homotopytypetheory@googlegroups.com \
    --cc=spls@lists.cent.gla.ac.uk \
    --cc=types-announce@lists.seas.upenn.edu \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).