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.
Can supervise: YES
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.
Intensional lambda-calculus adds intensional combinators to lambda-calculus to facilitate analysis. In particular, they are used to factorise data structures and programs into their components, which can be used to convert abstractions into combinators. This paper shows how to type an intensional lambda-calculus using no more than the types of System F. Even the quotation function used to access program syntax can be defined and typed, as can its inverse: the calculus supports typed self-quotation. Thus, one may freely alternate between program analysis and program execution. Proofs of all results have been verified in Coq.
Abstract A function on some domain is -definable if the corresponding function of -terms is so definable. However, the correspondence is parametrized by a representation of the domain. Often there is a natural choice of representation, but when the domain consists of -terms then they can be represented by either themselves or by the Church numeral of their Gdel number. This choice determines whether or not all computable functions are -definable.
Jay, B 2016, 'Programs as Data Structures in SF-Calculus', Electronic Notes in Theoretical Computer Science, vol. 325, pp. 221-236.
Abstract 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.
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. © IFIP International Federation for Information Processing 2010.
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.
Jay, B 2004, 'The pattern calculus', ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 26, pp. 911-937.
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, CB 2001, 'Distinguishing Data Structures and Functions: the Constructor Calculus and Functorial Types', Typed Lambda Calculi and Applications: 5th International Conference TLCA 2001, Kraków, Poland, May 2001 Proceedings, vol. 2044, pp. 217-239.
Jay, CB 2000, 'Costing parallel programs as a function of shapes', Science of Computer Programming, pp. 207-224.
Jay, CB 1999, 'Partial evaluation of shaped programs: experience with FISh', pp. 23 pp-23 pp.
Jay, CB 1999, 'Programming in FISh', International Journal on Software Tools for Technology Transfer, vol. 2.
Jay, CB, Bellè, G & Moggi, E 1998, 'Functorial ML', Journal of Functional Programming, vol. 8, pp. 573-619.
Jay, CB 1997, 'Covariant types', Theoretical Computer Science, vol. 185, pp. 237-258.
Jay, CB & Steckler, PA 1997, 'The Functional Imperative: Shape!'.
Jay, CB 1997, 'Finite Objects in a Locos', Journal of Pure and Applied Algebra, vol. 116, pp. 169-83.
Jay, CB & Staples, J 1996, 'Preface to a special issue on Australasian research', Theoretical Computer Science, vol. 169.
Jay, CB 1996, 'Shape in computing', ACM Computing Surveys, vol. 28, pp. 355-357.
Jay, CB & Ghani, N 1995, 'The virtues of eta-expansion', J. of Functional Programming, vol. 5, pp. 135-154.
Jay, CB 1995, 'Covariant types'.
Jay, CB 1995, 'A semantics for shape', Science of Computer Programming, vol. 25, pp. 251-283.
Jay, CB 1993, 'Tail recursion through universal invariants', Theoretical Computer Science, vol. 115, pp. 151-189.
Jay, CB 1992, 'Coherence in category theory and the Church-Rosser property', Notre Dame J. of Formal Logic, vol. 33, pp. 140-143.
Steffen, B, Jay, CB & Mendler, M 1992, 'Compositional characterisation of observable program properties', Theoretical Informatics and Applications, vol. 26, pp. 403-424.
Jay, CB 1991, 'Tail recursion via universal invariants'.
Jay, CB 1991, 'Fixpoint and loop constructions as colimits', Proceedings Summer Conference on Category Theory, Como 1990, vol. 1488, pp. 187-192.
Jay, CB 1991, 'Tail recursion from universal invariants', Category Theory and Computer Science Paris, France, September 1991 Proceedings, vol. 530, pp. 151-163.
Jay, CB 1990, 'A note on natural numbers objects in monoidal categories', Studia Logica, vol. 48, pp. 389-93.
Jay, CB 1990, 'Languages for triples, bicategories and braided monoidal categories', Cahiers de Topologie et Géométrie Différentielle Catégoriques, vol. 31, pp. 67-81.
Jay, CB 1990, 'The structure of free closed categories', Journal of Pure and Applied Algebra, vol. 66, pp. 271-285.
Steffen, B, Jay, CB & Mendler, M 1989, 'Compositional characterisation of observable program properties'.
Jay, CB 1989, 'Languages for monoidal categories', Journal of Pure and Applied Algebra, vol. 59, pp. 61-85.
Jay, CB 1988, 'Local adjunctions', Journal of Pure and Applied Algebra, vol. 53, pp. 227-238.
Jay, CB 1986, 'Lambek's operational categories', Bulletin of the Australian Mathematical Society, vol. 33, pp. 161-176.
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.
Jay, CB 1999, 'Research Directions in Parallel Functional Programming, K. Hammond and G.J. Michaelson (eds)', Springer-Verlag, pp. 219-232.
Jay, B 2018, 'Recursive Programs in Normal Form (Short Paper)', Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, ACM, pp. 67-73.
Given-Wilson, T, Huang, F & Jay, B 2013, 'Multi-polymorphic programming in bondi', Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP, pp. 53-60.View/Download from: Publisher's site
The bondi programming language is multi-polymorphic, in that it supports four polymorphic programming styles within a small core of computation, namely a typed pattern calculus. bondi's expressive power is illustrated by considering the problem of assigning reviewers to a paper. As the context generalises from a committee to a committee with additional reviewers, to a conference, to a federation or confederation, the solution incorporates polymorphism familiar from the functional, generic functional, relational, path-based, and object-oriented programming styles, respectively. These experiments show that multi-polymorphic programming is both practical and desirable. Copyright © 2013 ACM.
Jay, B & Vergara, J 2013, 'Growing a Language in Pattern Calculus', Theoretical Aspects of Software Engineering (TASE), 2013 International Symposium on, IEEE, pp. 233-240.
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.
Jay, B & Palsberg, J 2011, 'Typed self-interpretation by pattern matching', Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP, pp. 247-258.View/Download from: Publisher's site
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 statically-typed languages was achieved in 2009 by Rendel, Ostermann, and Hofer who presented the first typed selfrecogniser 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. In this paper we present the first statically-typed language that not only allows representations of different terms to have different types, and supports a self-recogniser, but also supports a selfenactor. Our language is a factorisation calculus in the style of Jay and Given-Wilson, a combinatory calculus with a factorisation operator that is powerful enough to support the pattern-matching functions necessary for a self-interpreter. This allows us to avoid a type:type rule. Indeed, the types of System F are sufficient. We have implemented our approach and our experiments support the theory. Copyright © 2011 ACM.
Jay, B & Palsberg, J 2011, 'Typed Self-Interpretation by Pattern Matching', Proceedings of the 2011 ACM Sigplan International Conference on Functional Programming, pp. 247-58.View/Download from: UTS OPUS
Jay, B & Jones, SP 2008, 'Scrap your type applications', Mathematics of Program Construction, 9th International Conference, MPC 2008, Marseille, France, July 2008, Springer, pp. 2-27.View/Download from: UTS OPUS
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, FY, Jay, CB & Skillicorn, DB 2006, 'Adaptiveness in well-typed Java bytecode verification', CASCON '06: Proceedings of the 2006 conference of the Center for Advanced Studies on Collaborative research, ACM Press, pp. 19-19.
Jay, B & Kesner, D 2006, 'Pure Pattern Calculus.', Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27–28, 2006, Proceedings (ed: P. Sestoft), pp. 100-114.
Huang, F, Jay, B & Skillicorn, D 2006, 'Programming with Heterogeneous Structures: Manipulating XML data Using \bf bondi', Twenty-Ninth Australasian Computer Science Conference (ACSC2006), pp. 287-296.View/Download from: UTS OPUS
Jay, CB 2006, 'Typing first-class patterns', Higher-Order Rewriting, electronic proceedings.
Huang, FY, 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, CB 2006, 'Type variables simplify sub-typing', Higher-Order Rewriting, electronic proceedings.
Jay, CB, Lu, HY & Nguyen, QT 2004, 'The Polymorphic Imperative', Computing:The Australasian Theory Symposium 2004, Science Direct, pp. 192-206.
Jay, CB 2004, 'Methods as pattern-matching functions', Foundations of Object-Oriented Languages, 2004, pp. 16 pp-16 pp.
Jay, CB & Keller, G 2000, 'Towards Dynamic Shaping', Communication-Based Systems: Proceedings of the 3rd International Workshop held at the TU Berlin, Germany, 31 March - 1 April 2000, Kluwer Academic Publishers, pp. 103-110.
Lederer, B, Plekhanova, V & Jay, CB 2000, 'Teaching a capstone subject in computer science – a variety engineering approach', Proceedings of the 23rd Australasian Computer Science Conference ACSC 2000 Canberra, Australia January 31 – February 3, 2000., Computer Science Association, pp. 136-142.
Moggi, E, Bellè & Jay, CB 1999, 'Monads, Shapely Functors and Traversals', Proceedings of the Eighth Conference on Category Theory and Computer Science (CTCS'99), Elsevier, pp. 265-286.
Jay, CB 1999, 'Partial evaluation of shaped programs: experience with FISh', ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '99) San Antonio, Texas, January 22-23, 1999: Proceedings, BRICS, pp. 147-158.
Jay, CB 1999, 'Denotational Semantics of Shape: Past, Present and Future', Fifteenth Conference on the Mathematical Foundations of Programming Semantics (MFPS XV) Tulane University New Orleans, LA USA April 28 - May 1, 1999: Proceedings, Elsevier, pp. 197-210.
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.
Moggi, E, Bellè & Jay, CB 1998, 'Monads, Shapely Functors and Traversals', Università di Genova.
Jay, CB & Steckler, PA 1998, 'The functional imperative: shape!', Programming languages and systems: 7th European Symposium on Programming, ESOP'98 Held as part of the joint european conferences on theory and practice of software, ETAPS'98 Lisbon, Portugal, March/April 1998, Springer Verlag, pp. 139-53.
Jay, CB, Moggi, E & Bellè, G 1998, 'Functors, types and shapes', Workshop on Generic Programming: Marstrand, Sweden, 18th June, 1998, Chalmers University of Technology, pp. 21-4.
Palsberg, J, Jay, CB & Noble, J 1998, 'Experiments with generic visitors', Workshop on generic programming: Marstrand, Sweden, 18th June, 1998, pp. 81-4.
Palsberg, J & Jay, CB 1997, 'The Essence of the Visitor Pattern', University of Technology, Sydney.
Jay, CB 1997, 'Separating shape from data', Category theory and computer science: 7th international conference, CTCS'97, Santa Margherita Ligure, Italy, September 1997 Proceedings, Springer Verlag, pp. 47-48.
Jay, CB & Sekanina, M 1997, 'Shape checking of array programs', Computing: the Australasian Theory Seminar, Proceedings, 1997, pp. 113-121.
Jay, CB, Cole, MI, Sekanina, M & Steckler, PA 1997, 'A Monadic Calculus for Parallel Costing of a Functional Language of Arrays', Euro-Par'97 Parallel Processing, Springer, pp. 650-661.
Bellé, G, Jay, CB & Moggi, E 1996, 'Functorial ML', PLILP '96, Springer Verlag, pp. 32-46.
Jay, CB 1996, 'Data categories', Computing: The Australasian Theory Symposium Proceedings, Melbourne, Australia, 29–30 January, 1996, Australian Computer Science Communications, pp. 21-28.
Jay, CB 1996, 'A fresh look at parametric polymorphism: covariant types', Nineteenth Australasian Computer Science Conference Proceedings, Melbourne, Australia, 31 January – 2 February, 1996, Australian Computer Science Communications, pp. 525-534.
Jay, CB, Clarke, DG & Edwards, JJ 1996, 'Exploiting Shape in Parallel Programming', 1996 IEEE Second International Conference on Algorithms and Architectures for Parallel Processing: Proceedings, IEEE, pp. 295-302.
Jay, CB, Cole, M, Sekanina, M & Steckler, PA 1996, 'A Monadic Calculus for Parallel Costing in a Functional Language of Arrays'.
Jay, CB 1995, 'Polynomial Polymorph\-ism', Proceedings of the Eighteenth Australasian Computer Science Conference: Glenelg, South Australia 1–3 February, 1995, ACS Communications, pp. 237-243.
Jay, CB 1995, 'Shape Analysis for Parallel Computing', Proceedings of the fourth international parallel computing workshop: Imperial College London, 25–26 September, 1995, Imperial College/Fujitsu Parallel Computing Research Centre, pp. 287-298.
Jay, CB & Cockett, JRB 1994, 'Shapely Types and Shape Polymorphism', Programming Languages and Systems – ESOP '94: 5th European Symposium on Programming, Edinburgh, U.K., April 1994, Proceedings, Springer Verlag, pp. 302-316.
Jay, CB 1994, 'A survey of shapely types', Proceedings of Computing: the Australian Theory Seminar, University of Technology, Sydney, 17-19 December, 1994, University of Technology, Sydney, pp. 81-88.
Jay, CB 1994, 'Matrices, monads and the fast Fourier transform', Proceedings of the Massey Functional Programming Workshop 1994, pp. 71-80.
Jay, CB 1992, 'Modelling reduction in confluent categories', Proceedings of the Durham Symposium on Applications of Categories in Computer Science, Cambridge University Press, pp. 143-162.
Jay, CB 1991, 'Partial functions, ordered categories, limits and cartesian closure', IV Higher Order Workshop, Banff, 1990, Springer Verlag, pp. 151-161.
Palsberg, J & Jay, CB, 'The Essence of the Visitor Pattern', Proceedings of COMPSAC'98, 22nd Annual International Computer Software and Applications Conference, pp. 9-15.
Jay, CB & Steckler, PA 1998, Polymorphism over Nested Regular Arrays: theory and implementation in FISh, no. 01, University of Technology, Sydney.
Jay, CB 1996, Type-free term reduction for covariant types, no. 96.07, University of Technology, Sydney.
Jay, CB & Noble, J 1996, Shaping object-oriented programs, no. 96-16, University of Technology, Sydney.
Jay, CB & Cockett, JRB 1994, Shapely Types and Shape Polymorphism: Extended Version, no. UTS-SOCS-94-??, University of Technology, Sydney.
Jay, CB 1993, An introduction to categories in computing, no. UTS-SOCS-93.9, University of Technology, Sydney.
Jay, CB 1993, Matrices, monads and the fast Fourier transform, no. UTS-SOCS-93.13, University of Technology, Sydney.
Jay, CB 1992, Program loops and loops in categories, no. ECS-LFCS-92-205, Edinburgh Univ., Dept. of Comp. Sci..
Jay, CB 1991, Long $$ normal forms and confluence, no. ECS-LFCS-91-183, Edinburgh Univ., Dept. of Comp. Sci..
Jay, CB 1991, Modelling reduction in confluent categories, no. ECS-LFCS-91-187, Edinburgh Univ., Dept. of Comp. Sci..
Jay, CB 1990, Extending properties to categories of partial maps, no. ECS-LFCS 90–107, Edinburgh Univ., Dept. of Comp. Sci..
Jay, B 2018, 'Intensional Computation: three draft chapters'.
Jay, B 2017, 'SF repository of proofs in Coq'.
Jay, B 2017, 'Typed LambdaFactor Calculus repository of proofs in Coq'.
Jay, B 2017, 'A Combinatory Account of Substitution'.
Jay, B 2017, 'Repository of proofs for L-calculus in Coq'.
Jay, B 2017, 'Beyond Lambda-Calculus: Intensional Computation'.
Jay, B 2017, 'Deconstructing Lambda-Calculus'.
Jay, B 2017, 'Intensional-computation, repository of proofs in Coq'.
Jay, B 2016, 'LamSF repository of proofs in Coq'.
Jay, B 2016, 'Typed-LamSF repository of proofs in Coq'.
Jay, B 2010, 'Declaring Classes in Pattern Calculus'.
Jay, CB 2009, 'Objects not Subjects!'.
Jay, B 2005, 'Polymorphic pattern calculus'.
Jay, B 2005, 'Pattern matching against functions'.
Jay, CB 2004, 'Higher-Order Patterns (unpublished)'.
cbj 2004, 'Unifiable Subtyping'.
cbj 2004, 'bondi'.
Jay, CB 2003, 'The constructor calculus (revised)'.
Jay, CB 2002, 'The constructor calculus'.
Jay, CB, Lu, HY & Nguyen, QT 2002, 'The Polymorphic Imperative'.
Jay, CB 2000, 'Functorial lambda-calculus'.
Jay, CB 2000, 'The Functional Imperative'.
Jay, CB 1998, 'Poly-dimensional regular arrays in FISh'.
Jay, CB 1998, 'Poly-dimensional array programming'.
Jay, CB 1998, 'The FISh language definition'.
Jay, CB 1997, 'FiSh v 0.4'.
Jay, CB 1995, 'P2'.