[09/01/23] Partner Event - Data Types with Negation About the event 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. Speaker 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. Jan 09 2024 11.00 - 12.00 [09/01/23] Partner Event - Data Types with Negation Join Huawei and Bob Atkey for this tech talk, taking place on 9th of January. 4th floor Bayes Centre, Coffee House or online Register
[09/01/23] Partner Event - Data Types with Negation About the event 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. Speaker 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. Jan 09 2024 11.00 - 12.00 [09/01/23] Partner Event - Data Types with Negation Join Huawei and Bob Atkey for this tech talk, taking place on 9th of January. 4th floor Bayes Centre, Coffee House or online Register
Jan 09 2024 11.00 - 12.00 [09/01/23] Partner Event - Data Types with Negation Join Huawei and Bob Atkey for this tech talk, taking place on 9th of January.
