[TYPES/announce] Postdoc in Chambéry
Tom Hirschowitz
tom.hirschowitz at univ-smb.fr
Mon Nov 18 09:11:44 EST 2024
Hi all,
The LAMA
https://urldefense.com/v3/__https://lama.univ-smb.fr__;!!IBzWLUs!XK6LrPbdtJuNxP7lWy7LjtjGqlFi8kU1tZHv2fB-QBSarOv-dn5NYLuWMgNaZCQ3BItus4w-L1IgNjd1rDMEdPMObqNz8Qq-bWPKq8-nqm6hmw$
offers a full-time, 18 month postdoc position starting February 2025. The deadline is really soon: December 9!
(Although the position should be re-published if not filled.)
The details are here
https://urldefense.com/v3/__https://univ-smb.nous-recrutons.fr/poste/nzyn17a55c-chercheur-post-doctorant-fh-usmb-shine-guli-anr-22-exes-0017/__;!!IBzWLUs!XK6LrPbdtJuNxP7lWy7LjtjGqlFi8kU1tZHv2fB-QBSarOv-dn5NYLuWMgNaZCQ3BItus4w-L1IgNjd1rDMEdPMObqNz8Qq-bWPKq8_Wy_MVJA$
and there
https://urldefense.com/v3/__https://www.univ-smb.fr/wp-content/uploads/2024/11/offre-emploi-post-doc-2024-100__lama_guli_vf.pdf__;!!IBzWLUs!XK6LrPbdtJuNxP7lWy7LjtjGqlFi8kU1tZHv2fB-QBSarOv-dn5NYLuWMgNaZCQ3BItus4w-L1IgNjd1rDMEdPMObqNz8Qq-bWPKq88sRpfLBQ$
but let us give a brief summary.
Most numerical simulation programs compute with very little checks for physical consistency. Typically, adding a
length (in metres) to a force (in newtons) is not detected as an error by the programming language. But the very
purpose of type systems is to detect inconsistencies of a similar nature. E.g., they prevent addition of numerical
values with arrays. Until now, programming language theorists have proposed solutions that are conceptually clear,
but too naive to cover all use cases. On the other hand, other attempts tried to handle numerous cases
independently, but eventually came out as too complex to be usable.
The goal of the present postdoc position is to try and design a conceptually clear solution covering all use cases.
The successful applicant will be based at LAMA, and work with Tom Hirschowitz and Pierre Hyvernat, but also with
Vincent Reverdy (who is a numerical physicist and the Particle Physics Laboratory in Annecy).
Relevant skills for the position include: type theory, category theory, programming language theory, programming in
proof assistants, implementation of programming languages. It is definitely not necessary to possess all these
skills to be successful.
Please don't hesitate to contact us if you have any question,
Tom Hirschowitz
Pierre Hyvernat
Vincent Reverdy
More information about the Types-announce
mailing list