Jeremy Edward DAWSON

Refereed Publications

Computer Science

• Jeremy Dawson, Nachum Dershowitz, Rajeev Goré, Well-Founded Unions, In: Automated Reasoning (IJCAR 2018), Oxford, LNCS/LNAI 10900, 117-133.

• Jeremy E. Dawson & Rajeev Goré, Machine-checked Meta-theory of Dual-Tableaux for Intuitionistic Logic, in Ewa Orlowska on Relational Methods in Logic and Computer Science, pp 253-282, Springer series Outstanding Contributions to Logic, 17, 2018

• Jeremy E. Dawson & Rajeev Goré, Issues in Machine-Checking the Decidability of Implicational Ticket Entailment. In: Automated Reasoning with Analytic Tableaux and Related Methods 2017 (Tableaux 2017), LNAI 10501, 347-363.

• Jeremy E. Dawson, James Brotherston & Rajeev Goré, Machine-checked Interpolation Theorems for Substructural Logics using Display Calculi. In: International Joint Conference on Automated Reasoning, Coimbra, Portugal, 2016 (IJCAR 2016), LNCS 9706, 452-468.

• Jeremy E. Dawson, Rajeev Goré & Jesse Wu, Machine-Checked Proof-Theory for Propositional Modal Logics. In: Progress Computer Science(Birkhäuser), Vol. 28, Reinhard Kahle et al. (Eds): Advances in Proof Theory, Chapter 5

• Jeremy E. Dawson, Rajeev Goré, Thomas Meumann: Machine-Checked Reasoning About Complex Voting Schemes Using Higher-Order Logic. In Proc. E-Voting and Identity - 5th International Conference, VoteID 2015, Bern, Switzerland, September 2-4, 2015.

• Jeremy E. Dawson, Ranald Clouston, Rajeev Goré & Alwen Tiu, From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic. In Proc. TCS 2014: Theoretical Computer Science, LNCS 8705, 250-264.

• Ranald Clouston, Jeremy E. Dawson, Rajeev Goré & Alwen Tiu, Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic. In Proc. CSL 2013: European Conferences on Computer Science Logics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, LIPIcs, 23:197-214.

• Jeremy E. Dawson & Rajeev Goré, Generic Methods for Formalising Sequent Calculi Applied to Provability Logic. In Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2010), LNCS 6397, 263-277.

• Alwen Tiu, Rajeev Goré & Jeremy Dawson, A Proof Theoretic Analysis of Intruder Theories. Logical Methods in Computer Science 6 (3:12), 2010, 1-37. http://arxiv.org/pdf/1005.4508

• Alwen Tiu & Jeremy E. Dawson, Automating Open Bisimulation Checking for the Spi Calculus. In Computer Security Foundations Symposium (CSF 2010), 307-321, IEEE Computer Society 2010.

• Jeremy E. Dawson & Alwen Tiu, Formalising Observer Theory for Environment-Sensitive Bisimulation. In 22nd International Conference on Theorem Proving in Higher Order Logics, Munich, August 2009 (TPHOLs 2009), LNCS 5674, 244-259.

• Jeremy E. Dawson & Rajeev Goré, Termination of Abstract Reduction Systems. International Journal of Foundations of Computer Science 20 (2009), 57-82.

• 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, Categories and Monads in HOL-Omega