Verified Subtyping with Traits and Mixins

Asankhaya Sharma

Traits allow decomposing programs into smaller parts and mixins are a form of composition that resemble multiple inheritance. Unfortunately, in the presence of traits, programming languages like Scala give up on subtyping relation between objects. In this paper, we present a method to check subtyping between objects based on entailment in separation logic. We implement our method as a domain specific language in Scala and apply it on the Scala standard library. We have verified that 67% of mixins used in the Scala standard library do indeed conform to subtyping between the traits that are used to build them.

In Shang-Wei Lin and Laure Petrucci: Proceedings 2nd French Singaporean Workshop on Formal Methods and Applications (FSFMA 2014), Singapore, 13th May 2014, Electronic Proceedings in Theoretical Computer Science 156, pp. 45–51.
Published: 8th July 2014.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: