Dominic Orchard

Lecturer / Stage 2 Year Director (UKC)

workTel: +44 (0)1227 82 3784
faxFax: +44 (0)1227 762811
Email: D.A.Orchard@kent.ac.uk

Room SW06
School of Computing
University of Kent, School of Computing, University of Kent Canterbury Kent CT2 7NF England

Publications

My publications are available from the University of Kent's Academic Repository.

Selected publications

Quantitative program reasoning with graded modal types - ICFP (2019)
Composing bidirectional programs monadically - ESOP (2019)
Complexity bounds for container functors and comonads - Information & Computation (2018)
Verifying Spatial Properties of Array Computations - OOPSLA (2017)
Session Types with Linearity in Haskell - Book chapter in Behaviour types: from Theory to Tools (2017)
Combining Effects and Coeffects via Grading - ICFP (2016)
Effects as Sessions, Sessions as Effects - POPL (2016)
Coeffects: A calculus of context-dependent computation - ICFP (2014)
A Computational Science Agenda for Programming Language Research - ICCS (2014)

A more complete (but temporary) list of my publications can be found here.
I also keep a list of my external talks, mostly with links to slides and sometimes YouTube videos.

Research Interests

I belong to the following research groups:

Programming Languages and Systems Group

I am also a Fellow of the Software Sustainability Institute.

I am on the following Programme Committees this year: PLACES 2019, LOLA 2019, PPDP 2019, POPL 2019, IFL 2018, TyDe 2018, BEAT 2019, ICE 2018. I am co-chairing PLACES 2019.

Main projects

Granule - Advanced type systems for verification of data treated as a resoruce.
CamFort - Lightweight verification of scientific computing models

Broadly I am interested in the intersection between logic, semantics, and types.

I have co-authored several papers introducing and developing the notion of coeffectful program behaviour (ICFP 2016, ICFP 2014, ICALP 2013). Coeffects are program behaviours which "consume" the execution context, e.g., variables, hardware resources, access policies, library versions, implicit parameters. Coeffect analyses and type theories capture a program's requirements on the execution environment. For example, a type theory corresponding to Bounded Linear Logic is a coeffect system which allows fine-grained control over variable usage.

I am also interested in applying results from programming language research to computational science, in particular for program verification. I am Co-Investigator on the project CamFort: Automated evolution and verification of computational science models joint with the University of Cambridge

Find me on: Twitter and GitHub and My blog

Teaching

I am currently teaching on the following courses:

CO519 - Theory of Computing
CO661 - Theory and Practice of Concurrency
CO545 - Functional and Concurrent Programming
CO583 - Introduction to Programming and Web Technologies

I also supervise projects for CO600, so please get in touch if you would like to discuss an idea. Details of my past teaching can be found here.

Organisation

A list of things I have organsied.

Short bio

Dominic has an undergraduate degree in Computer Science from the University of Warwick and a PhD in Computer Science from the University of Cambridge. He worked as a Research Associate at Imperial College London and Cambridge before joining the University of Kent.

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 09/11/2019

For current students & staff

Search

School of Computing