Any views expressed within media held on this service are those of the contributors, should not be taken as approved or endorsed by the University, and do not necessarily reflect the views of the University in respect of any particular issue.


Bob Atkey, University of Strathclyde will give a talk, in person and online, for the Coffee House Tech Talk Series. Details of the talk are below.

Speaker: Bob Atkey, University of Strathclyde

Title: Data Types with Negation

When: 11am Tue 9 Jan

Where: 4th floor Bayes Centre

External link:

Passcode: 381535


Inductive data types are a foundational tool for representing data and knowledge in dependently typed programming languages. The user defines an inductive data type by declaring constructors for constructing positive evidence. For example, evidence of a path through some graph, or the parse tree as evidence that a context-free grammar accepts some input. But in some cases, positive evidence is not enough. What if we want evidence that no path exists? or we want to represent parse trees of backtracking parsers, where alternatives are only tried in the case when another parse didn’t work? In this talk, I will explain how the use of negative evidence arises in many places in programming languages, describe a way of extending inductive data types with negation, and how we can understand them as an interaction of inductive and coinductive types.


Bob Atkey is a Senior Lecturer at the University of Strathclyde. Previously he worked in industry on static analysis tools and as a researcher at Strathclyde and Edinburgh. He did a PhD at the University of Edinburgh, graduating in 2006. His research is broadly on programming languages, through a type theoretic and semantic lens.


Report this page

To report inappropriate content on this page, please use the form below. Upon receiving your report, we will be in touch as per the Take Down Policy of the service.

Please note that personal data collected through this form is used and stored for the purposes of processing this report and communication with you.

If you are unable to report a concern about content via this form please contact the Service Owner.

Please enter an email address you wish to be contacted on. Please describe the unacceptable content in sufficient detail to allow us to locate it, and why you consider it to be unacceptable.
By submitting this report, you accept that it is accurate and that fraudulent or nuisance complaints may result in action by the University.