Monday, February 6, 2012 - 4:00pm to 4:50pm
Weniger 149

Speaker Information

Barry Jay
Associate Professor
School of Software and the Centre for Quantum Computing and Intelligent Systems
University of Technology, Sydney


Intensional computing has recently been generalised from database queries to arbitrary data structures, and then to combinators representing arbitrary functions, and this with enough expressive  power to support statically typed self-interpretation. This talk extends all of these ideas to a lambda calculus with six additional constants. The challenge of querying the body of a lambda abstraction (of looking "under the lambda") is handled by reducing lambda abstractions to combinators. Confluence of reduction is maintained by appropriately restricting the reduction of abstractions.

All of the operators can be typed using standard, quantified function type. However, to type generic queries requires two new  type forms. Operator types are used to identify the principal types of operators. Constraint types are used to incorporate type equations within types: a term has type [P=U]T if it has type T under the assumption that P=U.

Speaker Bio

Associate Professor Barry Jay is a member of the School of Software and the Centre for Quantum Computing and Intelligent Systems at the University of Technology, Sydney. He obtained his BSc (Hons, pure mathematics) from the University of Sydney (1980) and his PhD (mathematics) from McGill University, Montreal (1984). He learned about computing as a senior research fellow at the Laboratory for the Foundations of Computer Science in Edinburgh before moving to UTS in 1993. His current research develops the pattern calculus and its implications for programming in his language bondi, as set out in his recent Springer monograph "Pattern Calculus: Computing with Functions and Structures".