[TYPES] Request: Papers to understand Nordic logic talk

[Julin S]

Hi. I saw in the types-announce[2] mailing list about a talk by Thierry
Coquand
as part of the Nordic Online Logic Seminar.

I'm sort of new to logic and type theory and was trying to find papers that
would help me understand the talk better.

The abstract was:


> The first part will be about representation of mathematics on a
> computer.Questions that arise there are  naturally reminiscent of issues
that
> arise when teaching formal proofs in a basic logic course, e.g. how to
deal
> with free  and bound variables, and instantiation rules. As discussed in
a 1962
> paper of Tarski, these issues are "clearly experienced both in teaching an
> elementary course in mathematical logic and in formalizing the syntax of
> predicate logic for some theoretical purposes." I will present two quite
> different approaches to this problem: one inspired by Tarski's paper (N.
> Megill, system Metamath) and one using dependent type theory (N.G. de
Bruijn).
>
> The second part will then try to explain how notations introduced by
dependent
> type theory suggest new insights for old questions coming from Principia
> Mathematica (extensionality, reducibility axiom) through the notion of
> universe, introduced by Grothendieck for representing category theory in
set
> theory, and introduced in dependent type theory by P. Martin-Löf.


Could anyone help me find the papers/works that this abstract may be
referring
to (and anything else that can be helpful to better understand the talk)?

I tried searching for these on google scholar but couldn't pinpoint the
papers.

 - 1962 paper by Tarksi
 - Tarski's paper (N. Megill, system Metamath)
 - dependent type theory (N. G. de Bruijn)

Could metamath be this[1]?

[1]: https://urldefense.com/v3/__http://us.metamath.org/downloads/metamath.pdf__;!!IBzWLUs!GgCWS35KVAXOBGITv9G363gRbkyb18vD4--hSnWLV-gywkE2s4FtPjLKBnsWe-MrlCqCOSshYmI$ 
[2]: http://lists.seas.upenn.edu/pipermail/types-announce/2022/010050.html

Thanks and regards,
Julin Shaji