P. Martin-löf and «. , Choice Sequence in Type Theory », Handwritten notes by P. Mäenpää and A. Ranta on a lecture series given by P. Martin-Löf at Stockholm University, 1990.

P. Martin-löf, «. Nonstandard-type, and . Theory, Handwritten notes of a talk given at the Workshop Proof and Computation at Munich in, 1999.

E. Nelson, Internal set theory: A new approach to nonstandard analysis, Bulletin of the American Mathematical Society, vol.83, issue.6, pp.1165-1198, 1977.
DOI : 10.1090/S0002-9904-1977-14398-X

B. Nordström, K. Petersson, J. M. Smith, and . Programming, Out of print, available from www.cs.chalmers.se.Cs, 1990.

E. Palmgren, A constructive approach to nonstandard analysis, Annals of Pure and Applied Logic, pp.297-325, 1995.
DOI : 10.1016/0168-0072(94)00030-7