[TYPES/announce] Fully funded PhD scholarship at the IT University of Copenhagen

[Rasmus Ejlers Møgelberg]

Dear all,

As part of the research project Type Theories for Reactive Programming funded by Villum Fonden, I have an opening for a fully funded PhD scholarship at the IT University of Copenhagen starting this year. The aim of the project is to construct a (dependent) type theory for programming and reasoning about reactive systems, using modalities to encode productivity. The design of the type theory will be based on denotational models, so the ideal candidate will have knowledge of category theory and type theory, but this is not a requirement.

Further details on the project and how to apply can be found here:
https://tinyurl.com/y87wnwnq
Please feel free also to contact me directly for further details. A more detailed description of the project can be found below.

Best wishes,
Rasmus Møgelberg

-------------------------

Project description

Type theories are formal systems that can be viewed both as programming languages and logical systems for formalised mathematics. From a computer science perspective this is useful because it allows for programs, their specifications, and the proofs that these satisfy the specification to be expressed in the same formalism. The logical interpretation of type theories means that all programs must terminate. For this reason, programming and reasoning about non-terminating reactive programs in type theory remains a challenge. This is unfortunate since these include many of the most critical programs in use today.

In this project we aim to design a new type theory useful for programming with and reasoning about reactive programs. We build on recent progress in guarded recursion and functional reactive programming, using modal type constructors to capture productivity in types, as well as other recent advances in type theory, including homotopy type theory. We will use mathematical modelling when constructing the type theory and reasoning about consistency. The preferred candidate will therefore have knowledge of category theory and denotational semantics, but this is not a requirement. Experience with type theory or proof assistants is also an advantage, but not required.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20180223/f9260729/attachment.html>