Funded PhD Studentship: DTC CS 16 - Generative Programming - Integrating Object-Oriented and Dependently Typed Programming

Swansea University is a UK top 30 institution for research excellence (Research Excellence Framework 2014), and has been named Welsh University of the Year 2017 by The Times and Sunday Times Good University Guide.

Swansea Science DTC is a community committed to undertaking world-class research that has a positive impact globally and we have a fully-funded PhD scholarship for 2017/2018 entry.

The Department of Computer Science provides state-of-the-art facilities including fully networked laboratories running Windows and Linux and a project laboratory containing specialised equipment. Laboratories support a wide range of software including programming languages Java, C# and the .NET framework, C, C++, Haskell and Prolog.

There are also integrated programme development environments such as Visual Studio and Netbeans; the widely used Microsoft Office Package; web access tools and many special purpose software tools including graphical rendering and image manipulation tools and more.

In the most recent Research Excellence Framework (REF) in 2014, 80% of the research submitted by the Computer Science Department was judged to be world-leading or internationally excellent. High profile researchers include Professor Harold Thimbleby whose book ‘Press On’ won the American Publishers’ Association best book award in computer science. The department has the 12th highest percentage of world-leading researchers in any computer science department in the UK. The department also has strong links with multinational companies including IBM, Nokia, SanDisk, Philips, Affinity Software and Sourcebits.

Description:

The goal of generative programming is, instead of manually writing existing code again and again with small variations, to automate code generation, and write generic code, which can, by using appropriate parameters, be instantiated to the specific situation needed. Object-oriented Programming and dependently typed programming are two approaches for obtaining highly generative programs, and Anton Setzer has, together with co-authors, combined (https://tinyurl.com/hkhgqzt) the two approaches by integrating object-based programming (a subset of object-oriented programming) into the dependently typed programming language and theorem prover Agda including examples of Graphical User Interfaces. The goal of this project, for which support for exchange visits and Types summer schools and workshops is available through the EU COST ACTION EUTYPES ( https://eutypes.cs.ru.nl/ ), is to extend this approach to full object-oriented programming by adding a heap, allowing dynamic creation of objects on the heap, integrating subtyping (if time permits), and by carrying out more realistic case studies such as developing realistic games in Agda.