Interactive user experiences on the web are becoming the norm. Client-side programs are becoming more complicated and have to deal with event handling, reading HTML document state and updating the interface. In this paper we propose a declarative language that supports these three facets of client-side browser development declaratively and provides a programming model where complex interfaces can be written using simple programming techniques such as records, functions and recursion.
The polymorphic RPC calculus allows programmers to write succinct multitier programs using polymorphic location constructs. However, until now it lacked an implementation. We develop an experimental programming language based on the polymorphic RPC calculus. We introduce a polymorphic Client-Server (CS) calculus with the client and server parts separated. In contrast to existing untyped CS calculi, our calculus is not only able to resolve polymorphic locations statically, but it is also able to do so dynamically. We design a type-based slicing compilation of the polymorphic RPC calculus into this CS calculus, proving type and semantic correctness. We propose a method to erase types unnecessary for execution but retaining locations at runtime by translating the polymorphic CS calculus into an untyped CS calculus, proving semantic correctness.
The RPC calculus is a simple semantic foundation for multi-tier programming languages such as Links in which located functions can be written for the client-server model. Subsequently, the typed RPC calculus is designed to capture the location information of functions by types and to drive location type-directed slicing compilations. However, the use of locations is currently limited to monomorphic ones, which is one of the gaps to overcome to put into practice the theory of RPC calculi for client-server model. This paper proposes a polymorphic RPC calculus to allow programmers to write succinct multi-tier programs using polymorphic location constructs. Then the polymorphic multi-tier programs can be automatically translated into programs only containing location constants amenable to the existing slicing compilation methods. We formulate a type system for the polymorphic RPC calculus, and prove its type soundness. Also, we design a monomorphization translation together with proofs on its type and semantic correctness for the translation.
With multi-tier programming languages, programmers can specify the locations of code to run in order to reduce development efforts for the web-based client-server model where programmers write client and server programs separately and test the multiple programs together. The RPC calculus, one of the foundations of those languages by Cooper and Wadler, has the feature of symmetric communication in programmer's writing arbitrarily deep nested client-server interactions. However, the existing research only considers dynamically typed locations. We propose a typed RPC calculus where locations are tracked in type-level. A new located type system paves the way for a theory of RPC calculi for the client-server model.
(In the following papers published in SCP2020 and PPDP2021, the typed RPC calculus will be enhanced with polymorphic locations and a type-based slicing compilation.)
A visual block programming language allows users to make their own programs by dragging and dropping graphic blocks rather than by writing the program. This enables users who are not proficient in programming to create programs easily. Although existing studies have applied this idea to programming Internet of things (IoT) applications, existing visual language tools have certain limitations in terms of expressiveness, extensibility, and error prevention. In this paper, we propose a visual block language called Smart Block for SmartThings home automation, together with a visual programming environment that supports the three properties. We designed the visual block language based on the Internet of things automation (IoTa) calculus, a core calculus for IoT automation that generalizes event-condition-action (ECA) rules. Each ECA rule specifies that when an event occurs, and if a condition is met, a certain action is performed. Smart Block supports writing IoT applications in the ECA style and is implemented with Google Blockly, a client-side JavaScript library for creating visual block languages. Smart Block can help users develop reliable SmartApps by checking for redundancy, inconsistency, and circularity in the ECA rules before generating the code. We demonstrate that Smart Block can build 54 out of 56 (96.4%) of the SmartApps provided by the official SmartThings IDE. Furthermore, a user study with 33 participants shows that our approach, based on the foundation of the IoTa calculus, is understandable for users.
Recent researches have reported that Android programs are vulnerable to unexpected exceptions. One reason is that the current design of Android platform solely depends on Java exception mechanism, which is unaware of the component-based structure of Android programs. This paper proposes a component-level exception mechanism for programmers to build robust Android programs with. With the mechanism, they can define an intra-component handler for each component to recover from exceptions, and they can propagate uncaught exceptions to caller component along the reverse of component activation flow. Theoretically, we have formalized an Android semantics with exceptions to prove the robustness property of the mechanism. In practice, we have implemented the mechanism with a domain-specific library that extends existing Android components. This lightweight approach does not demand the change of the Android platform. In our experiment with Android benchmark programs, the library is found to catch a number of runtime exceptions that would otherwise get the programs terminated abnormally. We also measure the overhead of using the library to show that it is very small. Our proposal is a new mechanism for defending Android programs from unexpected exceptions.