TIME:
10-18-2022 16:30
SPEAKER:
Marcelo Fiore
Professor in Mathematical Foundations of Computer Science
Fellow of Christ’s College
University of Cambridge, UK
Personal page https://www.cst.cam.ac.uk/people/mpf23
ABSTRACT:
I will outline a mathematical theory for modelling, reasoning about, and computing with tree-like structures. Main application areas are to abstract syntax (the deep syntactic structure of formal languages) and to inductive data types (inductively defined data structures). The lecture format will be introductory and intended to be interactive, developing theory as motivated by applications.
The mathematical theory is semantic, funded upon a model theory. This is centered around a general notion of polynomial construction that specifies treelike structure and, crucially, will be shown to provide algebraic models together with compositional interpretations that support inductive reasoning principles and computation by structural recursion.
Theory and applications will be presented and studied at incrementally higher levels of generality. From the viewpoint of abstract syntax, these will range from uni-sorted languages with algebraic operators to multi-sorted languages with
variable-binding operators; while, from the viewpoint of inductive data types, they will encompass, ADTs (Algebraic Data Types), GADTs (Generalized Algebraic Data Types), and IFs (Inductive Families). An important feature of the mathematical theory is that it is directly programmable in dependently-typed computational languages supporting inductive data types; this aspect will also be considered.