Describing Inter Parameter Constraints in Web APIs Using Dependent Types
Date: Tue, May 17, 2022
Room: Lecture Hall H (building 36)
Note: This is a MSc thesis defense
Web APIs are being used for increasingly larger and complex use cases. Right now it can be hard to make sure that what is documented about an API is correct everywhere and to know if a change will have impact on the users of a web API. When details are missing in an API specification users of that API need to make assumptions about how the API works. The creators of the web API also wants to know what users expect from the API. There are two sides to this problem, enforcing that the implementation is actually the same as what is specified, and making it possible to define API specifications as precise as possible.
The type system of a programming language is a useful tool for enforcing the struc- ture of an implementation. In this thesis we use a dependent type system to enforce an
API specification in the implementation. By using the dependent type system we can de- fine additional, more specific, constraints on the API. These constraints are more specific
than constraints expressible in possible research. With this approach we can be sure that the specification and implementation are actually describing the same API. And with the added flexibility we can create a more complete description of web APIs.