Dr Jeremy Dawson
Areas of expertise
- Mathematical Logic, Set Theory, Lattices And Universal Algebra 010107
- Computational Logic And Formal Languages 080203
- Combinatorics And Discrete Mathematics (Excl. Physical Combinatorics) 010104
- Artificial Intelligence And Image Processing 0801
- Computation Theory And Mathematics 0802
- Computer Software 0803
Biography
Research interests:
Formal verification; Automated theorem proving, especially in relation to metalogic and cut-elimination, termination of term-rewriting; Functional programming.
Duties:
My research work previously at NICTA (and, prior to that, in my position as a Senior Research Associate on an ARC Large Grant held by Dr Rajeev Gore at the ANU) has largely been embedding a display calculus in Isabelle/HOL, and proving, in Isabelle, Belnap's cut-elimination theorem. In the course of work on a stronger result, the strong normalization property of the set of proof reductions used in cut-elimination, we discovered that the published proof of this omits a case, requiring a largely new proof, which we have now completed. We have realised that this proof can be translated into the context of general term-rewriting theory, and have accordingly derived theorems on termination of term-rewriting. Recently I have also mechanised some cut-elimination proofs for sequent calculi. I've been doing other things as well, see the publication list on my homepage. In the last couple of years with NICTA I was mostly working on Isabelle theories for fixed-length words in support of NICTA's L4 MicroKernel Verification project. Since returning to RSISE I first worked on machine-checked proof theory, doing a proof in Isabelle of the cut-elimination result for provability logic. Now I am working with Alwen Tiu on machine-checked proofs for the spi-calculus. Most recently I have formalised bitrace consistency, and proved results making it clear that consistency of an observer theory is decidable. I have also proved results which show, in combination with other published work, that consistency of a bitrace is decidable.
Formal verification; Automated theorem proving, especially in relation to metalogic and cut-elimination, termination of term-rewriting; Functional programming.
Duties:
My research work previously at NICTA (and, prior to that, in my position as a Senior Research Associate on an ARC Large Grant held by Dr Rajeev Gore at the ANU) has largely been embedding a display calculus in Isabelle/HOL, and proving, in Isabelle, Belnap's cut-elimination theorem. In the course of work on a stronger result, the strong normalization property of the set of proof reductions used in cut-elimination, we discovered that the published proof of this omits a case, requiring a largely new proof, which we have now completed. We have realised that this proof can be translated into the context of general term-rewriting theory, and have accordingly derived theorems on termination of term-rewriting. Recently I have also mechanised some cut-elimination proofs for sequent calculi. I've been doing other things as well, see the publication list on my homepage. In the last couple of years with NICTA I was mostly working on Isabelle theories for fixed-length words in support of NICTA's L4 MicroKernel Verification project. Since returning to RSISE I first worked on machine-checked proof theory, doing a proof in Isabelle of the cut-elimination result for provability logic. Now I am working with Alwen Tiu on machine-checked proofs for the spi-calculus. Most recently I have formalised bitrace consistency, and proved results making it clear that consistency of an observer theory is decidable. I have also proved results which show, in combination with other published work, that consistency of a bitrace is decidable.
Publications
- Dawson, J E & Gore, R 2017, 'Issues in machine-checking the decidability of implicational ticket entailment', 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2017, ed. Renate A. Schmidt and Claudia Nalon, Springer International Publishing, Cham, Switzerland, pp. 347-363.
- Dawson, J, Gore, R & Wu, J 2016, 'Machine-Checked Proof-Theory for Propositional Modal Logics', in Reinhard Kahle, Thomas Studer, Thomas Strahm (ed.), Advances in Proof Theory, Birkhauser Verlag, Switzerland, pp. 173-243.
- Dawson, J, Brotherston, J & Gore, R 2016, 'Machine-checked interpolation theorems for substructural logics using display calculi', International Joint Conference on Automated Reasoning, IJCAR 2016, ed. Olivetti N.Tiwari A., Springer Verlag, Germany, pp. 452-468.
- Dawson, J, Gore, R & Meumann, T 2015, 'Machine-checked reasoning about complex voting schemes using higher-order logic', 5th International Conference on E-Voting and Identity, VoteID 2015, ed. Haenni. R, Koenig R.E,Wikstrom. D, Springer International Publishing Switzerland, TBC, pp. 142-158.
- Dawson, J, Clouston, R, Gore, R et al 2014, 'From display calculi to deep nested sequent calculi: Formalised for full intuitionistic linear logic', 8th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science, TCS 2014, Springer Verlag, Rome Italy, pp. 250-264.
- Clouston, R, Dawson, J, Gore, R, et al 2013, 'Annotation-Free Sequent Calculi for full Intuitionistic Linear Logic - Extended Version', Logical Methods in Computer Science, vol. Online (published dates tbc), pp. 1-18.
- Dawson, J & Gore, R, 2010, 'Generic methods for formalising sequent Calculi applied to provability logic', International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2010), ed. Christian G. Ferm, Springer, Berlin, pp. 263-277.
- Tiu, A & Dawson, J 2010, 'Automating Open Bisimulation Checking for the Spi Calculus', IEEE Computer Security Foundations Symposium 2010, IEEE Computer Society, pp. 307 - 321.
- Tiu, A, Gore, R & Dawson, J 2010, 'A Proof Theoretic Analysis of Intruder Theories', Logical Methods in Computer Science, vol. 6, no. 3, pp. 1-37.
- Dawson, J 2009, 'Isabelle theories for machine words', Electronic Notes in Theoretical Computer Science, vol. 250, no. 1, pp. 55-70.
- Dawson, J & Gore, R 2009, 'Termination of abstract reduction systems', International Journal of Foundations of Computer Science, vol. 20, no. 1, pp. 57-82.
- Dawson, J & Tiu, A 2009, 'Formalising Observer Theory for Environment-Sensitive Bisimulation', in S. Berghofer, S Nipkow, C Urban, M Wenzel (ed.), Theorem Proving in Higher Order Logics (TPHOLs), Springer, Berlin, pp. 180-195.
- Dawson, J 2007, 'Formalising generalised substitutions', in Klaus Schneider, Jens Brandt (ed.), Theorem Proving in Higher Order Logics, Springer, Berlin, Germany, pp. 54-69.
- Dawson, J & Gore, R 2007, 'Termination of abstract reduction systems', Computing: The Australasian Theory Symposium (CATS 2007), ed. Joachim Gudmundsson and Barry Jay, Association for Computing Machinery Inc (ACM), Sydney, Australia, pp. 35-44.
- Dawson, J 2007, 'Compound monads in specification languages', Programming Languages meets Program Verification (PLPV 2007), ed. A. Stump, H. Xi, Association for Computing Machinery Inc (ACM), New York, NY USA, pp. 3-10.
- Dawson, J & Gore, R 2004, 'A general theorem on termination of rewriting', Annual Conference of the European Association for Computer Science Logic (CSL 2004), ed. Jerzy Marcinkowski, Andrzej Tarlecki, Springer, Berlin, Germany, pp. 100-114.
- Dawson, J 2004, 'Formalising general correctness', Electronic Notes in Theoretical Computer Science, vol. 91, pp. 21-42.
- Dawson, J & Gore, R 2003, 'A New Machine-checked Proof of Strong Normalisation for Display Logic', Computing: The Australasian Theory Symposium (CATS 2003), ed. James Harland, Elsevier, Netherlands, pp. 20-39.
- Dawson, J & Gore, R 2002, 'Machine-checking the timed interval calculus', Australian Joint Conference on Artificial Intelligence (AI 2002), ed. B. McKay, J. Slaney, Springer, Berlin, Germany, pp. 95-106.
- Dawson, J & Gore, R 2002, 'Formalised cut admissibility for display logic', International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), ed. G. Goos, J. Hartmanis, J. van Leeuwen, Springer, Berlin, pp. 131-147.
- Dawson, J & Gore, R 2001, 'Embedding Display Calculi into Logical Frameworks: Comparing Twelf and Isabelle', Computing: The Australasian Theory Symposium (CATS 2001), ed. Colin Fidge, Elsevier, Netherlands, pp. 89-103.
- Dawson, J & Gore, R 2000, 'Embedding Display Calculi into Logical Frameworks', Australasian Workshop on Computational Logic (AWCL 2000), ed. Lloyd, J, Australian National University, Canberra, pp. 179-188.