Resolving Quartz Overloading
Quartz is a new declarative hardware description language with polymorphism, overloading, higher-order combinators and a relational approach to data flow, supporting formal reasoning for design verification in the same style as the Ruby language. The combination of parametric polymorphism and overloading within the language involves the implementation of a system of constrained types. This paper describes how Quartz overloading is resolved using satisfiability matrix predicates. Our algorithm is a new approach to overloading designed specifically for the requirements of describing hardware in Quartz.
KeywordsType Class Type Check Matrix Predicate Composite Block Open World Assumption
- 1.Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Proc. POPL 1989, pp. 60–76. ACM Press, New York (1989)Google Scholar
- 4.Jones, G., Sheeran, M.: Circuit design in Ruby. In: Staunstrup, J. (ed.) Formal Methods for VLSI Design, pp. 13–70. North-Holland/Elsevier (1990)Google Scholar