【BAYES COFFEE HOUSE TECH TALK SERIES】Data Types with Negation
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
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.