Jeremy Edward DAWSON

Refereed Publications

Computer Science

• Jeremy E. Dawson & Rajeev Goré, Termination of Abstract Reduction Systems. International Journal of Foundations of Computer Science, to appear.

• Jeremy E. Dawson, Isabelle Theories for Machine Words. In Seventh International Workshop on Automated Verification of Critical Systems (AVOCS'07), Oxford, September 2007, Electronic Notes in Theoretical Computer Science, 250 (2009), pp. 55-70, Elsevier. (Also in Proceedings of TPHOLs 2007 Emerging Trends, Internal Report 364/07, Department of Computer Science, University of Kaiserslautern)

• Jeremy E. Dawson, Compound Monads in Specification Languages. In Proceedings of Programming Languages meets Program Verification (PLPV) 2007, Freiburg, October 2007, ACM, 2007, 3-10.

• Jeremy E. Dawson, Formalising Generalised Substitutions. In 20th International Conference on Theorem Proving in Higher Order Logics Kaiserslautern, September 2007 (TPHOLs 2007), LNCS 4732, 54-69.

• Jeremy E. Dawson & Rajeev Goré, Termination of Abstract Reduction Systems. In Computing: The Australasian Theory Symposium, 2007 (CATS 2007), Conferences in Research and Practice in Information Technology (CRPIT), Vol. 65, 35-43.

• Jeremy E. Dawson & Rajeev Goré, A General Theorem on Termination of Rewriting. In Computer Science Logic (CSL'04), LNCS 3210, 100-114.

• Jeremy E. Dawson, Formalising General Correctness. In Computing: The Australasian Theory Symposium, 2004, Electronic Notes in Theoretical Computer Science 91, 46-65, Elsevier.

• Jeremy E. Dawson & Rajeev Goré, A New Machine-checked Proof of Strong Normalisation for Display Logic. In Computing: The Australasian Theory Symposium, 2003, Electronic Notes in Theoretical Computer Science 78, 16-35, Elsevier.

• Jeremy E. Dawson & Rajeev Goré, Machine-checking the Timed Interval Calculus, In 15th Australian Joint Conference on Artificial Intelligence (AI'02), LNCS 2557, 95-106.

• Jeremy E. Dawson & Rajeev Goré, Formalised Cut Admissibility for Display Logic, In 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), LNCS 2410, 131-147.

• Jeremy E. Dawson & Rajeev Goré, Embedding Display Calculi into Logical Frameworks : Comparing Twelf and Isabelle, In Computing: The Australasian Theory Symposium, 2001, Electronic Notes in Theoretical Computer Science, Elsevier, volume 42.

• Jeremy Dawson & Peter Strazdins, Optimizing User-Level Communication Patterns on the Fujitsu AP3000, In IWCC'99, 1st IEEE International Workshop On Cluster Computing, 105-111, IEEE Computer Society Press, Melbourne, Dec 1999.

• Jeremy E. Dawson & Rajeev Goré, A Mechanisation of Classical Modal Tense Logics Using Isabelle, In Proceedings of the 11th Australian Joint Conference on Artificial Intelligence, LNCS 1502, 107-118.

• Jeremy E. Dawson & Rajeev Goré, A Mechanised Proof System for Relation Algebra using Display Logic, In Proceedings of the 6th European Workshop on Logics in Artificial Intelligence, LNCS 1489, 264-278.

• Mechanised Proof Systems for Relation Algebras. Grad. Dip. Sci. subthesis, Dept. of Computer Science, A.N.U., 1997.

Mathematics

• A Note on the construction of GH(4tq,EA(q)) for t = 1,2. Aust. J. Combin. 6 (1992), 177-186 (with W. De Launey).

• An asymptotic result on the existence of Generalized Hadamard Matrices. J. Combinatorial Theory (A) 65 (1994), 158-163 (with W. De Launey).

• Some necessary conditions for sums of matroids. Quart. J. Math. (Oxford) (2) 39 (1988), 281-283.

• Equineighboured designs of block size 4. Ars Combinatoria 19A (1985), 295-301.

• Testing for indirect censoring: a general purpose test and some moment formulae. Festschrift for Bernard G. Greenberg, ed. P.K. Sen (North-Holland, 1985), 345-356 (with N.L. Johnson).

• A construction for the generalized Hadamard matrices GH(4q,EA(q)). J. Statist. Planning & Inference 11 (1985), 103-110.

• Algorithms for directed packings. Annals of Discrete Mathematics 26 (1985), 137-142.

• Solubility of the matroid sum equation. Ars Combinatoria 17A (1984), 103-116.

• A collection of sets related to the Tutte polynomial of a matroid. Proceedings of the First Southeast Asian Colloquium on Graph Theory, Lecture Notes in Mathematics 1073 (Springer-Verlag, 1984), 193-204.

• Decomposition of binary matroids. Combinatorica 5 (1984), 1-9.

• The projective geometry arising from a hollow module. J. Aust. Math. Soc. (A) 37 (1984), 351-357.

• The directed packing numbers DD(t,v,v). Combinatorica 4 (1984), 121-130 (with J.R. Seberry and D.B. Skillicorn).

• Balanced sets in an independence structure induced by a submodular function. J. Math. Anal. & Appl. 95 (1983), 214-222.

• A formula approximating the root of a function. IMA J. of Numerical Anal. 2 (1982), 371-375.

• Independence structures on the submodules of a module. Eur. J. Comb. 6 (1985), 37-44.

• Matroid bases, opposite families and some related algorithms. Combinatorial Mathematics IX, Lecture Notes in Mathematics 952 (Springer-Verlag, 1982), 225-238.

• Independence spaces and uniform modules. Eur. J. Comb. 6 (1985), 29-36.

• Some results on two matroids on a set. Bull. Malaysian Math. Soc. 6 (1983), 19-21.

• The utilization of rice straw fed to Zebu cattle and swamp buffalo as influenced by alkali treatment and lucaena supplementation. Aust. J. Agric. Res. 34 (1983), 73-84 (with J.B. Moran & K.B. Satoto).

• Interactions between Camargue horses and horseflies (Tabanidae). Bull. of Entomological Res. 71 (1981), 227-242 (with R.D. Hughes & P. Duncan).

• A construction for a family of sets and its application to matroids. Combinatorial Mathematics VIII, Lecture Notes in Mathematics 884 (Springer-Verlag, 1981), 136-147.

• A matroid theoretic approach to the matching structure of a graph. Quart. J. Math. (Oxford) (2) 33 (1982), 297-302.

• A simple approach to some basic results in matroid theory. J. Math. Anal. & Appl. 84 (1981), 555-559.

• The algebraic equivalence of two measures of genetic distance. J. Applied Probability 18 (1981), 520-522.

• A note on some algorithms for matroids. J. Math. Anal. & Appl. 75 (1980), 611-615.

• Optimal matroid bases: an algorithm based on cocircuits. Quart. J. Math. (Oxford) (2) 31 (1980), 65-69.

• The determination of necessary and sufficient conditions for the existence of a solution to the 3x3x3 multi-index problem. Aplikace Mathematiky 24 (1979), 201-208 (with G. Smith).

• Hereditary circuit spaces. Compositio Math. 37 (1978), 339-351 (with V.M. Bryant and Hazel Perfect).

• Designs and circuit spaces. Archiv der Math. 30 (1978), 665-671 (with V.M. Bryant).

• Circuits and balanced sets. Ph.D. thesis, Dept. of Pure Mathematics, University of Sheffield, 1978.

• Balanced sets and circuits in a transversal space. J. Combinatorial Theory (B) 23 (1977), 14-23.

• A remark on an exchange theorem for bases. J. Math. Anal. & Appl. 62 (1978), 354-355.

• Independence spaces and transversals. M.Sc. essay, Dept. of Pure Mathematics, University of Sydney, 1975.

Technical Reports, etc

• Jeremy E. Dawson, Formalising General Correctness, In Theorem Proving in Higher Order Logics, NASA/CP-2002-211736, 36-47.

• Jeremy E. Dawson & Matt Fairtlough, Automatic Constraint Calculation using Lax Logic, In Theorem Proving in Higher Order Logics, NASA/CP-2002-211736, 48-59.

• Jeremy E. Dawson, Simulating Term-Rewriting in LPF and in Display Logic, Theorem Proving in Higher Order Logics: Emerging Trends (supplementary proceedings of TPHOLs'98), TR-CS-98-08, Australian National University, 47-62.

Submitted or in preparation

• Jeremy E. Dawson, Compound Monads and the Kleisli Category.