Hi all,
The LAMA
offers a full-time, 18 month postdoc position starting September 2025. The deadline is really soon: July 3!
The details are here
and there
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. Typically, physicists sometimes need to use libraries written with different unit systems, in a compatible way. 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: proof assistants, type theory, category theory, programming language theory, 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