The following is an addendum to Sam Sanders’ answer, too long for a comment: It’s a short bibliography of constructive NSA and related theories of nonstandardness, taken from Erik Palmgren’s now-defunct webpage at Uppsala University (https://www2.math.uu.se/∼palmgren/biblio/nonstd.html), last modified Dec 2010 according to the file timestamp. Erik’s later webpage at Stockholm University remains extant here.

## Constructive nonstandard mathematics

Chuaqui, R., Suppes, P.: Free-variable axiomatic foundations of
infinitesimal analysis: A fragment with finitary consistency proof.
J. Symbolic Logic 60(1995), 122 - 159.

Chwistek, L.: The Limits of Science, Kegan Paul, London 1948.

Dragalin, A.G.: An explicit boolean-valued model for
the non-standard arithmetic, Publ. Math. Debrecen 42(1993), 369 - 389.

Laugwitz, D. : Omega-calculus as a generalisation of field extension
- an alternative approach to nonstandard analysis, in: A.E. Hurd
(ed.) Non-standard Analysis - Recent Developments, Lecture Notes
in Mathematics, Vol. 983, Springer, Berlin 1983.

Liu, S.-C.: A proof-theoretic approach to nonstandard analysis with
emphasis on distinguishing between constructive and non-constructive
results, in: H.J. Keisler and K. Kunen (eds.), The Kleene
Symposium, North-Holland, Amsterdam 1980, 391 - 414.

Martin-Löf, P.: Mathematics of Infinity,
in: P. Martin-Löf and G.E. Mints (eds.) COLOG-88 Computer
Logic,
Lecture Notes in Computer Science, vol. 417, Springer, Berlin
1989.

Moerdijk, I.: A model for intuitionistic
non-standard arithmetic, Ann. Pure Appl. Logic 73(1995), 37 --51.

Moerdijk, I., Palmgren, E.: Minimal models
of Heyting arithmetic, Uppsala University, Department of
Mathematics Report 1995:25 (accepted for publication in J.
Symbolic Logic).

Mycielski, J.: Analysis without actual infinity, Journal of Symbolic
Logic 46(1981), 625-633.

Palmgren, E.: A note on 'Mathematics of Infinity', Journal of
Symbolic Logic 58(1993), 1195 -- 1200.

Palmgren, E.: A constructive approach to nonstandard analysis,
Ann. Pure Appl. Logic 73(1995), 297 -- 325.

Palmgren, E.: Constructive nonstandard analysis, Cahiers du
Centre de Logique, vol. 9, Academia, Louvain, 1996.

Palmgren, E.: A sheaf-theoretic foundation for nonstandard analysis,
Uppsala University, Department of Mathematics Report 1995:43
(to appear in Ann. Pure Appl. Logic).

Palmgren, E.: Sheaf-theoretic nonstandard analysis: constructive
aspects. Uppsala University, Department of Mathematics Report 1996:28.

Schmieden, C., Laugwitz, D.: Eine Erweiterung der
Infinitesimalrechnung, Math. Zeitschrift 69(1958), 1-39.

Vesley, R.: An intuitionistic infinitesimal calculus, in: F. Richman
(ed.) Constructive Mathematics, Lecture Notes in Mathematics, Vol.
873, Springer, 1983.

Wattenberg, F.: Nonstandard analysis and constructivism?
Studia Logica 47(1988), 303 -- 309.