Barry Jay


Associate Professor; researches and lectures in the School of Software at the University of Technology Sydney.

Associate Professor Barry Jay is a member of the School of Software and the Centre for Artificial Intelligence 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 research focuses on calculi for computation, and their realisation in new programming languages that stretch the functional programming paradigm in unexpected ways. His most recent language was bondi, which realises the pattern calculus (Springer 2009). Since then he has developed novel combinatory calculi that support program analysis as part of a general account of intensional computation.

He teaches research students how to organise their thoughts, one paragraph at a time.

 Pattern Calculus

 Programs as Data Structures in λSF-Calculus

YOW! Lambda Jam 2017 Sydney

Beyond Lambda-Calculus: Intensional Computation


There is a paradox in the foundations of computing. On the one hand, lambda calculus is supposed to compute anything that can be computed. On the other hand, many intensional computations, such as deciding equality of programs (terms in closed normal form), are not definable within lambda calculus. The paradox has now been resolved by close reading of the original papers and books, which clarifies that lambda calculus is inherently extensional.

More importantly, there are new, intensional calculi which are more expressive than lambda calculus. First, pattern calculus supports both higher-order functions and generic queries of data structures, by basing all computation on pattern matching. Second, SF-calculus can query programs as well as data structures by factoring them, using the operator F. In particular, the Goedel number of a program can be defined within the calculus itself.Third, lambda-SF calculus adds native support for lambda-abstraction to SF-calculus. Other calculi are currently under development.

Pattern calculus has been realised in the programming language, bondi. Even better programming languages are now possible.