In this talk, we will see how to build trace models of programming languages in a systematic way using labelled transition systems designed by operational game semantics. The primary purpose of these models is to characterize contextual equivalence, the maximal observational equational theory, thanks to full-abstraction results. We will consider higher-order programming languages with features that include mutable store (local references), control operators (call/cc), cryptographic operators (dynamic sealing), and rich type systems (algebraic data types, parametric polymorphism). We will see how to apply this framework to prove a fully abstract compilations result from parametric polymorphism to untyped cryptographic lambda-calculus.