Missing pieces

[stevana]

Here are a couple of things that, as far as I know, haven't been digitalised yet.

• Hank has a paper copy of the inconsistent 1971 version. If there's enough interest, I'm sure he can be persuaded into scanning it.
• The mathematics library at Chalmers should still have two copies of the book "Notes on constructive mathematics". (Hank said he lost his copy and that he misses it, so maybe we could trade it for the 71 article?)

Anything else out there?

[stevana]

Re-typeset/searchable version of Constructive mathematics and computer programming: http://www.cs.tufts.edu/~nr/cs257/archive/per-martin-lof/constructive-math.pdf

[stevana]

More on 1971: https://www.reddit.com/r/dependent_types/comments/3s7ws5/looking_for_a_theory_of_types/

[mietek]

It appears that we are unlikely to get the 1971 version:

I talked to Martin-Löf today. Unfortunately he does not want "A theory of types" to be published or digitally available.

[mietek]

The 1971 version is being reformulated by @pigworker: https://github.com/pigworker/Bi71

[gallais]

Caveat:

\section{The 1971 Rules} Let us first see the system which we are about to reorganise. \textbf{Really? Actually, I'm just guessing.}

Maybe someone with access to a physical copy can comment on whether it is indeed the 1971 system.