Some aspects of Euler's work were formalized in terms of modern infinitesimal theories by Laugwitz, McKinzie, Tuckey, and others. Referring to the latter, G. Ferraro claims that "one can see in operation in their writings a conception of mathematics which is quite extraneous to that of Euler." Ferraro concludes that "the attempt to specify Euler's notions by applying modern concepts is only possible if elements are used which are essentially alien to them, and thus Eulerian mathematics is transformed into something wholly different"; see http://dx.doi.org/10.1016/S0315-0860(03)00030-2.
Meanwhile, P. Reeder writes: "I aim to reformulate a pair of proofs from [Euler's] "Introductio" using concepts and techniques from Abraham Robinson's celebrated non-standard analysis (NSA). I will specifically examine Euler's proof of the Euler formula and his proof of the divergence of the harmonic series. Both of these results have been proved in subsequent centuries using epsilontic (standard epsilon-delta) arguments. The epsilontic arguments differ significantly from Euler's original proofs." Reeder concludes that "NSA possesses the tools to provide appropriate proxies of the inferential moves found in the Introductio"; see http://philosophy.nd.edu/assets/81379/mwpmw_13.summaries.pdf (page 6).
Historians and philosophers thus appear to disagree sharply as to the relevance of modern theories to Euler's mathematics. Can one meaningfully reformulate Euler's infinitesimal mathematics in terms of modern theories?
Note 1. There is a related thread at Would Euler's proofs get published in a modern math Journal, especially considering his treatment of the Infinite?
Note 2. We challenged a reductionist view of Euler's infinitesimal mathematics in a recent article in The Mathematical Intelligencer. Here we refute H. Edwards' reduction of Euler to an Archimedean framework.
Best Answer
[Converted from comment to answer per Yemon Choi's suggestion.]
From a casual run-through of the Ferraro paper, it seems like Euler's ideas about infinitesimals were, unsurprisingly, not formalized to modern standards and therefore don't map exactly onto modern concepts. He apparently didn't think of a line segment as a point set, which would be more similar to smooth infinitesimal analysis than to NSA. But other aspects of Ferraro's description do seem more like NSA than SIA. Infinite numbers are imagined as infinitely increasing sequences, whereas not all models of SIA have invertible infinitesimals. I assume Euler used Aristotelian logic.