[ The Types Forum (announcements only),
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

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 

Further details on the project and how to apply can be found here:
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.

Reply via email to