Details of Grant 

EPSRC Reference:	EP/T007265/1
Title:	Programming as Conversation: Type-Driven Development in Action
Principal Investigator:	Brady, Dr EC
Other Investigators:
Researcher Co-Investigators:
Project Partners:	Galois, Inc Potsdam Institute for Climate Impact Res PRECISE Center, University of Pennsylvan University of Kent University of Strathclyde Well Typed LLP
Department:	Computer Science
Organisation:	University of St Andrews
Scheme:	Standard Research
Starts:	01 April 2020	Ends:	31 March 2023	Value (£):	367,276
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	Information Technologies
Related Grants:
Panel History:	Panel Date Panel Name Outcome 10 Jul 2019 EPSRC ICT Prioritisation Panel July 2019 Announced
Summary on Grant Application Form
This project aims to improve the program development process, using a process of "Type-driven Development". We believe that in order to enable the highest levels of productivity, programming should be a conversation between the programmer and the machine. In type-driven development, we begin by giving a type as a plan for a program. Then the machine, rather than being seen as an adversary which rejects incomplete or incorrect programs, is the programmer's assistant. A limited form of this idea exists in modern integrated development environments: when typing "x." into a text buffer, the environment will show with methods "x" implements. This project will take this idea several steps further. Not only can we give feedback on partial programs, we can also use types and their structure to generate significant parts of a program and direct the implementation of more complex components such as communication and security protocols. During development, programs spend most of their time in an incomplete state, and the act of programming is as much about the steps required to achieve a complete program as it is about the end result. Accordingly, language implementations and tools must support the editing process as well as check and compile the end result. In this project, we will develop the necessary tooling to support interactive type-driven development, based on sound theoretical foundations. Furthermore, we will make the tooling itself programmable: the foundations will essentially give a language of programming "tactics", which will be composable intro sophisticated methods for automatic program construction, directed by the type. We will liaise with industry throughout to ensure that the techniques we develop are well-suited to commercially relevant problems.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.st-and.ac.uk