多层Web语言中类型与效应推断的抽象语义
计算机科学中的逻辑
2011-08-12 v1 编程语言
摘要
类型与效应是类型系统，允许表达一般的语义属性并静态推理程序的执行。它们已被广泛用于规约静态分析，例如跟踪并发程序中的计算副作用、异常和通信。在本文中，我们采用抽象解释技术来重构（遵循Cousot的方法论）一个为处理多层Web语言安全问题而开发的类型与效应系统。我们的重构使我们能够表明，该类型与效应系统相对于语言的语义是不健全的。此外，我们纠正了分析中的健全性问题，并系统地构建了一个正确的分析器。
引用
@article{arxiv.1108.2359,
title = {An Abstract Semantics for Inference of Types and Effects in a Multi-Tier Web Language},
author = {Letterio Galletta and Giorgio Levi},
journal= {arXiv preprint arXiv:1108.2359},
year = {2011}
}
备注
In Proceedings WWV 2011, arXiv:1108.2085