Refinement Types for TLA+ - Archive ouverte HAL Access content directly
Conference Papers Year : 2014

Refinement Types for TLA+

(1) , (1, 2)


TLA+ is a specification language, mainly intended for concurrent and distributed systems. Its non-temporal fragment is based on a variant of (untyped) ZF set theory. Motivated by the integration of the TLA+ Proof System with SMT solvers or similar tools based on multi-sorted first-order logic, we define a type system for TLA+ and we prove its soundness. The system includes refinement types, which fit naturally in set theory. Combined with dependent function types, we obtain type annotations on top of an untyped specification language, getting the best of both the typed and untyped approaches. After implementing the type inference algorithm, we show that the resulting typing discipline improves the verification capabilities of the proof system.
Not file

Dates and versions

hal-01063516 , version 1 (12-09-2014)



Stephan Merz, Hernán Vanzetto. Refinement Types for TLA+. NASA Formal Methods - 6th International Symposium, 2014, Houston, Texas, United States. pp.143-157, ⟨10.1007/978-3-319-06200-6_11⟩. ⟨hal-01063516⟩
203 View
0 Download



Gmail Facebook Twitter LinkedIn More