Programming Languages Dissertation Series

Tools used in software engineering often balance a tradeoff between generality and specificity. The most important tools in software engineering are programming languages, and the most common ones are General-Purpose Languages (GPLs). Because of their generality, GPLs can be used to develop many kinds of software. Domain-Specific Languages (DSLs) are a more specific counterpart; they are programming languages tailored to a specific domain. DSLs are not generally applicable but can be more effective for developing software within their particular domain.

Information systems store and organize data, and manage business processes concerned with that data. Information systems aim to support operations, management and decision-making in organizations. Web applications are ideal for implementing information systems. Although existing web frameworks provide abstractions for creating web applications, there are three major issues with current web frameworks.

Computers execute software to do the tasks we expect from them. This software is written by human beings, we call this programming. The most common way to program is by writing text in a programming language. A programming language is very structured so we can be precise, but ultimately these languages are still for humans to read and write. In order to execute the written program, we need to translate it to a list of tiny instruction steps that the hardware of the computer can execute. This translation is also automated with software. The most common forms this software takes is (1) interpreters that execute a program live as they read it, or (2) compilers that translate the entire program for later execution.

The PhD thesis is about the design of meta-languages for the specification and implementation of typed programming languages, such that the implementation is formally proven type-correct. For language front-ends—i.e., type checkers—the thesis contributions a method for automatically obtaining sound type checkers from declarative type-system specifications. Language back-ends—i.e., interpreters and compilers—are developed in the dependently typed meta-language Agda in an intrinsically typed style so that the implementation also encompasses a type-safety proof. The contributions of the thesis there is to make it to scale these ideas from simply typed functional languages, to languages with references a la ML or concurrency and session-typed cross-thread communication, and a low-level language with labels and jumps. This is made possible by developing, among other things, an abstract, shallowly embedded separation logic in Agda, as a basis for functional abstractions (e.g., monads) that encapsulate both computational work and proof work.

All computers run software, such as operating systems, web browsers, and video games, which are used by billions of people around the world. Therefore, it is important to develop high-quality software, which is only possible through interactive programming systems that involve programmers in the exchange of correct and responsive feedback. Fortunately, for many general-purpose programming languages, integrated development environments provide interactive programming systems through code editors and editor services.

Programming languages are one of the key components of computer science, allowing programmers to control, define, and change the behaviour of computer systems. However, they require considerable effort to design, implement, maintain, and develop them. Fortunately, declarative approaches can be used to define programming languages facilitating their development and implementation.

Information systems are systems for the collection, organization, storage, and communication of information. Information systems aim to support operations, management and decision-making. In order to do this, these systems filter and process data according to business logic to create new data. Typically these information systems contain large amounts of data and receive frequent updates to this data. Over time requirements for information systems change, from the decision making logic to the number of users interacting with the system. As organizations evolve, so must their information systems. Our reliance on information systems to make decisions and the ever changing requirements poses the following challenges for information system engineering. Validatability: how easy is it for information system developers to establish that a system ‘does the right thing’? Traceability: can the origin of decisions made by the system be verified? Reliability: can we trust the system to consistently make decisions and not lose our data? Performance: can the system keep responding promptly to the load of its users? Availability: can we trust that the system performs its functionality all of the time?And finally, modifiability: how easy is it to change the system specification when requirements change?In this dissertation we show the feasibility and usefulness of declarative programming for information systems in light of these challenges. Our research method is design research. This iterative method repeats four phases: analysis, design, evaluation, and diffusion. We analyze the challenges of information system engineering, design a new programming language to address these, evaluate our new programming language in practice, and diffuse our knowledge through scholarly articles. This resulted in four new declarative languages: the Relations language, IceDust, IceDust2, and PixieDust. Our contributions can be summarized by the new features of these languages. Native multiplicities, bidirectional relations, and concise navigation improve information system validatability and modifiability over object-oriented and relational approaches. Derived attribute values improve traceability. Incremental and eventual computing based on path analysis and calculation strategy switching improve information system modifiability without sacrificing performance and availability over object-oriented and relational approaches. Calculation strategy composition improves validatability, modifiability, and reliability over reactive programming approaches. And finally, Bidirectional derived relations improve information system validatability over relational approaches. The results of this dissertation can be applied in practice. We applied IceDust2 to the learning management information system WebLab. We found that validatability, traceability, reliability, and modifiability were considerably improved while retaining similar performance and availability. Moreover, the fact that IceDust and PixieDust work in different domains, business logic and user interfaces respectively, suggests that our language features could be applied to more domains.

Reference

Reference

Reference