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: 4^th floor Bayes Centre

External link: https://meeting.huaweicloud.com/welink/j/95973609/D5HiJPcxftyMkkIHpVKDdMmWEHQrujaq5

Passcode: 381535

Abstract

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.

Bio

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.

【BAYES COFFEE HOUSE TECH TALK SERIES】Data Types with Negation / Huawei-Edinburgh Joint Lab by blogadmin is licensed under a Creative Commons Attribution CC BY 3.0