The Coq mailing list

[Tom Hirschowitz <tom.hirschowitz AT univ-smb.fr>]

Hi all,

The LAMA

https://lama.univ-smb.fr

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://univ-smb.nous-recrutons.fr/poste/nzyn17a55c-chercheur-post-doctorant-fh-usmb-shine-guli-anr-22-exes-0017/

and there

https://www.univ-smb.fr/wp-content/uploads/2024/11/offre-emploi-post-doc-2024-100__lama_guli_vf.pdf

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