[TYPES/announce] Postdoc position at IT University of Copenhagen

[Rasmus Ejlers Møgelberg]

Dear all,

I would like to advertise a 2-year postdoc position available at the IT University of Copenhagen, Denmark. The suggested starting date is August 2017, but this is negotiable. The position is part of my research project Type Theories for Reactive Programming funded by Villum Fonden, and running for 5 years involving 2 PhDs and 2 postdoc positions in total. I include a short description of the goals of the project below.

Applicants should have experience with category theory and denotational semantics. Knowledge of models of (dependent) type theory or functional reactive programming is an advantage, but is not required.

The deadline for application is February 28. Further information on the position and how to apply can be found here:
http://bit.ly/2kl7zRy

I encourage all interested in applying to contact me in advance.

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 modalities to capture productivity in types.

The project also involves the development of Guarded Cubical Type Theory, an extension of Cubical Type Theory with guarded recursive types. These can be used for smooth programming with coinductive types and construction of models of advanced programming languages. This part of the project is a collaboration with professor Lars Birkedal at Aarhus University.

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 modalities to capture productivity in types.

The project also involves the development of Guarded Cubical Type Theory, an extension of Cubical Type Theory with guarded recursive types. These can be used for smooth programming with coinductive types and construction of models of advanced programming languages. This part of the project is a collaboration with professor Lars Birkedal at Aarhus University.
- See more at: https://candidate.hr-manager.net/ApplicationInit.aspx?cid=119&ProjectId=180828&MediaId=5#sthash.uggmBukd.dpu
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 modalities to capture productivity in types.

The project also involves the development of Guarded Cubical Type Theory, an extension of Cubical Type Theory with guarded recursive types. These can be used for smooth programming with coinductive types and construction of models of advanced programming languages. This part of the project is a collaboration with professor Lars Birkedal at Aarhus University.
- See more at: https://candidate.hr-manager.net/ApplicationInit.aspx?cid=119&ProjectId=180828&MediaId=5#sthash.uggmBukd.dpuf
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 modalities to capture productivity in types.

The project also involves the development of Guarded Cubical Type Theory, an extension of Cubical Type Theory with guarded recursive types. These can be used for smooth programming with coinductive types and construction of models of advanced programming languages. This part of the project is a collaboration with professor Lars Birkedal at Aarhus University.
- See more at: https://candidate.hr-manager.net/ApplicationInit.aspx?cid=119&ProjectId=180828&MediaId=5#sthash.uggmBukd.dpu
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 modalities to capture productivity in types.

The project also involves the development of Guarded Cubical Type Theory, an extension of Cubical Type Theory with guarded recursive types. These can be used for smooth programming with coinductive types and construction of models of advanced programming languages. This part of the project is a collaboration with professor Lars Birkedal at Aarhus University.
- See more at: https://candidate.hr-manager.net/ApplicationInit.aspx?cid=119&ProjectId=180828&MediaId=5#sthash.uggmBukd.dpufProject 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 modalities to capture productivity in types.

The project also involves the development of Guarded Cubical Type Theory, an extension of Cubical Type Theory with guarded recursive types. These can be used for smooth programming with coinductive types and construction of models of advanced programming languages. This part of the project is a collaboration with professor Lars Birkedal at Aarhus University.
- See more at: https://candidate.hr-manager.net/ApplicationInit.aspx?cid=119&ProjectId=180828&MediaId=5#sthash.uggmBukd.dpuf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20170203/306ff78c/attachment-0001.html>