UTS site search

Associate Professor Barry Jay


Associate Professor Barry Jay is a member of the School of Software 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 in1993. He served a term as Associate Dean for Research.

Image of Barry Jay
Associate Professor, School of Software
Core Member, Centre for Artificial Intelligence
BSc (Hons) (Syd), PhD (McGill)
+61 2 9514 1814
+61 2 9514 4535

Research Interests

  In 1990s he developed the theory of shaped data structures  which underpins his language FISh. In 2000s he developed pattern calculus which underpins the bondi programming language, as explained in his monograph "Pattern Calculus" (Springer, 2009).  In 2010s he is developing a general theory of intensional computation, in which the generic queries of pattern calculus are generalised to include program analyses that are written in the source language, without any need for encoding. Recently, he has been verifying his proofs using he Coq theorem-prover, and uploading them to GitHub.

Can supervise: Yes


Jay, B. 2009, Pattern Calculus: Computing with Functions and Structures, 1, Springer, New York, USA.
View/Download from: UTS OPUS or Publisher's site
The pattern calculus is a new foundation for computation, in which the expressive power of functions and of data structures are fruitfully combined within pattern-matching functions. The best of existing foundations focus on either functions (in the lambda-calculus) or on data structures (in Turing machines) or compromise on both (as in object-orientation). By contrast, a small typed pattern calculus supports all the main programming styles, including functional, imperative, object-oriented and query-based styles. Indeed, it may help to support web services, to the extent that these are generic functions applied to partially specified data structures.


