[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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
