By João Barbosa
On 28 April at 4 pm, in FC6 0.29, João Barbosa will give a lecture entitled ‘Regular Types and Their Properties’.
Title
Regular Types and Their Properties
Abstract
Regular types are types that can be described by regular term grammars. They correspond to recursive sets of ground terms that have decidable intersection, comparison, and emptiness checking. They have been used extensively as the types for logic programs, since they are easily implemented in logic programs themselves. Additionally, they are related to algebraic data types, that have been extensively used as types in functional programming. Several operations and properties of regular types have been formalized and used in type inference algorithms, to limited success. We will also extend on this definition by adding variables and discovering where that leads us in terms of expressiveness and decidability of operations.
Bio
João Barbosa has a PhD in Computer Science, in the Faculty of Science of the University of Porto and is a Professor at this Faculty. He started his research trying to describe a type discipline for logic programming, which is typically untyped. His Master thesis was based on the concept of regular types and a subset of those, called Closed Types. In his PhD thesis, he described a three-valued declarative semantics for logic programming, a type system, and a type inference algorithm which inferred Closed (Regular) Types. He also described a typed operational semantics for logic programming, which was based on the same three-valued logic, and described how it can be extended from the traditional operational semantics (SLD-resolution) and used to detect type errors in programs/queries.
Recently he has described a typed unification algorithm and implemented a Prolog interpreter that uses the typed operational semantics I developed during his PhD and the typed unification algorithm. The implementation is in Maude, a rewriting logic framework. He is also currently using tree automata in order to obtain further algorithms for regular types, by relating the two. This relation will be formalized using a proof assistant, Lean.