Jay, B. & Vergara Medina, J.A. 2013, 'Growing a Language in Pattern Calculus', 2013 International Symposium on Theoretical Aspects of Software Engineering, IEEE, Birmingham UK, pp. 233-240.
View/Download from: UTS OPUS or Publisher's site
Pattern calculus treats all computation as pattern matching, which is, in turn, central to the implementation of programming languages. Hence, its realisation in the general purpose language bondi provides a natural host in which to develop domain-specific languages (DSLs). bondi is a strongly typed language that supports mixing of programming styles to support the features required for language implementation. In particular, bondi supports queries, views and transformations that can be used to develop object-oriented meta-models. The approach is illustrated by growing a small combinatory language in which each language feature i.e. each production of each grammar, is isolated within a single object-oriented class that captures the rules for parsing, type inference, evaluation and printing. Further, growth is used to support lambda-abstractions, providing good evidence that this combinatory language could grow to support a general purpose programming language.
Jay, B. & Palsberg, J. 2011, 'Typed Self-Interpretation by Pattern Matching', The 16th ACM SIGPLAN International Conference on Functional Programming, International Conference on Functional Programming, ACMPress, Tokyo, Japan, pp. 247-258.
View/Download from: UTS OPUS
Self-interpreters can be roughly divided into two sorts: self-recognisers that recover the input program from a canonical representation, and self-enactors that execute the input program. Major progress for statistically-typed languages was achieved in 2009 by Rendal, Ostermann, and Hofer who presented the first typed self-recogniser that allows representations of different terms to have different types. A key feature of their type system is a type:type rule that renders the kind system of their language inconsistent.
Jay, B., Palsberg, J. & ACM 2011, 'Typed Self-Interpretation by Pattern Matching', ICFP 11 - PROCEEDINGS OF THE 2011 ACM SIGPLAN: INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING, pp. 247-258.
Given-Wilson, T.P., Gorla, D. & Jay, B. 2010, 'Concurrent Pattern Calculus', IFIP Advances in Information and Communication Technology - Theoretical Computer Science - Proceedings of 6th IFIP TC 1/WG 2.2 International Conference, IFIP International Conference on Theoretical Computer Science, Springer, Brisbane, Australia, pp. 244-258.
View/Download from: UTS OPUS or Publisher's site
Concurrent pattern calculus drives interaction between processes by unifying patterns, just as sequential pattern calculus drives computation by matching a pattern against a data structure. By generalising from pattern matching to unification, interaction becomes symmetrical, with information flowing in both directions. This provides a natural language for describing any form of exchange or trade. Many popular process calculi can be encoded in concurrent pattern calculus.
Jay, B. & Jones, S.P. 2008, 'Scrap Your Type Applications', Mathematics of Program Construction Proceedings, International Conference, MPC, Springer, Marseille, France, pp. 2-27.
View/Download from: UTS OPUS or Publisher's site
We intoduce System IF, for implicit System F, in which many type applications can be made implicit. It supports decidable type checking and strong normalisation. System IF constitutes a first foray into a new area in the design space of typed lambda calculi, that is interesting in its own right and may prove useful in practice.
Jay, B. 2007, 'N/A', Proceedings of the Thirteenth Computing: The Austalasian Theory Symposium (CATS2007), Computing: The Australasian Theory Symposium, Australian Computer Society, Victoria, Australia, pp. 1-163.
Huang, F.Y., Jay, B. & Skillicorn, D. 2006, 'Programming with Heterogeneous Structures: Manipulating XML data Using bondi', Computer Science 2006 - Proceedings of the 29th Australasian Computer Science Conference, Australasian Computer Science Conference, Australian Computer Society Inc, Hobart, Tasmania, pp. 287-295.
View/Download from: UTS OPUS
Manipulating semistructured data such as XML does not fit well within conventional programming languages A typical manipulation requires finding all occurrences of a structure matching a structured search pattern whose context may be different in different places, and both aspects cause difficulty If a special purpose query language is used to manipulate XML, an interface to a more general programming environment is required and this interface typically creates runtime overhead for type conversion. However, adding XML manipulation to a general purpose programming language has proven difficult because of problems associated with expressiveness and typing
Jay, B. 2006, 'Typing first-class patterns', Higher-Order Rewriting, electronic proceedings, Higher-Order Rewriting, Seattle, pp. 1-6.
fully refereed workshop but only electronic publication
Murdaca, C. & Jay, B. 2006, 'A relational Account of Objects', Computer Science 2006 - Proceddings of the 29th Australasian Computer Science Conference, Australasian Computer Science Conference, Australian Computer Science Society Inc, Hobart, Tasmania, pp. 297-302.
View/Download from: UTS OPUS
Huang, F.Y., Jay, B. & Skillicorn, D. 2006, 'Adaptiveness in Well-Typed java bytecode verification', Proceedings of the CASCON 2006, Conference of the Center for Advanced Studies on Collaborative Research, ACM Press, Toronto, Canada, pp. 1-15.
View/Download from: UTS OPUS or Publisher's site
Research on security techniques for Java bytecode has paid little attention to the security of the implementations of the techniques themselves, assuming that ordinary tools for programming, verification and testing are sufficient for security. However, different categories of security policies and mechanisms usually require different implementations. Each implementation requires extensive effort to test it and/or verify it.We show that programming with well-typed pattern structures in a statically well-typed language makes it possible to implement static byte-code verification in a fully type-safe and highly adaptive way, with security policies being fed in as first-order parameters, reduces the effort required to verify security of an implementation itself and the programming need for new policies. Also bytecode instrumentation can be handled in exactly the same way. The approach aims at reducing the workload of building and understanding distributed systems, especially those of mobile code.
Jay, B. 2006, 'Type variables simplify sub-typing', Higher-Order Rewriting, electronic proceedings, Higher-Order Rewriting, Seattle, pp. 1-6.
fully refereed workshop
Jay, B. & Kesner, D. 2006, 'Pure pattern calculus', Programming Languages And Systems, Proceedings, Lecture Notes in Computer Science, European Symposium on Programming, Springer-Verlag Berlin, Austria, pp. 100-114.
View/Download from: UTS OPUS or Publisher's site
The pure pattern calculus generalises the pure lambda-calculus by basing computation on pattern-matching instead of beta-reduction. The simplicity and power of the calculus derive from allowing any term to be a pattern. As well as supporting a uniform ap
Lederer, B., Plekhanova, V. & Jay, C.B. 2000, 'Teaching a capstone subject in computing science - A variety engineering approach', Proceedings - 23rd Australasian Computer Science Conference, ACSC 2000, pp. 136-142.
View/Download from: Publisher's site
© 2000 IEEE. Software Development Case Study is a capstone subject in the BSc (Computing) degree at the University of Technology, Sydney. Its purpose is to give students as realistic an experience as possible of working in an IT industry environment on software development. At the same time we are trying to ensure that certain educational aims, such as students being exposed to programming in the large and having a sense of engaging with this task and completing it, are met. In analysing the way we run the course we use Ashby's concept of requisite variety: that for a system's essential variables (subject coordinator) must be able to deploy enough variety (or manoeuvres) to match that of the system being regulated (class). In our case the regulatory variety relates to the type and complexity of the projects on offer as well as to the project roles; this has to match the variety of vocational needs and interests brought to us by the students. We give examples of how conflicts, e.g. between educational and industrial aims, can trigger the emergence of new regulatory variety (such as specialised approaches to the task). We also describe how the coordinator's regulatory variety is amplified by involving the students: e.g. in the framing of the project requirements, where we solicit input from the students via proposals: or in the running of the teams, where the students manage themselves but with monitoring by liaison officers. This student-centred approach is designed to promote project ownership and team responsibility. Although it also produces greater task uncertainty than the students are used to it provides them with greater opportunities for exploration and creativity.
Jay, C.B. 1999, 'Denotational semantics of shape: Past, present and future', Electronic Notes in Theoretical Computer Science, pp. 320-333.
View/Download from: Publisher's site
Past work on the semantics of vectors and arrays provides a denotational semantics for the new, higher-order, polymorphic array programming language FISh, that uses static analysis to determine array shapes. This semantics will be combined with that of shape polymorphism to underpin a language that will support both shape analysis and shape polymorphism on both arrays and inductive types. ©1999 Published by Elsevier Science B. V.
Jay, C.B., Cole, M.I., Sekanina, M. & Steckler, P. 1997, 'A monadic calculus for parallel costing of a functional language of arrays', Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 650-661.
VEC is a higher-order functional language of nested arrays, which includes a general folding operation. Static computation of the shape of its programs is used to support a compositional cost calculus basedmn a cost monad. This, in turn, is based on a cost algebra, whose operations may be customized to handle different cost regimes, especially for parallel programming. We present examples based on sequential costing and on the PRAM model of parallel computation. The latter has been implemented in Haskell, and applied to some linear algebra examples.

