| MCK: Model checking the logic of knowledge P Gammie, R Van Der Meyden Computer Aided Verification: 16th International Conference, CAV 2004, Boston …, 2004 | 333 | 2004 |
| seL4: from general purpose to a proof of information flow enforcement T Murray, D Matichuk, M Brassil, P Gammie, T Bourke, S Seefried, ... 2013 IEEE Symposium on Security and Privacy, 415-429, 2013 | 303 | 2013 |
| seL4 enforces integrity T Sewell, S Winwood, P Gammie, T Murray, J Andronick, G Klein International Conference on Interactive Theorem Proving, 325-340, 2011 | 122 | 2011 |
| Noninterference for operating system kernels T Murray, D Matichuk, M Brassil, P Gammie, G Klein Certified Programs and Proofs: Second International Conference, CPP 2012 …, 2012 | 85 | 2012 |
| Relaxing safely: verified on-the-fly garbage collection for x86-TSO P Gammie, AL Hosking, K Engelhardt ACM SIGPLAN Notices 50 (6), 99-109, 2015 | 36 | 2015 |
| Synchronous digital circuits as functional programs P Gammie ACM Computing Surveys (CSUR) 46 (2), 1-27, 2013 | 30 | 2013 |
| Model checking knowledge and linear time: PSPACE cases K Engelhardt, P Gammie, R Van Der Meyden Logical Foundations of Computer Science: International Symposium, LFCS 2007 …, 2007 | 20 | 2007 |
| Provable Security: How feasible is it? G Klein, T Murray, P Gammie, T Sewell, S Winwood 13th Workshop on Hot Topics in Operating Systems (HotOS XIII), 2011 | 16 | 2011 |
| Short note: Strict unwraps make worker/wrapper fusion totally correct P Gammie Journal of Functional Programming 21 (2), 209-213, 2011 | 7 | 2011 |
| The Stern–Brocot tree. Archive of Formal Proofs (2015) P Gammie, A Lochbihler | 5 | 2012 |
| The worker/wrapper transformation P Gammie Archive of Formal Proofs (Oct. 2009). URL: http://afp. sf. net/entries …, 2009 | 4 | 2009 |
| Peter Van Roy and Seif Haridi. Concepts, Techniques, and Models of Computer Programming. The MIT Press, 2004. ISBN: 0262220695 Price $70. 930pp. P Gammie Journal of Functional Programming 19 (2), 254-256, 2009 | 3 | 2009 |
| Stable matching P Gammie Archive of Formal Proofs, 2016 | 2 | 2016 |
| CAmkES glue code semantics M Fernandez, P Gammie, J Andronick, G Klein, I Kuz NICTA and UNSW, 2013 | 2 | 2013 |
| The Tortoise and the Hare Algorithm P Gammie | 1 | 2015 |
| Verified synthesis of knowledge-based programs in finite synchronous environments P Gammie International Conference on Interactive Theorem Proving, 87-102, 2011 | 1 | 2011 |
| Lambda-Calculus and Combinators: An Introduction, by JR Hindley and JP Seldin P Gammie Journal of Functional Programming 21 (1), 115-117, 2011 | 1 | 2011 |
| Concurrent HOL P Gammie Arch. Formal Proofs 2024, 2024 | | 2024 |
| Putting the ‘K’into Bird’s derivation of Knuth-Morris-Pratt string matching P Gammie | | 2024 |
| The Kuratowski Closure-Complement Theorem P Gammie, G Gioiosa | | 2024 |
Gerwin KleinProofcraft and UNSWVerified email at unsw.edu.au
