Associate Professor Barry Jay

Jay, B. 2009, Pattern Calculus: Computing with Functions and Structures, 1, Springer, New York, USA.
View/Download from: UTSePress | Publisher's site
View description>>

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. & 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: UTSePress
View description>>

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: UTSePress | Publisher's site
View description>>

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.

Jay, B. 2004, 'The Pattern Calculus', ACM Transactions on Programming Language and Systems (TOPLAS), vol. 26, no. 6, pp. 911-937.
View/Download from: UTSePress
View description>>

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., Lu, H.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: UTSePress | Publisher's site
View description>>

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. & Palsberg, J. 2011, 'Typed Self-Interpretation by Pattern Matching', International Conference on Functional Programming, Tokyo, Japan, September 2011 in The 16th ACM SIGPLAN International Conference on Functional Programming, ed Olivier Danvy, ACMPress, New York, pp. 247-258.
View/Download from: UTSePress
View description>>

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.

Given-Wilson, T.P., Gorla, D. & Jay, B. 2010, 'Concurrent Pattern Calculus', IFIP International Conference on Theoretical Computer Science, Brisbane, Australia, September 2010 in IFIP Advances in Information and Communication Technology - Theoretical Computer Science - Proceedings of 6th IFIP TC 1/WG 2.2 International Conference, ed C. Calude and V. Sassone, Springer, The Netherlands, pp. 244-258.
View/Download from: UTSePress | Publisher's site
View description>>

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', International Conference, MPC, Marseille, France, July 2008 in Mathematics of Program Construction Proceedings, ed Philippe Audebaud, Christine Paulin-Mohring, Springer, Germany, pp. 2-27.
View/Download from: UTSePress | Publisher's site
View description>>

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.

Huang, F.Y., Jay, B. & Skillicorn, D. 2006, 'Adaptiveness in Well-Typed java bytecode verification', Conference of the Center for Advanced Studies on Collaborative Research, Toronto, Canada, October 2006 in Proceedings of the CASCON 2006, ed Erdogmus, H; Stroulia, E; Stewart, D, ACM Press, Toronto, Canada, pp. 1-15.
View/Download from: UTSePress
View description>>

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.

Huang, F.Y., Jay, B. & Skillicorn, D. 2006, 'Programming with Heterogeneous Structures: Manipulating XML data Using bondi', Australasian Computer Science Conference, Hobart, Tasmania, January 2006 in Computer Science 2006 - Proceedings of the 29th Australasian Computer Science Conference, ed Estivill-Castro, V; Dobbie, G, Australian Computer Society Inc, Sydney, Australia, pp. 287-295.
View/Download from: UTSePress
View description>>

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. & Kesner, D. 2006, 'Pure pattern calculus', European Symposium on Programming, Austria, March 2006 in Programming Languages And Systems, Proceedings, Lecture Notes in Computer Science, ed Sestoff, P, Springer-Verlag Berlin, Berlin, Germany, pp. 100-114.
View/Download from: UTSePress | Publisher's site
View description>>

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

Murdaca, C., Jay, B. 2006, 'A relational Account of Objects', Australasian Computer Science Conference, Hobart, Tasmania, January 2006 in Computer Science 2006 - Proceddings of the 29th Australasian Computer Science Conference, ed Estivill-Castro, V; Dobbie, G, Australian Computer Science Society Inc, Sydney, Australia, pp. 297-302.
View/Download from: UTSePress