#set text(size: 13pt)
#set par(first-line-indent: 1em, justify: true)
#show link : body => text(blue, body)

Dear Dr. <NAME>,

I am <NAME>, an incoming second-year Master's student at
#link("https://wikimpri.dptinfo.ens-cachan.fr/doku.php")[MPRI] (Parisian Masters
of Research in Computer Science), in France. I am writing to express my
enthusiastic interest in attending the "Proof and Computation" Autumn School
2024 at Aurachhof. My research interests lie in Type Theory, Proof Assistants,
and Logic, particularly in the metatheory of proof assistants. The courses
offered by this autumn school align perfectly with my research focus on proofs
and computation, thus it would be a great honor to join the school in
Fischbachau this September.

Since May 2024, I have been undertaking my Master's Year 1 internship with
<NAME> at the Cambium team in INRIA Paris, working on the project
"Towards Formalizing the Guard Condition of Coq." This project aims to produce a
specification of the guard checker of the Coq proof assistant, which enforces a
sufficient condition for termination on fixpoints. A sound guard condition will
ensure the termination of fixpoint reduction and facilitate strong normalization
proofs, ultimately proving the consistency of the type theory behind the Coq
proof assistant. I was pleased to have presented my work at the
#link("https://www.irif.fr/reciprog/workshop-guarded-june24")[Workshop on the
Guard Condition of Coq], held on 3 June by the
#link("https://www.irif.fr/reciprog/index")[RECIPROG project] in Nantes, France,
where it was well received.

In 2022, I worked on the formalization of the Modules system of Coq in MetaCoq
during my undergraduate internship under the guidance of Nicolas Tabareau.
Alongside Martin Henz and <NAME>, I co-authored my
#link("https://github.com/SwampertX/undergraduate-thesis")[bachelor's thesis] on
this topic, which received an A grade from the National University of Singapore,
where I completed a dual bachelor's degree in Mathematics and Computer Science.

During the first two semesters of my Master's Year 1 (M1) in 2023-24, I studied
the formalization of type theory in type theory via Category with Families under
the supervision of Ambrus Kaposi. This project culminated in a small
formalization of (a less-dependent version of) Category with Families in Agda.
Among the courses I studied in M1,
#link("http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/")[INF551
Computational Logic], taught by <NAME>, was the most relevant to my
research interests. I was awarded full marks (20/20) in this course, where I
implemented, for the final project, a dependent type-checker / proof-assistant
supporting Dependent Function, Equality, and Natural Number types.

As an international student studying in Paris, I am seeking funding to attend
the autumn school, which I am eager to join but cannot afford without financial
assistance. I believe this is an excellent opportunity to further my research
and connect with like-minded researchers and peers, as I enter my final year in
my master's programme.

Thank you very much for considering my application, and I look forward to your
favorable response.

#v(1fr)
#set par(first-line-indent: 0pt, justify: true)
Warmest regards,\
<NAME>