Typing under Incomplete Information
Lead Research Organisation:
UNIVERSITY COLLEGE LONDON
Department Name: Computer Science
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
People |
ORCID iD |
| David Clark (Primary Supervisor) | |
| David Kelly (Student) |
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/N509577/1 | 30/09/2016 | 24/03/2022 | |||
| 1928445 | Studentship | EP/N509577/1 | 30/09/2017 | 25/01/2022 | David Kelly |
| Description | Our novel contributions are: the first optional security type system for the polymorphic lambda calculus (System F). We are the first to use information theory to suggest placements for type annotations. We make a novel use of information flow ranking (RIF) to reduce the cost of exact QIF calculation. SafeStrings is the first approach to use grammars as a means of generating an in-language, type-based, subsumption relation for strings. We also show that this approach is realistic by performing a large-scale study of how strings are used in programming languages. |
| Exploitation Route | The outcomes so far are in the theoretical end of research. We have shown proof of concept implementation of both optional security typing and SafeStrings, but both need to be scaled up, and have more robust engineering, before being taken into industry. Strong groundwork has been laid, leaving the main challenge to deployability in the realms of dedicated engineering. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| Description | SafeStrings |
| Organisation | Microsoft Research |
| Country | Global |
| Sector | Private |
| PI Contribution | Typing for strings is difficult because a string is a "black box" to a type checker, even though most strings used in computer programs are highly structured. Our solution to this problem uses embedded grammars to expose this latent structure to the type checker. We have developed an expressive approach to string type checking, SafeStrings, that uses only the native mechanisms of a target programming language to bring increased type safety, and testing efficiency, to string-controlled programs. We used search-based methods to assist the developer in knowing where to annotate, maximising the impact of the annotation on the overall correctness of a program. |
| Collaborator Contribution | The partner (Mark Marron) brought editing and structural advice to the initial research paper. This is a problem which MicroSoft Research are actively engaged in. |
| Impact | We have two research papers written under this collaboration. Both papers are presently under review and have not yet been published. |
| Start Year | 2018 |