Dependent Types for Safe and Secure Web Programming
Simon Fowler, Edwin C. Brady · 2013
Dependently-typed languages allow precise types to be used during development, facilitating static reasoning about program behaviour. However, with the use of more specific types comes the disadvantage that it becomes increasingly difficult to write programs that are accepted by a type checker, meaning additional proofs may have to be specified manually.