Combinatorial sketching for finite programs
Armando Solar-Lezama, Liviu Tancau, et al.
ASPLOS 2006
X10 is a modern object-oriented language designed for productivity and performance in concurrent and distributed systems. In this setting, dependent types offer significant opportunities for detecting design errors statically, documenting design decisions, eliminating costly run-time checks (e.g., for array bounds, null values), and improving the quality of generated code. We present the design and implementation of constrained types, a natural, simple, clean, and expressive extension to object-oriented programming: A type C{c} names a class or interface C and a constraint c on the immutable state of C and in-scope final variables. Constraints may also be associated with class definitions (representing class invariants) and with method and constructor definitions (representing preconditions). Dynamic casting is permitted. The system is parametric on the underlying constraint system: the compiler supports a simple equality-based constraint system but, in addition, supports extension with new constraint systems using compiler plugins. Copyright © 2008 ACM.
Armando Solar-Lezama, Liviu Tancau, et al.
ASPLOS 2006
Jianpeng Cheng, Siva Reddy, et al.
ACL 2017
Aharon Abadi, Ran Ettinger, et al.
OOPSLA 2008
Olivier Tardieu, Benjamin Herta, et al.
PPoPP 2014