About the position
Context The candidate will be a member of the Picube team at the IRIF lab (irif.fr) and a member of the Malinca project (malinca.org). Assignment The objective of the position is to develop a "dictionary" of correspondences between topos theory and type theory, in particular between infinity-toposes and the calculus of inductive constructions (e.g. classifiers as possibly-univalent universes, Ω as hProp, fibered types as indexed types, ...) Main activities The work will notably consist in independent research and development, publications or implementations of the results obtained, participation to the research activities in proof theory at IRIF and laboratories nearby. Skills Technical skills and level required: expertise in homotopy type theory and infinity category theory. Languages: French and English
This listing was collected from a public source and is reproduced here for
information only. Always confirm the details on the original posting before applying.
View the original posting