| MCK: Model checking the logic of knowledge P Gammie, R Meyden International Conference on Computer Aided Verification, 479-483, 2004 | 309 | 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 | 248 | 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 | 106 | 2011 |
| Noninterference for operating system kernels T Murray, D Matichuk, M Brassil, P Gammie, G Klein International Conference on Certified Programs and Proofs, 126-142, 2012 | 69 | 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 | 35 | 2015 |
| Synchronous digital circuits as functional programs P Gammie ACM Computing Surveys (CSUR) 46 (2), 1-27, 2013 | 27 | 2013 |
| Model checking knowledge and linear time: PSPACE cases K Engelhardt, P Gammie, R Meyden International Symposium on Logical Foundations of Computer Science, 195-211, 2007 | 18 | 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 | 15 | 2011 |
| Short note: Strict unwraps make worker/wrapper fusion totally correct P Gammie Journal of Functional Programming 21 (2), 209-213, 2011 | 8 | 2011 |
| The worker/wrapper transformation P Gammie Archive of Formal Proofs (Oct. 2009). URL: http://afp. sf. net/entries …, 2009 | 5 | 2009 |
| The Stern–Brocot tree. Archive of Formal Proofs (2015) P Gammie, A Lochbihler | 4 | 2012 |
| 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 |
| 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 | 2 | 2009 |
| The Kuratowski closure-complement theorem P Gammie, G Gioiosa | 1 | 2021 |
| 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 |
| Putting the ‘K’into Bird’s derivation of Knuth-Morris-Pratt string matching P Gammie | | 2021 |
| December 14, 2021 P Gammie | | 2021 |
| The Tortoise and the Hare Algorithm P Gammie | | 2016 |
Gerwin KleinProofcraft and UNSWVerified email at unsw.edu.au
