Emeritus Professor Rajeev Gore
BSc MSc *Melbourne*, PhD *Cambridge*
Professor
ANU College of Engineering, Computing and Cybernetics
T:
6125 8603
Areas of expertise
- Analysis Of Algorithms And Complexity 080201
- Mathematical Logic, Set Theory, Lattices And Universal Algebra 010107
- Computational Logic And Formal Languages 080203
- Computer System Security 080303
- Combinatorics And Discrete Mathematics (Excl. Physical Combinatorics) 010104
- Software Engineering 080309
- Artificial Intelligence And Image Processing 0801
- Computation Theory And Mathematics 0802
Research interests
Electronic Voting and Vote-Counting, Proof Methods for Non-classical Logics, Term Rewriting, Interactive Theorem Proving, Automated Reasoning, Logic
Biography
I obtained my PhD from the Computer Laboratory of the University of Cambridge in 1992. Before that I was at the University of Melbourne, completing a BSc (hons I) with a double major in Physics and Computer Science, and an MSc in design automation.
Duties:
Available student projects
Practical access control in Java - Keywords: Access control, runtime verification, monitoring, temporal logic, Java
Publications
- Hou, Z, Clouston, R, Gore, R et al. 2018, 'Modular Labelled Sequent Calculi for Abstract Separation Logics', ACM Transactions on Computational Logic, vol. 19, no. 2, pp. 1-35pp.
- 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.
- Gore, R & Lebedeva, E 2017, Simulating STV hand-counting by computers considered harmful: A.C.T.
- 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.
- Verity, F, Pattinson, D & Gore, R 2016, 'Modular Synthesis of Provably Correct Vote Counting Programs', 1st International Joint Conference on Electronic Voting, E-Vote-ID 2016, ed. R Krimmer, M Volkamer, J Barrat, J Benaloh, N Goodman, P Ryan and V Teague, Springer International Publishing AG, Switzerland, pp. 55-70pp.
- Alarcon D and Gore, R 2016, 'Efficient Error Localisation and Imputation for Real-World Census Data Using SMT', Australian Computer Science Conference 2016, Association for Computing Machinery (ACM), Australia, pp. 1-10. Won Best Paper award.
- Clouston, R & Gore, R 2015, 'Sequent Calculus in the Topos of Trees', 18th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2015, ed. Andrew Pitts, Springer, Berlin, pp. 133-147.
- Hou, Z, Gore, R & Tiu, A 2015, 'Automated Theorem Proving for Assertions in Separation Logic with All Connectives', 25th International Conference on Automated Deduction CADE 2015, ed. Amy P. Felty, Aart Middeldorp, Springer International Publishing AG, Switzerland, pp. 501-516.
- 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.
- Gore, R, Li, J , Pagram, T 2015, 'Implementing Modal Tableaux Using Sentential Decision Diagrams', 28th Australasian Joint Conference on Artificial Intelligence AI 2015, ed. B. Pfahringer and J Renz, Springer International Publishing AG, Switzerland, pp. 218-228.
- Hou, Z, Clouston, R, Gore, R et al 2014, 'Proof Search for Propositional Abstract Separation Logics via Labelled Sequents', 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2014, Association for Computing Machinery (ACM), San Diego, CA, pp. 465-476.
- Gore, R & Ramanayake, R 2014, 'Cut-elimination for Weak Grzegorczyk Logic Go', Studia Logica, vol. 102, no. 1, pp. 1-27.
- Gore, R 2014, 'And-or tableaux for fixpoint logics with converse: LTL, CTL, PDL and CPDL', 7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, ed. S Demri, D Kapur, C Weidenbach, Springer Verlag, Switzerland, pp. 26-45.
- Gore, R, Thomson, J & Wu, J 2014, 'A history-based theorem prover for intuitionistic propositional logic using global caching: InthistGC system description', 7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, ed. S Demri, D Kapur, C Weidenbach, Springer Verlag, Switzerland, pp. 262-268.
- Kramer, S, Gore, R & Okamoto, E 2014, 'Computer-aided decision-making with trust relations and trust domains (cryptographic applications)', Journal of Logic and Computation, vol. 24, no. 1, pp. 19-54.
- 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.
- Beckert, B, Gore, R, Schurmann, C et al 2014, 'Verifying voting schemes', Journal of Information Security and Applications, vol. 19, pp. 115-129.
- Gore, R & Meumann, T 2014, 'Proving the monotonicity criterion for a plurality vote-counting program as a step towards verified vote-counting', 6th International Conference on Electronic Voting: Verifying the Vote (EVOTE) 2014, IEEE, USA, pp. 1-7.
- Gore, R, Kooi, B & Kurucz, A, eds, 2014, Advances in Modal Logic, Volume 10, College Publications, London UK.
- Beckert, B, Bormer, T, Gore, R et al 2014, 'Reasoning About Vote Counting Schemes Using Light-weight and Heavy-weight Methods', 8th International Verification Workshop. Held as Part of the Vienna Summer of Logic, VSL 2014
- Gore, R, Olesen, K & Thomson, J 2014, 'Implementing tableau calculi using BDDs: BDDTab system description', 7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, ed. S Demri, D Kapur, C Weidenbach, Springer Verlag, Switzerland, pp. 337-343.
- Gore, R & Nguyen, L 2013, 'ExpTime Tableaux for ALC Using Sound Global Caching', Journal of Automated Reasoning, vol. 50, no. 4, pp. 355-381.
- Beckert, B, Gore, R & Schurmann, C 2013, 'Analysing Vote Counting Algorithms via Logic And Its Application to the CADE Election Scheme', 24th International Conference on Automated Deduction CADE-24, ed. Maria Paola Bonacina, Springer, LNCS 7898 pp. 135-144.
- Beckert, B, Gore, R & Schurmann, C 2013, 'On the Specification and Verification of Voting Schemes, Lecture Notes in Computer Science (LNCS), vol. 7985, no. 2013, pp. 25-40.
- 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.
- Gore, R & Thomson, J 2013, 'An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description', 24th International Conference on Automated Deduction CADE-24, ed. Maria Paola Bonacina, Springer, LNCS Voume 7898 pp. 275-281.
- Hou, Z, Tiu, A & Gore, 2013,'A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search', TABLEAUX 2013, ed. D. Galmiche and D. Larchey-Wendling, Springer-Verlag Berlin Heidelberg, USA, pp. 172-187.
- Awad, A, Gore, R, Hou, Z et al 2012, 'An iterative approach to synthesize business process templates from compliance rules', Information Systems Journal, vol. 37, no. 8, pp. 714-736.
- Gore, R & Ramanayake, R 2012, 'Labelled tree sequents, Tree hypersequents and Nested (Deep) Sequents', Advances in Modal Logic (AiML 2012), College Publications, Unknown, pp. 279-299.
- Gore, R & Ramanayake, R 2012, 'Valentini's cut-elimination for provability logic resolved', Review of Symbolic Logic, vol. 5, no. 2, pp. 212-238.
- Gore, R & Thomson. 'BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics', Lecture Notes in Computer Science (LNCS), vol. 7364, pp. 301-315, 2012.
- Tiu, A, Ianovski, E & Gore, R 2012, 'Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures', Advances in Modal Logic (AiML 2012), College Publications, Kings College London, pp. 1-22.
- Gore, R, Thomson, J & Widmann, F 2011, 'An Experimental Comparison of Theorem Provers for CTL', International Symposium on Temporal Representation and Reasoning (TIME 2011), ed. Carlo Combi, Martin Leucker and Frank Wolter, IEEE Computer Society, Los Alamitos USA, pp. 49-56.
- Gore, R, Postniece, L & Tiu, A 2011, 'On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics', Logical Methods in Computer Science, vol. 7, no. 2, p. 38.
- Awad, A, Gore, R, Thomson, J et al 2011, 'An Iterative Approach for Business Process Template Synthesis from Compliance Rules', Lecture notes in computer science, vol. 6741, pp. 406-421.
- Brotherston, J & Gore, R 2011, 'Craig Interpolation in Displayable Logics', TABLEAUX 2011, Lecture notes in computer science, vol. 6793, pp. 88-103.
- Gore, R, Kupke, C, Pattinson, D et al 2010, 'Global Caching for Coalgebraic Description Logics', International Joint Conference on Automated Reasoning (IJCAR 2010), ed. Conference Program Committee, Conference Organising Committee, Scotland, p. 15.
- Tran, K, Compton, M, Wu, J et al 2010, 'Semantic Sensor Composition', Semantic Sensor Networks SSN 2010, ed. Kerry Taylor, Arun Ayyagari and David De Roure, CEUR-WS.ORG, online, p. 16.
- Kramer, S, Gore, R & Okamoto, E 2010, 'Formal definitions and complexity results for trust relations and trust domains fit for TTPs, the Web of Trust, PKIs, and ID-Based Cryptography', SIGACT News, vol. 41, no. 1.
- 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.
- Gore, R & Widmann, F 2010, 'Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse', International Joint Conference on Automated Reasoning (IJCAR 2010), Conference Organising Committee, Scotland.
- Gore, R, Kupke, C & Pattinson, D 2010, 'Optimal Tableau Algorithms for Coalgebraic Logics', International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2010, ed. J. Esparza and R Majumdar, Springer, Berlin, Germany.
- Gore, R, Postniece, L & Tiu, A 2010, 'Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic', Advances in Modal Logic (AiML 2010), ed. Lev Beklemishev et al, College Publications, , pp. 156-177.
- 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.
- Gore, R 2009, 'Machine checking proof theory: An application of logic to logic', Indian Conference on Logic and Its Applications (ICLA 2009), ed. R. Ramanujam, S. Sarukkai, Springer, Berlin, Germany, pp. 23-35.
- Bauer, A, Gore, R & Tiu, A 2009, 'A first-order policy language for history-based transaction monitoring', International Colloquium on Theoretical Aspects of Computing (ICTAC 2009), ed. Martin Leucker, Charles C. Morgan, Springer, Berlin, Germany, pp. 96-111.
- Gore, R & Nguyen, L 2009, 'Clausal Tableaux for Multimodal Logics of Belief', Fundamenta Mathematicae, vol. 94, no. 1, pp. 21-40.
- Tiu, A & Gore, R 2009, 'A Proof Theoretic Analysis of Intruder Theories', International conference on Rewriting Techniques and Applications (RTA 2009), ed. Ralf Treinen, Springer, Brasilia, Brazil, pp. 103-117.
- Gore, R, Postniece, L & Tiu, A 2009, 'Taming displayed tense logics using nested sequents with deep inference', International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2009), ed. Conference Program Committee, Springer, Oslo, Norway, pp. 189-204.
- Gore, R & Widmann, F 2009, 'An Optimal On-the-fly Tableau-based Decision Procedure for PDL satisfiability', International Conference on Automated Deduction (CADE 2009), ed. R A Schmidt, Springer, berlin, pp. 437-452.
- Gore, R 2009, 'Global caching, inverse roles and fixpoint logics', International workshop on Description Logics (DL 2009), ed. B. Grau, I. Horrocks, B.Motik, U.Sattler, CEUR-WS.ORG, UK, p. 11.
- Gore, R & Widmann, F 2009, 'Sound Global State Caching for ALC with Inverse roles', International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2009), ed. Conference Program Committee, Springer, Oslo, Norway, pp. 205-219.
- Abate, P, Gore, R & Widmann, F 2009, 'An on-the-fly Tableau-based decision procedure for PDL-satisfiability', Workshop on Methods for Modalities (M4M5 2007), ed. C. Areces, S. Demri, Elsevier, The Netherlands, pp. 191-209.
- Abate, P & Gore, R 2009, 'System description: The Tableau workbench', Workshop on Methods for Modalities (M4M5 2007), ed. C. Areces, S. Demri, Elsevier, The Netherlands, pp. 55-67.
- Dawson, J & Gore, R 2009, 'Termination of abstract reduction systems', International Journal of Foundations of Computer Science, vol. 20, no. 1, pp. 57-82.
- Gore, R & Nguyen, L 2008, 'Analytic cut-free Tableaux for regular modal logics of agent beliefs', in F. Sadri, K. Satoh (ed.), Computational Logic in Multi-Agent Systems, Springer, Berlin, Germany, pp. 268-287.
- Gore, R & Postniece, L 2008, 'Combining Derivations and Refutations for Cut-free Completeness in Bi-intuitionistic Logic', Journal of Logic and Computation, vol. 20, no. 1, pp. 233-260.
- Gore, R & Postniece, L 2008, 'An experimental evaluation of global caching for ALC (system description)', International Joint Conference on Automated Reasoning (IJCAR 2008), ed. Alessandro Armando, Peter Baumgartner and Giles Dowek, Springer, Berlin, Germany, pp. 299-305.
- Gore, R, Postniece, L & Tiu, A 2008, 'Cut-elimination and proof-search for bi-intutionistic logic using nested sequents', Advances in Modal Logic (AiML 2008), ed. Carlos Areces and Robert Goldblatt, College Publications, United Kingdom, pp. 43-66.
- Gore, R & Ramanayake, D 2008, 'Valentini's cut-elimination for provability logic resolved', Advances in Modal Logic (AiML 2008), ed. Carlos Areces and Robert Goldblatt, College Publications, United Kingdom, pp. 67-86.
- Abate, P, Gore, R & Widmann, F 2007, 'One-pass tableaux for computation tree logic', International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2007), ed. Nachum Dershowitz, Andrei Voronkov, Springer, USA, pp. 32-46.
- 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.
- Gore, R & Tiu, A 2007, 'Classical modal display logic in the calculus of structures and minimal cut-free deep inference calculi for S5', Journal of Logic and Computation, vol. 17, no. 4, pp. 767-794.
- Gore, R & Nguyen, L 2007, 'EXPTIME tableaux with global caching for description logics with transitive roles, inverse roles and role hierarchies', International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2007), ed. Olivetti, Nicola, Springer, Berlin, pp. 133-148.
- Gore, R & Nguyen, L 2007, 'EXPTIME tableaux for ALC using sound global caching', International Workshop on Description Logics (DL 2007), ed. Diego Calvanese et al, Bozen-Bolzano University Press, Bozen-Bolzano, p. 8.
- Postniece, L & Gore, R 2007, 'A cut-free sequent calculus for bi-intuitionistic logic', International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2007), ed. Olivetti, Nicola, Springer, Berlin, pp. 90-106.
- Gore, R & Nguyen, L 2005, 'A tableau calculus with automaton-labelled formulae for regular grammar logics', International Conference on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX 2005), ed. Bernhard Beckert, Springer, Berlin Germany, pp. 138-152.
- Nguyen, L & Gore, R 2005, 'Completeness of hyper-resolution via the semantics of disjunctive logic programs', Information Processing Letters, vol. 95, no. 2, pp. 363-369.
- Boskovitz, A, Gore, R & Wong, P 2005, 'Data editing and logic', United Nations Statistical Commission and Economic Commission for Europe Conference of European Statisticians 2005, ed. UNECE, United Nations Economic Commission for Europe, online, pp. 1-12.
- Boskovitz, A & Gore, R 2005, 'Automatic data editing: A framework from logic', Session of the International Statistical Institute 2005, ed. Dennis Trewin, International Statistical Institute, Sydney NSW, Australia, pp. 1-2.
- 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.
- Davoren, J, Moor, T, Gore, R et al 2004, 'On two-sided approximate model-checking: problem formulation and solution via finite topologies', in Y. Lakhnech, S. Yovine (ed.), Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Springer, Heidelberg, Germany, pp. 52-67.
- Abate, P & Gore, R 2003, 'The Tableaux Work Bench', International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2003), ed. Marta Cialdea Mayer, Fiora Pirri, Springer, Berlin, pp. 230-236.
- Boskovitz, A, Gore, R & Hegland, M 2003, 'A Logical Formalisation of the Fellegi-Holt Method of Data Cleaning', International Symposium on Intelligent Data Analysis (IDA 2003), ed. Berthold, Lenz, Bradley, Kruse, Borgelt, Springer, Berlin, pp. 554-565.
- 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.
- Gore, R 2003, 'An introduction to classical propositional logic: syntax, semantics, sequents', in Helen Lauer (ed.), History and Philosophy of Science for African Undergraduates, Hope Publications Ltd, Ibadan, Nigeria, pp. 597-643.
- Gore, R & Nguyen, P 2002, 'CardS4: modal theorem proving on Java smart cards', Journal of Telecommunications and Information Technology, vol. 4/2002, pp. 68-80.
- Demri, S & Gore, R 2002, 'Theoremhood-preserving maps characterising cut elimination for modal provability logics', Journal of Logic and Computation, vol. 12, no. 5, pp. 861-884.
- 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.
- Demri, S, Gore, R & Demri, S 2002, 'Display calculi for nominal tense logics', Journal of Logic and Computation, vol. 12, no. 6, pp. 993-1016.
- 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.
- Gore, R & Beckert, B 2001, 'Free-variable tableaux for propositional modal logic', Studia Logica, vol. 69, pp. 59-96.
- Gore, R & Nguyen, P 2001, 'CARDS4: Modal Theorem Proving on Java Smartcards', in Isabelle Attali Thomas Jensen (ed.), Smart Card Programming and Security, Springer, Germany, pp. 111-124.
- Gore, R & Nguyen, P 2001, 'CardKt: Automated multi-modal deduction on Java cards for multi-application security', in Attali, I & Jensen, T (ed.), Java on Smart Cards: Programming and Security, Springer, Berlin, pp. 38-51.
- Davoren, J & Gore, R 2000, 'Bimodal Logics for Reasoning about Continuous Dynamics', Advances in Modal Logic (AiMT-ICTL 2000), Unknown, unknown, pp. 51-60.
- Gore, R 2000, 'Dual Intuitionistic Logic Revisited', International Conference on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX 2000), Springer, Berlin, Germany, pp. 252-267.
- 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.
- Demri, S & Gore, R 2000, 'Display Calculi for Logics with Relative Accessibility Relations', Journal of Logic, Language and Information, vol. 9, pp. 213-236.
- Demri, S & Gore, R 2000, 'Theoremhood preserving maps characterising cut-elimination for modal provability logics', Annual Summer Meeting of the Association for Symbolic Logic - Logic Colloquium 2000, RA Sorbonne Association for Symbolic Logic, Paris, France, p. 14.
- Demri, S & Gore, R 2000, 'An O((n-logn)3)-Time Transformation from GRZ into Decidable Fragments of Classical First Order Logic', International Workshop on First-Order Theorem Proving (FTP 1998), Springer, Germany, pp. 152-166.
- Gore, R & Demri, S 1999, 'Cut-free display calculi for nominal tense logics', International Conference on Theorem Proving with Analytic Tableaux and Related methods (TABLEAUX 1999), ed. Kanade, T et al, Springer, Berlin, pp. 155-170.
- Gore, R 1999, 'System description: KtSeqC', International Conference on Theorem Proving with Analytic Tableaux and Related methods (TABLEAUX 1999), ed. Kanade, T et al, Springer, Berlin, pp. 29-31.
- Gore, R & Demri, S 1999, 'Tractable transformation from modal provability logics into first-order logic', International Conference of Automated Deduction (CADE 1999), Springer, Berlin, pp. 16-30.
- Gore, R 1999, 'Tableaux methods for modal and temporal logics', in M. D'Agostine (ed.), Handbook of Tableaux Methods, Kluwer Academic Publishers, Unknown, pp. 297-396.
Projects and Grants
Grants information is drawn from ARIES. To add or update Projects or Grants information please contact your College Research Office.
- Machine-checked Foundations for Verified Vote Counting (Primary Investigator)
- Mechanised Foundations of Proof Calculi (Primary Investigator)
