Types and Effects for Resource Usage Analysis

摘要: An extension of the λ-calculus is proposed, to study resource usage analysis and verification. Resources can be dynamically created, passed / returned by functions; their usages have side effects, represented events. Usage policies are properties over histories events, a possibly nested, local scope. A type effect system over-approximates set program generate at run-time. crucial point solved here concerns correctly associating fresh resources with within approximations. second issue that these approximations may contain an unbounded number resources. Despite that, we devised technique model-check validity valid approximation resource-safe: no run-time monitor needed safely drive its executions.