Context-aware programming languages
Context-aware programming languages
复制标题
上下文感知编程语言
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
T. Petříček
中科院分区：
文献类型：
--
作者：
T. Petříček
编程语言的发展需要反映程序执行方式的重要变化。近年来，这包括开发并行编程模型(以应对多核革命)或改进数据访问技术。这篇论文是对另一场这样的革命的回应--运行程序的设备和系统的多样化。本文的关键点是认识到执行环境或上下文是编写现代应用程序的基础，编程语言应该为使用上下文进行编程和验证如何访问它提供抽象。我们确定了许多以前没有联系的程序属性，但建立了一些上下文概念的模型。我们的例子包括跟踪跨平台开发中的不同执行平台(及其版本)、不同执行环境中可用的资源(例如，手机上的GPS传感器和服务器上的数据库)，但也包括更传统的概念，例如基于流的数据流编程中的变量使用(例如，在活动分析和线性逻辑中)或过去的值。我们的第一个贡献是发现了上述例子与它们以微积分(协同效应系统)的形式呈现的新颖形式之间的联系。所提出的类型系统和形式语义学强调了不同语境概念之间的关系。我们的第二个贡献是定义了两个统一的协效演算，它们捕获了示例的共同结构。特别是，我们的平面协同效应演算使用执行环境的上下文属性对语言进行建模，而我们的结构协同效应演算对上下文属性附加到变量使用的语言进行建模。我们根据索引式联结的范畴理论结构(基于著名的单元式结构的对偶化)来定义演算的语义，并用它来定义操作语义并证明演算的类型安全性。我们的第三个贡献是以基于网络的互动文章的形式对我们的工作进行了新颖的介绍。这提供了三种上下文感知编程语言的简单实现，并允许读者编写和运行简单的上下文感知程序，但还可以探索实现背后的理论，包括类型派生和语义。
The development of programming languages needs to reflect important changes in the way programs execute. In recent years, this has included the development of parallel programming models (in reaction to the multicore revolution) or improvements in data access technologies. This thesis is a response to another such revolution – the diversification of devices and systems where programs run. The key point made by this thesis is the realization that an execution environment or a context is fundamental for writing modern applications and that programming languages should provide abstractions for programming with context and verifying how it is accessed. We identify a number of program properties that were not connected before, but model some notion of context. Our examples include tracking different execution platforms (and their versions) in cross-platform development, resources available in different execution environments (e. g. GPS sensor on a phone and database on the server), but also more traditional notions such as variable usage (e. g. in liveness analysis and linear logics) or past values in stream-based dataflow programming. Our first contribution is the discovery of the connection between the above examples and their novel presentation in the form of calculi (coeffect systems). The presented type systems and formal semantics highlight the relationship between different notions of context. Our second contribution is the definition of two unified coeffect calculi that capture the common structure of the examples. In particular, our flat coeffect calculus models languages with contextual properties of the execution environment and our structural coeffect calculus models languages where the contextual properties are attached to the variable usage. We define the semantics of the calculi in terms of category theoretical structure of an indexed comonad (based on dualisation of the well-known monad structure), use it to define operational semantics and prove type safety of the calculi. Our third contribution is a novel presentation of our work in the form of web-based interactive essay. This provides a simple implementation of three context-aware programming languages and lets the reader write and run simple context-aware programs, but also explore the theory behind the implementation including the typing derivation and semantics.