Journal articles

Jay, B. 2016, 'Programs as Data Structures in SF-Calculus', Electronic Notes in Theoretical Computer Science, vol. 325, pp. 221-236.
View/Download from: Publisher's site
© 2016 The Author(s) Lambda-SF-calculus can represent programs as closed normal forms. In turn, all closed normal forms are data structures, in the sense that their internal structure is accessible through queries defined in the calculus, even to the point of constructing the Goedel number of a program. Thus, program analysis and optimisation can be performed entirely within the calculus, without requiring any meta-level process of quotation to produce a data structure. Lambda-SF-calculus is a confluent, applicative rewriting system derived from lambda-calculus, and the combinatory SF-calculus. Its superior expressive power relative to lambda-calculus is demonstrated by the ability to decide if two programs are syntactically equal, or to determine if a program uses its input. Indeed, there is no homomorphism of applicative rewriting systems from lambda-SF-calculus to lambda-calculus. Program analysis and optimisation can be illustrated by considering the conversion of a programs to combinators. Traditionally, a program p is interpreted using fixpoint constructions that do not have normal forms, but combinatory techniques can be used to block reduction until the program arguments are given. That is, p is interpreted by a closed normal form M. Then factorisation (by F) adapts the traditional account of lambda-abstraction in combinatory logic to convert M to a combinator N that is equivalent to M in the following two senses. First, N is extensionally equivalent to M where extensional equivalence is defined in terms of eta-reduction. Second, the conversion is an intensional equivalence in that it does not lose any information, and so can be reversed by another definable conversion. Further, the standard optimisations of the conversion process are all definable within lambda-SF-calculus, even those involving free variable analysis. Proofs of all theorems in the paper have been verified using the Coq theorem prover.
Given-Wilson, T., Gorla, D. & Jay, B. 2014, 'A CONCURRENT PATTERN CALCULUS', LOGICAL METHODS IN COMPUTER SCIENCE, vol. 10, no. 3.
View/Download from: UTS OPUS or Publisher's site
Jay, B. & Given-Wilson, T.P. 2011, 'A Combinatory Account of Internal Structure', Journal Of Symbolic Logic, vol. 76, no. 3, pp. 807-826.
View/Download from: UTS OPUS or Publisher's site
Traditional combinatory logic uses combinators S and K to represent all Turing-computable functions on natural numbers, but there are Turing-computable functions on the combinators themselves that cannot be so represented, because they access internal structure in ways that S and K cannot. Much of this expressive power is captured by adding a factorisation combinator F. The resulting SF-calculus is structure complete, in that it supports all pattern-matching functions whose patterns are in normal form, including a function that decides structural equality of arbitrary normal forms. A general characterisation of the structure complete, confluent combinatory calculi is given along with some examples. These are able to represent all their Turing-computable functions whose domain is limited to normal forms. The combinator F can be typed using an existential type to represent internal type information.
Jay, B. & Kesner, D. 2009, 'First-class patterns', Journal Of Functional Programming, vol. 19, no. 2, pp. 191-225.
View/Download from: UTS OPUS or Publisher's site
Pure pattern calculus supports pattern-matching functions in which patterns are first-class citizens that can be passed as parameters, evaluated and returned as results. This new expressive power supports two new forms of polymorphism. Path polymorphism allows recursive functions to traverse arbitrary data structures. Pattern polymorphism allows patterns to be treated as parameters which may be collected from various sources or generated from training data. A general framework for pattern calculi is developed. It supports a proof of confluence that is parameterised by the nature of the matching algorithm, Suitable for the pure pattern calculus and all other known pattern calculi.
Gudmundsson, J. & Jay, B. 2007, 'Preface to Special Issue: Selected Papers from CATS 2006', International Journal Of Foundations Of Computer Science, vol. 18, no. 2, pp. 195-196.
Gudmundsson, J. & Jay, B. 2007, 'Untitled', INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, vol. 18, no. 2, pp. 195-196.
View/Download from: Publisher's site
Jay, B., Lu, H. & Nguyen, Q. 2004, 'The Polymorphic Imperative: a Generic Approach to In-place Update', Electronic Notes in Theoretical Computer Science - Proceedings of Computing: The Australasian Theory Symposium (CATS) 2004, vol. 91, pp. 195-211.
View/Download from: UTS OPUS
The constructor calculus supports generic operations defined over arbitrary data types including abstract data types. This paper extends the basic constructor calculus to handle constructed locations. The resulting calculus is able to define a generic assignment operation that performs in-place whenever appropriate and allocates fresh memory otherwise. This approach may eliminate many of the space overheads associated with higher-order polymorphic languages. In combination with existing generic programming techniques it can express some very powerful algorithms such as the visitor pattern.
Jay, B. 2004, 'The Pattern Calculus', ACM Transactions on Programming Language and Systems (TOPLAS), vol. 26, no. 6, pp. 911-937.
View/Download from: UTS OPUS or Publisher's site
There is a significant class of operations such as mapping that are common to all data structures. The goal of generic programming is to support these operations on arbitrary data types without having to recode for each new type. The pattern calculus and combinatory type system reach this goal by representing each data structure as a combination of names and a finite set of constructors. These can be used to define generic functions by pattern-matching programs in which each pattern has a different type. Evaluation is type-free. Polymorphism is captured by quantifying over type variables that represent unknown structures. A practical type inference algorithm is provided.
Jay, B. 2001, 'Distinguishing Data Structures And Functions: The Constructor Calculus And Functorial Types', Typed Lambda Calculi And Applications, Proceedings, vol. 2044, pp. 217-239.
The expressive power of functional programming can be improved by identifying and exploiting the characteristics that distinguish data types from function types. Data types support generic functions for equality, mapping, folding, etc. that do not apply
Jay, B. 2000, 'Costing Parallel Programs As A Function Of Shapes', Science Of Computer Programming, vol. 37, pp. 207-224.
View/Download from: Publisher's site
Portable, efficient, parallel programming requires cost models to compare different possible implementations. In turn, these require knowledge of the shapes of the data structures being used, as well as knowledge of the hardware parameters. This paper sh
Jay, C.B. 1999, 'Programming in FISh', International Journal on Software Tools for Technology Transfer, vol. 2, no. 3, pp. 307-315.
View/Download from: Publisher's site
Shape is a new abstraction that can be used to organise and optimise programs. In brief, the shape of a data structure is a description of its structure independent of the particular choice of the data stored within it. For example, the shape of a matrix of integers is determined by the number of its rows and columns. Shapes have been incorporated into the design of the FISh programming language. This paper uses simple programs written in FISh to illustrate the main benefits of a shaped approach. © 1999 Springer-Verlag.
Jay, B. & Steckler, P. 1998, 'The Functional Imperative: Shape!', Programming Languages And Systems, vol. 1381, pp. 139-153.
Jay, B. 1997, 'Covariant Types', Theoretical Computer Science, vol. 185, pp. 237-258.
The covariant type system is an impredicative system that is rich enough to represent some polymorphism on inductive types, such as lists and trees, and yet is simple enough to have a set-theoretic semantics. Its chief novelty is to replace function type
Jay, B. 1997, 'Finite Objects In A Locos', Journal Of Pure And Applied Algebra, vol. 116, pp. 169-183.
View/Download from: Publisher's site
Listable objects in a locos are those which have a (finite) list of elements. Their full subcategory forms a 2-valued topos satisfying the axiom of choice. Listable objects are isomorphic to finite cardinals. (C) 1997 Elsevier Science B.V.
Jay, B. 1996, 'Shape In Computing', ACM Computing Surveys, vol. 28, pp. 355-357.
View/Download from: Publisher's site
Jay, B. & Staples, J. 1996, 'Theoretical computer science in Australia and New Zealand - Preface', THEORETICAL COMPUTER SCIENCE, vol. 169, no. 1, pp. 1-1.
View/Download from: Publisher's site
Jay, B. 1995, 'A Semantics For Shape', Science Of Computer Programming, vol. 25, pp. 251-283.
View/Download from: Publisher's site
Shapely types separate data, represented by lists, from shape, or structure. This separation supports shape polymorphism, where operations are defined for arbitrary shapes, and shapely operations, for which the shape of the result is determined by that o
Jay, B. 1993, 'Tail Recursion Through Universal Invariants', Theoretical Computer Science, vol. 115, pp. 151-189.
Tail-recursive constructions suggest a new semantics for datatypes, which allows a direct match between specifications and tail-recursive programs. The semantics focuses on loops, their fixpoints, invariants and convergence. Convergent models of the natu
Steffen, B., Jay, B. & Mendler, M. 1992, 'Compositional Characterization Of Observable Program Properties', Rairo-informatique Theorique Et Applications-theoretical Informatics And Applications, vol. 26, pp. 403-424.
In this paper we model both program behaviours and abstractions between them as lax functors, which generalize abstract interpretations by exploiting the natural ordering of program properties. This generalization provides a framework in which correctnes
Jay, B. 1991, 'Fixpoint And Loop Constructions As Colimits', Lecture Notes In Mathematics, vol. 1488, pp. 187-192.
The constructions of fixpoints and while-loops in a category of domains can be derived from the colimit, loop(f) of a diagram which consists of a single endomorphism f : D --> D. If f is increasing then the colimiting map is the least-fixpoint function Y
Jay, B. 1991, 'Tail Recursion From Universal Invariants', Lecture Notes In Computer Science, vol. 530, pp. 151-163.
The categorical account of lists is usually given in terms of initial algebras, i.e. head recursion. But it is also possible to define them by interpreting tail recursion by means of the colimit of a loop diagram, i.e. its universal invariant. Parametr
Jay, B. 1990, 'The Structure Of Free Closed Categories', Journal Of Pure And Applied Algebra, vol. 66, pp. 271-285.
View/Download from: Publisher's site
Jay, B. 1989, 'Languages For Monoidal Categories', Journal Of Pure And Applied Algebra, vol. 59, pp. 61-85.
View/Download from: Publisher's site
Jay, B. 1988, 'Local Adjunctions', Journal Of Pure And Applied Algebra, vol. 53, pp. 227-238.
View/Download from: Publisher's site
Jay, B. 1986, 'Lambek Operational Categories', Bulletin Of The Australian Mathematical Society, vol. 33, pp. 161-175.
View/Download from: Publisher's site
Jay, B. & Vergara, J., 'Confusion in the Church-Turing Thesis'.
The Church-Turing Thesis confuses numerical computations with symbolic computations. In particular, any model of computability in which equality is not definable, such as the lambda-models underpinning higher-order programming languages, is not equivalent to the Turing model. However, a modern combinatory calculus, the SF-calculus, can define equality of its closed normal forms, and so yields a model of computability that is equivalent to the Turing model. This has profound implications for programming language design.
Selected Peer-Assessed Projects