Vitek, JanJagannathan, SureshWelc, AdamHosking, Antony L.2026-01-012026-01-013-540-21313-90302-9743ORCID:/0000-0002-4487-6923/work/167651639https://hdl.handle.net/1885/733801572A transaction defines a locus of computation that satisfies important concurrency and failure properties; these so-called ACID properties provide strong serialization guarantees that allow us to reason about concurrent and distributed programs in terms of higher-level units of computation (e.g., transactions) rather than lower-level data structures (e.g., mutual-exclusion locks). This paper presents a framework for specifying the semantics of a transactional facility integrated within a host programming language. The TFJ calculus supports nested and multi-threaded transactions. We give a semantics to TFJ that is parameterized by the definition of the transactional mechanism that permits the study of different transaction models.en200410.1007/978-3-540-24725-8_1835048845164