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