Type-based reasoning is popular in functional programming. In particular, parametric polymorphism constrains functions in such a way that statements about their behavior can be de...
Jan Christiansen, Daniel Seidel, Janis Voigtlä...
This paper presents a resource typing framework for the Guru d-programming language, in which abstractions for various kinds of program resources can be defined. Implemented exam...
Some programs are doubly-generic. For example, map is datatypegeneric in that many different data structures support a mapping operation. A generic programming language like Gener...
Reasoning about object-oriented programs is difficult since such programs usually involve aliasing, and it is not easy to identify the ways objects can relate to each other and t...
Real-time systems, and in particular safety-critical systems, are a rich source of challenges for the program verification community as software errors can have catastrophic conse...